Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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))

Q is empty.

(1) QTRSToCSRProof (EQUIVALENT transformation)

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

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))

Q is empty.
Special symbols used for the transformation (see [GM04]):
top: top, active: active, mark: mark, ok: ok, proper: proper
The replacement map contains the following entries:

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).

(2) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

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

(3) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x₁)) = x₁   
POL(U21(x₁)) = 2·x₁   
POL(U31(x₁)) = x₁   
POL(U41(x₁, x₂)) = 2 + x₁ + x₂   
POL(U42(x₁)) = x₁   
POL(U51(x₁, x₂)) = 2·x₁   
POL(U52(x₁)) = x₁   
POL(U61(x₁, x₂, x₃)) = 2·x₁ + 2·x₂ + 2·x₃   
POL(U62(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(isNat(x₁)) = 0   
POL(isNatIList(x₁)) = 2 + x₁   
POL(isNatList(x₁)) = 0   
POL(length(x₁)) = x₁   
POL(nil) = 0   
POL(s(x₁)) = 2·x₁   
POL(tt) = 0   
POL(zeros) = 0   

(4) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

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

(5) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U31(tt) → tt

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x₁)) = x₁   
POL(U21(x₁)) = 2·x₁   
POL(U31(x₁)) = 2 + 2·x₁   
POL(U41(x₁, x₂)) = 2·x₁ + x₂   
POL(U42(x₁)) = x₁   
POL(U51(x₁, x₂)) = 2·x₁   
POL(U52(x₁)) = 2·x₁   
POL(U61(x₁, x₂, x₃)) = 2·x₁ + x₂ + x₃   
POL(U62(x₁, x₂)) = 2·x₁ + x₂   
POL(cons(x₁, x₂)) = x₁ + 2·x₂   
POL(isNat(x₁)) = 0   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = 0   
POL(length(x₁)) = x₁   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(tt) = 0   
POL(zeros) = 0   

(6) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

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

(7) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

length(nil) → 0

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x₁)) = 2·x₁   
POL(U21(x₁)) = 2·x₁   
POL(U41(x₁, x₂)) = 2·x₁   
POL(U42(x₁)) = 2·x₁   
POL(U51(x₁, x₂)) = 2·x₁   
POL(U52(x₁)) = 2·x₁   
POL(U61(x₁, x₂, x₃)) = 2·x₁ + 2·x₂   
POL(U62(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(isNat(x₁)) = 0   
POL(isNatIList(x₁)) = 0   
POL(isNatList(x₁)) = 0   
POL(length(x₁)) = x₁   
POL(nil) = 1   
POL(s(x₁)) = 2·x₁   
POL(tt) = 0   
POL(zeros) = 0   

(8) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

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

(9) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U11(tt) → tt
isNat(length(V1)) → U11(isNatList(V1))

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x₁)) = 1 + x₁   
POL(U21(x₁)) = x₁   
POL(U41(x₁, x₂)) = x₁ + 2·x₂   
POL(U42(x₁)) = 2·x₁   
POL(U51(x₁, x₂)) = x₁ + 2·x₂   
POL(U52(x₁)) = x₁   
POL(U61(x₁, x₂, x₃)) = 1 + x₁ + 2·x₂ + 2·x₃   
POL(U62(x₁, x₂)) = 1 + x₁ + 2·x₂   
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(isNat(x₁)) = 2·x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = 1 + 2·x₁   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(tt) = 0   
POL(zeros) = 0   

(10) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

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

(11) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

isNatList(nil) → tt

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U21(x₁)) = x₁   
POL(U41(x₁, x₂)) = x₁ + 2·x₂   
POL(U42(x₁)) = 2·x₁   
POL(U51(x₁, x₂)) = x₁ + 2·x₂   
POL(U52(x₁)) = x₁   
POL(U61(x₁, x₂, x₃)) = x₁ + 2·x₂ + x₃   
POL(U62(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(isNat(x₁)) = 0   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = 2·x₁   
POL(length(x₁)) = 2·x₁   
POL(nil) = 2   
POL(s(x₁)) = x₁   
POL(tt) = 0   
POL(zeros) = 0   

(12) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

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}

(13) CSRInnermostProof (EQUIVALENT transformation)

The CSR is orthogonal. By [CS_Inn] we can switch to innermost.

(14) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

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.

(15) CSDependencyPairsProof (EQUIVALENT transformation)

Using Improved CS-DPs [LPAR08] we result in the following initial Q-CSDP problem.

(16) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length, U42', U52', LENGTH, U21'} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U41', U51', U62', U61'} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATILIST, ISNATLIST, ISNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

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)

The collapsing dependency pairs are DP_c:

U62'(tt, L) → L

The hidden terms of R are:

zeros

Every hiding context is built from:none

Hence, the new unhiding pairs DP_u are :

U62'(tt, L) → U(L)
U(zeros) → ZEROS

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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))

(17) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 4 SCCs with 9 less nodes.

(18) Complex Obligation (AND)

(19) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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))

(20) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].

The following pairs can be oriented strictly and are deleted.

ISNAT(s(V1)) → ISNAT(V1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
ISNAT(x1)  =  x1

Subterm Order

(21) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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))

(22) PIsEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

(23) TRUE

(24) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U51'} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U51'(isNat(V1), V2)
U51'(tt, V2) → ISNATLIST(V2)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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))

(25) QCSUsableRulesProof (EQUIVALENT transformation)

The following rules are not useable [DA_EMMES] and can be deleted:

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)

(26) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, U21, U42, U52, length} are replacing on all positions.
For all symbols f in {cons, U51', U41, U51, U61, U62} we have µ(f) = {1}.
The symbols in {isNat, ISNATLIST, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U51'(isNat(V1), V2)
U51'(tt, V2) → ISNATLIST(V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt

The set Q consists of the following terms:

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))

(27) QCSDPMuMonotonicPoloProof (EQUIVALENT transformation)

By using the following µ-monotonic polynomial ordering [POLO], at least one Dependency Pair or term rewrite system rule of this Q-CSDP problem can be strictly oriented and thus deleted.
Strictly oriented dependency pairs:

ISNATLIST(cons(V1, V2)) → U51'(isNat(V1), V2)
U51'(tt, V2) → ISNATLIST(V2)

Strictly oriented rules of the TRS R:

isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 2   
POL(ISNATLIST(x₁)) = 1 + 2·x₁   
POL(U21(x₁)) = 1 + 2·x₁   
POL(U51'(x₁, x₂)) = 2 + 2·x₁ + 2·x₂   
POL(cons(x₁, x₂)) = 2 + 2·x₁ + 2·x₂   
POL(isNat(x₁)) = 2·x₁   
POL(s(x₁)) = 2 + 2·x₁   
POL(tt) = 2   

(28) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length} are replacing on all positions.
For all symbols f in {U41, U51, U61, U62, cons} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:
none

R is empty.
The set Q consists of the following terms:

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))

(29) PIsEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

(30) TRUE

(31) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U61', U62'} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U61'(isNatList(L), L, N)
U61'(tt, L, N) → U62'(isNat(N), L)
U62'(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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))

(32) QCSDPReductionPairProof (EQUIVALENT transformation)

Using the order
Polynomial interpretation [POLO]:

POL(0) = 2   
POL(LENGTH(x₁)) = 2   
POL(U21(x₁)) = x₁   
POL(U51(x₁, x₂)) = 0   
POL(U52(x₁)) = x₁   
POL(U61'(x₁, x₂, x₃)) = 2 + 2·x₁   
POL(U62'(x₁, x₂)) = 2   
POL(cons(x₁, x₂)) = 0   
POL(isNat(x₁)) = 2·x₁   
POL(isNatList(x₁)) = 0   
POL(s(x₁)) = 1 + 2·x₁   
POL(tt) = 1   
POL(zeros) = 0   

the following usable rules

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)

could all be oriented weakly.
Furthermore, the pairs

U61'(tt, L, N) → U62'(isNat(N), L)

could be oriented strictly and thus removed by the CS-Reduction Pair Processor [LPAR08,DA_EMMES].

(33) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U61', U62'} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U61'(isNatList(L), L, N)
U62'(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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))

(34) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 0 SCCs with 2 less nodes.

(35) TRUE

(36) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U41'} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U41'(isNat(V1), V2)
U41'(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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))

(37) QCSUsableRulesProof (EQUIVALENT transformation)

The following rules are not useable [DA_EMMES] and can be deleted:

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)

(38) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, U21, U42, U52, length} are replacing on all positions.
For all symbols f in {cons, U41', U41, U51, U61, U62} we have µ(f) = {1}.
The symbols in {isNat, ISNATILIST, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U41'(isNat(V1), V2)
U41'(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt

The set Q consists of the following terms:

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))

(39) QCSDPMuMonotonicPoloProof (EQUIVALENT transformation)

By using the following µ-monotonic polynomial ordering [POLO], at least one Dependency Pair or term rewrite system rule of this Q-CSDP problem can be strictly oriented and thus deleted.
Strictly oriented dependency pairs:

ISNATILIST(cons(V1, V2)) → U41'(isNat(V1), V2)
U41'(tt, V2) → ISNATILIST(V2)

Strictly oriented rules of the TRS R:

isNat(0) → tt
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 2   
POL(ISNATILIST(x₁)) = 1 + 2·x₁   
POL(U21(x₁)) = 1 + 2·x₁   
POL(U41'(x₁, x₂)) = 2 + 2·x₁ + 2·x₂   
POL(cons(x₁, x₂)) = 2 + 2·x₁ + 2·x₂   
POL(isNat(x₁)) = 2·x₁   
POL(s(x₁)) = 2 + 2·x₁   
POL(tt) = 2   

(40) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U21, U42, U52, s, length} are replacing on all positions.
For all symbols f in {U41, U51, U61, U62, cons} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:
none

R is empty.
The set Q consists of the following terms:

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))

(41) PIsEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

(42) TRUE