MAYBE
Termination Proof using AProVETerm Rewriting System R:
[V1, V2, V, N, L, IL, M]
zeros -> cons-Nat-NatIList(0, zeros)
cons-Nat-NatIList(V1, V2) -> cons-Nat-NatList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-Nat-NatIList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-Nat-NatList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-Nat-os-osb-NatIList-os-csb(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-os-osb-Nat-os-csb-NatIList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-os-osb-Nat-os-csb-NatList(V1, V2)
is'Nat-Nat(V) -> tt
is'Nat-os-osb-Nat-os-csb(V1) -> is'Nat-Nat(V1)
is'NatIList-NatIList(V) -> tt
is'NatIList-NatList(V) -> tt
is'NatIList-os-osb-NatIList-os-csb(V1) -> is'NatIList-NatIList(V1)
is'NatIList-os-osb-NatIList-os-csb(V1) -> is'NatIList-NatList(V1)
is'NatList-NatList(V) -> tt
is'NatList-os-osb-NatIList-os-csb(V1) -> is'NatList-NatIList(V1)
is'NatList-os-osb-NatIList-os-csb(V1) -> is'NatList-NatList(V1)
is'Thruth-Thruth(V) -> tt
is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)
length-NatList(nil) -> 0
length-NatList(cons-Nat-NatList(N, L)) -> s-Nat(length-NatList(L))
length-os-osb-NatIList-os-csb(V1) -> length-NatIList(V1)
length-os-osb-NatIList-os-csb(V1) -> length-NatList(V1)
s-os-osb-Nat-os-csb(V1) -> s-Nat(V1)
take-Nat-NatIList(0, IL) -> nil
take-Nat-NatIList(V1, V2) -> take-Nat-NatList(V1, V2)
take-Nat-NatIList(s-Nat(M), cons-Nat-NatIList(N, IL)) -> cons-Nat-NatList(N, take-Nat-NatIList(M, IL))
take-Nat-NatList(0, IL) -> nil
take-Nat-NatList(s-Nat(M), cons-Nat-NatList(N, IL)) -> cons-Nat-NatList(N, take-Nat-NatList(M, IL))
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-Nat-NatIList(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-Nat-NatList(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-Nat-os-osb-NatIList-os-csb(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-os-osb-Nat-os-csb-NatIList(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-os-osb-Nat-os-csb-NatList(V1, V2)
Termination of R to be shown.
R
↳Remaining Obligation(s)
The following remains to be proven:
[V1, V2, V, N, L, IL, M]
zeros -> cons-Nat-NatIList(0, zeros)
cons-Nat-NatIList(V1, V2) -> cons-Nat-NatList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-Nat-NatIList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-Nat-NatList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-Nat-os-osb-NatIList-os-csb(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-os-osb-Nat-os-csb-NatIList(V1, V2)
cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> cons-os-osb-Nat-os-csb-NatList(V1, V2)
is'Nat-Nat(V) -> tt
is'Nat-os-osb-Nat-os-csb(V1) -> is'Nat-Nat(V1)
is'NatIList-NatIList(V) -> tt
is'NatIList-NatList(V) -> tt
is'NatIList-os-osb-NatIList-os-csb(V1) -> is'NatIList-NatIList(V1)
is'NatIList-os-osb-NatIList-os-csb(V1) -> is'NatIList-NatList(V1)
is'NatList-NatList(V) -> tt
is'NatList-os-osb-NatIList-os-csb(V1) -> is'NatList-NatIList(V1)
is'NatList-os-osb-NatIList-os-csb(V1) -> is'NatList-NatList(V1)
is'Thruth-Thruth(V) -> tt
is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)
length-NatList(nil) -> 0
length-NatList(cons-Nat-NatList(N, L)) -> s-Nat(length-NatList(L))
length-os-osb-NatIList-os-csb(V1) -> length-NatIList(V1)
length-os-osb-NatIList-os-csb(V1) -> length-NatList(V1)
s-os-osb-Nat-os-csb(V1) -> s-Nat(V1)
take-Nat-NatIList(0, IL) -> nil
take-Nat-NatIList(V1, V2) -> take-Nat-NatList(V1, V2)
take-Nat-NatIList(s-Nat(M), cons-Nat-NatIList(N, IL)) -> cons-Nat-NatList(N, take-Nat-NatIList(M, IL))
take-Nat-NatList(0, IL) -> nil
take-Nat-NatList(s-Nat(M), cons-Nat-NatList(N, IL)) -> cons-Nat-NatList(N, take-Nat-NatList(M, IL))
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-Nat-NatIList(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-Nat-NatList(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-Nat-os-osb-NatIList-os-csb(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-os-osb-Nat-os-csb-NatIList(V1, V2)
take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb(V1, V2) -> take-os-osb-Nat-os-csb-NatList(V1, V2)
The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
10:01 minutes