0 QTRS
↳1 QTRSToCSRProof (⇔)
↳2 CSR
↳3 PoloCSRProof (⇔)
↳4 CSR
↳5 PoloCSRProof (⇔)
↳6 CSR
↳7 PoloCSRProof (⇔)
↳8 CSR
↳9 PoloCSRProof (⇔)
↳10 CSR
↳11 PoloCSRProof (⇔)
↳12 CSR
↳13 CSRInnermostProof (⇔)
↳14 CSR
↳15 CSDependencyPairsProof (⇔)
↳16 QCSDP
↳17 QCSDependencyGraphProof (⇔)
↳18 AND
↳19 QCSDP
↳20 QCSDPSubtermProof (⇔)
↳21 QCSDP
↳22 PIsEmptyProof (⇔)
↳23 TRUE
↳24 QCSDP
↳25 QCSUsableRulesProof (⇔)
↳26 QCSDP
↳27 QCSDPMuMonotonicPoloProof (⇔)
↳28 QCSDP
↳29 PIsEmptyProof (⇔)
↳30 TRUE
↳31 QCSDP
↳32 QCSDPReductionPairProof (⇔)
↳33 QCSDP
↳34 QCSDependencyGraphProof (⇔)
↳35 TRUE
↳36 QCSDP
↳37 QCSUsableRulesProof (⇔)
↳38 QCSDP
↳39 QCSDPMuMonotonicPoloProof (⇔)
↳40 QCSDP
↳41 PIsEmptyProof (⇔)
↳42 TRUE
active(zeros) → mark(cons(0, zeros))
active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)
active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))
active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))
active(U52(tt)) → mark(tt)
active(U61(tt, L, N)) → mark(U62(isNat(N), L))
active(U62(tt, L)) → mark(s(length(L)))
active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))
active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U61(isNatList(L), L, N))
active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))
active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))
active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))
active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))
active(U61(X1, X2, X3)) → U61(active(X1), X2, X3)
active(U62(X1, X2)) → U62(active(X1), X2)
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))
U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))
U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))
U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))
U61(mark(X1), X2, X3) → mark(U61(X1, X2, X3))
U62(mark(X1), X2) → mark(U62(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))
proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))
proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))
proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))
proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2, X3)) → U61(proper(X1), proper(X2), proper(X3))
proper(U62(X1, X2)) → U62(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))
U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))
U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))
isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))
U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))
U61(ok(X1), ok(X2), ok(X3)) → ok(U61(X1, X2, X3))
U62(ok(X1), ok(X2)) → ok(U62(X1, X2))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(zeros) → mark(cons(0, zeros))
active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)
active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))
active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))
active(U52(tt)) → mark(tt)
active(U61(tt, L, N)) → mark(U62(isNat(N), L))
active(U62(tt, L)) → mark(s(length(L)))
active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))
active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U61(isNatList(L), L, N))
active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))
active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))
active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))
active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))
active(U61(X1, X2, X3)) → U61(active(X1), X2, X3)
active(U62(X1, X2)) → U62(active(X1), X2)
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))
U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))
U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))
U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))
U61(mark(X1), X2, X3) → mark(U61(X1, X2, X3))
U62(mark(X1), X2) → mark(U62(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))
proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))
proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))
proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))
proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2, X3)) → U61(proper(X1), proper(X2), proper(X3))
proper(U62(X1, X2)) → U62(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))
U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))
U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))
isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))
U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))
U61(ok(X1), ok(X2), ok(X3)) → ok(U61(X1, X2, X3))
U62(ok(X1), ok(X2)) → ok(U62(X1, X2))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).
zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set
Used ordering:
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
POL(0) = 0
POL(U11(x1)) = x1
POL(U21(x1)) = 2·x1
POL(U31(x1)) = x1
POL(U41(x1, x2)) = 2 + x1 + x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = 2·x1
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3
POL(U62(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = 2 + x1
POL(isNatList(x1)) = 0
POL(length(x1)) = x1
POL(nil) = 0
POL(s(x1)) = 2·x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set
Used ordering:
U31(tt) → tt
POL(0) = 0
POL(U11(x1)) = x1
POL(U21(x1)) = 2·x1
POL(U31(x1)) = 2 + 2·x1
POL(U41(x1, x2)) = 2·x1 + x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = 2·x1
POL(U52(x1)) = 2·x1
POL(U61(x1, x2, x3)) = 2·x1 + x2 + x3
POL(U62(x1, x2)) = 2·x1 + x2
POL(cons(x1, x2)) = x1 + 2·x2
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = 0
POL(length(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set
Used ordering:
length(nil) → 0
POL(0) = 0
POL(U11(x1)) = 2·x1
POL(U21(x1)) = 2·x1
POL(U41(x1, x2)) = 2·x1
POL(U42(x1)) = 2·x1
POL(U51(x1, x2)) = 2·x1
POL(U52(x1)) = 2·x1
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2
POL(U62(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = 0
POL(isNatList(x1)) = 0
POL(length(x1)) = x1
POL(nil) = 1
POL(s(x1)) = 2·x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set
Used ordering:
U11(tt) → tt
isNat(length(V1)) → U11(isNatList(V1))
POL(0) = 0
POL(U11(x1)) = 1 + x1
POL(U21(x1)) = x1
POL(U41(x1, x2)) = x1 + 2·x2
POL(U42(x1)) = 2·x1
POL(U51(x1, x2)) = x1 + 2·x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3
POL(U62(x1, x2)) = 1 + x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = 2·x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 1 + 2·x1
POL(nil) = 0
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros: empty set
cons: {1}
0: empty set
tt: empty set
U21: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set
Used ordering:
isNatList(nil) → tt
POL(0) = 0
POL(U21(x1)) = x1
POL(U41(x1, x2)) = x1 + 2·x2
POL(U42(x1)) = 2·x1
POL(U51(x1, x2)) = x1 + 2·x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = x1 + 2·x2 + x3
POL(U62(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = 2·x1
POL(length(x1)) = 2·x1
POL(nil) = 2
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros: empty set
cons: {1}
0: empty set
tt: empty set
U21: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros: empty set
cons: {1}
0: empty set
tt: empty set
U21: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
Innermost Strategy.
U41'(tt, V2) → U42'(isNatIList(V2))
U41'(tt, V2) → ISNATILIST(V2)
U51'(tt, V2) → U52'(isNatList(V2))
U51'(tt, V2) → ISNATLIST(V2)
U61'(tt, L, N) → U62'(isNat(N), L)
U61'(tt, L, N) → ISNAT(N)
U62'(tt, L) → LENGTH(L)
ISNAT(s(V1)) → U21'(isNat(V1))
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → U41'(isNat(V1), V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → U51'(isNat(V1), V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U61'(isNatList(L), L, N)
LENGTH(cons(N, L)) → ISNATLIST(L)
U62'(tt, L) → L
zeros
U62'(tt, L) → U(L)
U(zeros) → ZEROS
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
ISNAT(s(V1)) → ISNAT(V1)
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ISNAT(s(V1)) → ISNAT(V1)
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
ISNATLIST(cons(V1, V2)) → U51'(isNat(V1), V2)
U51'(tt, V2) → ISNATLIST(V2)
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
zeros → cons(0, zeros)
U41(tt, x0) → U42(isNatIList(x0))
U42(tt) → tt
U51(tt, x0) → U52(isNatList(x0))
U52(tt) → tt
U61(tt, x0, x1) → U62(isNat(x1), x0)
U62(tt, x0) → s(length(x0))
isNatIList(cons(x0, x1)) → U41(isNat(x0), x1)
isNatList(cons(x0, x1)) → U51(isNat(x0), x1)
length(cons(x0, x1)) → U61(isNatList(x1), x1, x0)
ISNATLIST(cons(V1, V2)) → U51'(isNat(V1), V2)
U51'(tt, V2) → ISNATLIST(V2)
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
ISNATLIST(cons(V1, V2)) → U51'(isNat(V1), V2)
U51'(tt, V2) → ISNATLIST(V2)
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
POL(0) = 2
POL(ISNATLIST(x1)) = 1 + 2·x1
POL(U21(x1)) = 1 + 2·x1
POL(U51'(x1, x2)) = 2 + 2·x1 + 2·x2
POL(cons(x1, x2)) = 2 + 2·x1 + 2·x2
POL(isNat(x1)) = 2·x1
POL(s(x1)) = 2 + 2·x1
POL(tt) = 2
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
LENGTH(cons(N, L)) → U61'(isNatList(L), L, N)
U61'(tt, L, N) → U62'(isNat(N), L)
U62'(tt, L) → LENGTH(L)
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
POL(0) = 2
POL(LENGTH(x1)) = 2
POL(U21(x1)) = x1
POL(U51(x1, x2)) = 0
POL(U52(x1)) = x1
POL(U61'(x1, x2, x3)) = 2 + 2·x1
POL(U62'(x1, x2)) = 2
POL(cons(x1, x2)) = 0
POL(isNat(x1)) = 2·x1
POL(isNatList(x1)) = 0
POL(s(x1)) = 1 + 2·x1
POL(tt) = 1
POL(zeros) = 0
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
zeros → cons(0, zeros)
U61'(tt, L, N) → U62'(isNat(N), L)
LENGTH(cons(N, L)) → U61'(isNatList(L), L, N)
U62'(tt, L) → LENGTH(L)
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
ISNATILIST(cons(V1, V2)) → U41'(isNat(V1), V2)
U41'(tt, V2) → ISNATILIST(V2)
zeros → cons(0, zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(cons(N, L)) → U61(isNatList(L), L, N)
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
zeros → cons(0, zeros)
U41(tt, x0) → U42(isNatIList(x0))
U42(tt) → tt
U51(tt, x0) → U52(isNatList(x0))
U52(tt) → tt
U61(tt, x0, x1) → U62(isNat(x1), x0)
U62(tt, x0) → s(length(x0))
isNatIList(cons(x0, x1)) → U41(isNat(x0), x1)
isNatList(cons(x0, x1)) → U51(isNat(x0), x1)
length(cons(x0, x1)) → U61(isNatList(x1), x1, x0)
ISNATILIST(cons(V1, V2)) → U41'(isNat(V1), V2)
U41'(tt, V2) → ISNATILIST(V2)
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
ISNATILIST(cons(V1, V2)) → U41'(isNat(V1), V2)
U41'(tt, V2) → ISNATILIST(V2)
isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
POL(0) = 2
POL(ISNATILIST(x1)) = 1 + 2·x1
POL(U21(x1)) = 1 + 2·x1
POL(U41'(x1, x2)) = 2 + 2·x1 + 2·x2
POL(cons(x1, x2)) = 2 + 2·x1 + 2·x2
POL(isNat(x1)) = 2·x1
POL(s(x1)) = 2 + 2·x1
POL(tt) = 2
zeros
U21(tt)
U41(tt, x0)
U42(tt)
U51(tt, x0)
U52(tt)
U61(tt, x0, x1)
U62(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))