TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60003 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (12965ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (3ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (4ms).
 | – Problem 9 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (8675ms), DependencyGraph (48ms), PolynomialLinearRange8NegiUR (30000ms), DependencyGraph (timeout), ReductionPairSAT (timeout)].
 | – Problem 10 was processed with processor SubtermCriterion (2ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).
 | – Problem 12 was processed with processor SubtermCriterion (4ms).
 | – Problem 13 was processed with processor SubtermCriterion (1ms).
 | – Problem 14 was processed with processor SubtermCriterion (1ms).
 | – Problem 15 was processed with processor SubtermCriterion (2ms).
 | – Problem 16 was processed with processor SubtermCriterion (3ms).
 | – Problem 17 was processed with processor SubtermCriterion (3ms).
 | – Problem 18 was processed with processor SubtermCriterion (4ms).
 | – Problem 19 was processed with processor SubtermCriterion (2ms).

The following open problems remain:



Open Dependency Pair Problem 9

Dependency Pairs

top#(mark(X))top#(proper(X))top#(ok(X))top#(active(X))

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, active, U11, ok, proper, U31, U21, top, nil, cons


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

proper#(U41(X1, X2))proper#(X2)proper#(cons(X1, X2))proper#(X1)
proper#(length(X))length#(proper(X))proper#(U41(X1, X2))proper#(X1)
active#(U51(X1, X2))active#(X1)proper#(U62(X1, X2))U62#(proper(X1), proper(X2))
active#(U41(tt, V2))isNatIList#(V2)proper#(U52(X))U52#(proper(X))
active#(U21(X))U21#(active(X))active#(U51(tt, V2))U52#(isNatList(V2))
active#(U51(tt, V2))isNatList#(V2)U51#(mark(X1), X2)U51#(X1, X2)
active#(isNat(length(V1)))isNatList#(V1)active#(U31(X))U31#(active(X))
proper#(U42(X))U42#(proper(X))active#(U42(X))U42#(active(X))
top#(mark(X))proper#(X)active#(U62(tt, L))length#(L)
length#(mark(X))length#(X)active#(U11(X))U11#(active(X))
proper#(U61(X1, X2, X3))U61#(proper(X1), proper(X2), proper(X3))active#(length(X))active#(X)
isNat#(ok(X))isNat#(X)isNatIList#(ok(X))isNatIList#(X)
active#(isNatIList(cons(V1, V2)))isNat#(V1)active#(U41(X1, X2))active#(X1)
proper#(U21(X))U21#(proper(X))active#(U61(tt, L, N))U62#(isNat(N), L)
proper#(U61(X1, X2, X3))proper#(X1)active#(U62(X1, X2))U62#(active(X1), X2)
active#(U61(X1, X2, X3))active#(X1)proper#(U62(X1, X2))proper#(X2)
cons#(mark(X1), X2)cons#(X1, X2)proper#(U62(X1, X2))proper#(X1)
proper#(U11(X))proper#(X)top#(ok(X))active#(X)
active#(isNat(length(V1)))U11#(isNatList(V1))U62#(ok(X1), ok(X2))U62#(X1, X2)
active#(U41(tt, V2))U42#(isNatIList(V2))active#(U52(X))active#(X)
proper#(isNatList(X))proper#(X)proper#(isNat(X))isNat#(proper(X))
proper#(U51(X1, X2))proper#(X2)U61#(mark(X1), X2, X3)U61#(X1, X2, X3)
U42#(ok(X))U42#(X)proper#(U21(X))proper#(X)
active#(isNat(s(V1)))isNat#(V1)U11#(mark(X))U11#(X)
U51#(ok(X1), ok(X2))U51#(X1, X2)active#(U52(X))U52#(active(X))
proper#(isNat(X))proper#(X)active#(U61(X1, X2, X3))U61#(active(X1), X2, X3)
active#(isNat(s(V1)))U21#(isNat(V1))active#(s(X))s#(active(X))
active#(isNatList(cons(V1, V2)))U51#(isNat(V1), V2)U31#(ok(X))U31#(X)
s#(ok(X))s#(X)proper#(length(X))proper#(X)
proper#(s(X))s#(proper(X))active#(zeros)cons#(0, zeros)
active#(isNatIList(V))U31#(isNatList(V))top#(ok(X))top#(active(X))
active#(isNatIList(cons(V1, V2)))U41#(isNat(V1), V2)proper#(isNatIList(X))isNatIList#(proper(X))
cons#(ok(X1), ok(X2))cons#(X1, X2)active#(cons(X1, X2))cons#(active(X1), X2)
U42#(mark(X))U42#(X)proper#(U51(X1, X2))U51#(proper(X1), proper(X2))
active#(U62(X1, X2))active#(X1)active#(U41(X1, X2))U41#(active(X1), X2)
active#(length(cons(N, L)))U61#(isNatList(L), L, N)active#(U51(X1, X2))U51#(active(X1), X2)
length#(ok(X))length#(X)U62#(mark(X1), X2)U62#(X1, X2)
U21#(ok(X))U21#(X)top#(mark(X))top#(proper(X))
active#(U31(X))active#(X)proper#(cons(X1, X2))proper#(X2)
proper#(isNatIList(X))proper#(X)active#(U61(tt, L, N))isNat#(N)
U52#(ok(X))U52#(X)proper#(U61(X1, X2, X3))proper#(X2)
isNatList#(ok(X))isNatList#(X)proper#(s(X))proper#(X)
proper#(isNatList(X))isNatList#(proper(X))active#(isNatList(cons(V1, V2)))isNat#(V1)
U31#(mark(X))U31#(X)active#(cons(X1, X2))active#(X1)
active#(U11(X))active#(X)active#(U42(X))active#(X)
proper#(U61(X1, X2, X3))proper#(X3)proper#(U31(X))U31#(proper(X))
proper#(U42(X))proper#(X)proper#(U51(X1, X2))proper#(X1)
active#(U21(X))active#(X)active#(length(cons(N, L)))isNatList#(L)
U41#(ok(X1), ok(X2))U41#(X1, X2)active#(U62(tt, L))s#(length(L))
proper#(U11(X))U11#(proper(X))U41#(mark(X1), X2)U41#(X1, X2)
active#(length(X))length#(active(X))U21#(mark(X))U21#(X)
U61#(ok(X1), ok(X2), ok(X3))U61#(X1, X2, X3)proper#(U41(X1, X2))U41#(proper(X1), proper(X2))
active#(isNatIList(V))isNatList#(V)s#(mark(X))s#(X)
proper#(cons(X1, X2))cons#(proper(X1), proper(X2))active#(s(X))active#(X)
U11#(ok(X))U11#(X)U52#(mark(X))U52#(X)
proper#(U52(X))proper#(X)proper#(U31(X))proper#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


The following SCCs where found

U41#(ok(X1), ok(X2)) → U41#(X1, X2)U41#(mark(X1), X2) → U41#(X1, X2)

U61#(ok(X1), ok(X2), ok(X3)) → U61#(X1, X2, X3)U61#(mark(X1), X2, X3) → U61#(X1, X2, X3)

U42#(mark(X)) → U42#(X)U42#(ok(X)) → U42#(X)

U31#(ok(X)) → U31#(X)U31#(mark(X)) → U31#(X)

isNat#(ok(X)) → isNat#(X)

U21#(ok(X)) → U21#(X)U21#(mark(X)) → U21#(X)

isNatList#(ok(X)) → isNatList#(X)

s#(mark(X)) → s#(X)s#(ok(X)) → s#(X)

isNatIList#(ok(X)) → isNatIList#(X)

cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)

length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)

proper#(U41(X1, X2)) → proper#(X2)proper#(cons(X1, X2)) → proper#(X1)
proper#(U62(X1, X2)) → proper#(X2)proper#(isNat(X)) → proper#(X)
proper#(U61(X1, X2, X3)) → proper#(X3)proper#(U41(X1, X2)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(isNatIList(X)) → proper#(X)
proper#(U62(X1, X2)) → proper#(X1)proper#(U11(X)) → proper#(X)
proper#(U61(X1, X2, X3)) → proper#(X2)proper#(U51(X1, X2)) → proper#(X1)
proper#(U42(X)) → proper#(X)proper#(length(X)) → proper#(X)
proper#(s(X)) → proper#(X)proper#(isNatList(X)) → proper#(X)
proper#(U61(X1, X2, X3)) → proper#(X1)proper#(U51(X1, X2)) → proper#(X2)
proper#(U21(X)) → proper#(X)proper#(U52(X)) → proper#(X)
proper#(U31(X)) → proper#(X)

U11#(ok(X)) → U11#(X)U11#(mark(X)) → U11#(X)

U52#(mark(X)) → U52#(X)U52#(ok(X)) → U52#(X)

active#(U62(X1, X2)) → active#(X1)active#(U61(X1, X2, X3)) → active#(X1)
active#(U11(X)) → active#(X)active#(U41(X1, X2)) → active#(X1)
active#(U42(X)) → active#(X)active#(U31(X)) → active#(X)
active#(U51(X1, X2)) → active#(X1)active#(s(X)) → active#(X)
active#(length(X)) → active#(X)active#(U52(X)) → active#(X)
active#(U21(X)) → active#(X)active#(cons(X1, X2)) → active#(X1)

top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

U62#(ok(X1), ok(X2)) → U62#(X1, X2)U62#(mark(X1), X2) → U62#(X1, X2)

U51#(mark(X1), X2) → U51#(X1, X2)U51#(ok(X1), ok(X2)) → U51#(X1, X2)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U51#(mark(X1), X2)U51#(X1, X2)U51#(ok(X1), ok(X2))U51#(X1, X2)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U51#(ok(X1), ok(X2))U51#(X1, X2)U51#(mark(X1), X2)U51#(X1, X2)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U52#(mark(X))U52#(X)U52#(ok(X))U52#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U52#(mark(X))U52#(X)U52#(ok(X))U52#(X)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U31#(ok(X))U31#(X)U31#(mark(X))U31#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U31#(ok(X))U31#(X)U31#(mark(X))U31#(X)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatIList#(ok(X))isNatIList#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatIList#(ok(X))isNatIList#(X)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNat#(ok(X))isNat#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNat#(ok(X))isNat#(X)

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

cons#(mark(X1), X2)cons#(X1, X2)cons#(ok(X1), ok(X2))cons#(X1, X2)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

cons#(mark(X1), X2)cons#(X1, X2)cons#(ok(X1), ok(X2))cons#(X1, X2)

Problem 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U62#(ok(X1), ok(X2))U62#(X1, X2)U62#(mark(X1), X2)U62#(X1, X2)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U62#(ok(X1), ok(X2))U62#(X1, X2)U62#(mark(X1), X2)U62#(X1, X2)

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

length#(mark(X))length#(X)length#(ok(X))length#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

length#(mark(X))length#(X)length#(ok(X))length#(X)

Problem 11: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U11#(ok(X))U11#(X)U11#(mark(X))U11#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U11#(ok(X))U11#(X)U11#(mark(X))U11#(X)

Problem 12: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U41#(ok(X1), ok(X2))U41#(X1, X2)U41#(mark(X1), X2)U41#(X1, X2)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U41#(ok(X1), ok(X2))U41#(X1, X2)U41#(mark(X1), X2)U41#(X1, X2)

Problem 13: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U42#(mark(X))U42#(X)U42#(ok(X))U42#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U42#(mark(X))U42#(X)U42#(ok(X))U42#(X)

Problem 14: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U61#(ok(X1), ok(X2), ok(X3))U61#(X1, X2, X3)U61#(mark(X1), X2, X3)U61#(X1, X2, X3)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U61#(ok(X1), ok(X2), ok(X3))U61#(X1, X2, X3)U61#(mark(X1), X2, X3)U61#(X1, X2, X3)

Problem 15: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatList#(ok(X))isNatList#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatList#(ok(X))isNatList#(X)

Problem 16: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(U41(X1, X2))proper#(X2)proper#(isNat(X))proper#(X)
proper#(U62(X1, X2))proper#(X2)proper#(cons(X1, X2))proper#(X1)
proper#(U41(X1, X2))proper#(X1)proper#(U61(X1, X2, X3))proper#(X3)
proper#(cons(X1, X2))proper#(X2)proper#(isNatIList(X))proper#(X)
proper#(U62(X1, X2))proper#(X1)proper#(U11(X))proper#(X)
proper#(U61(X1, X2, X3))proper#(X2)proper#(U42(X))proper#(X)
proper#(U51(X1, X2))proper#(X1)proper#(length(X))proper#(X)
proper#(s(X))proper#(X)proper#(isNatList(X))proper#(X)
proper#(U61(X1, X2, X3))proper#(X1)proper#(U51(X1, X2))proper#(X2)
proper#(U21(X))proper#(X)proper#(U52(X))proper#(X)
proper#(U31(X))proper#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(U41(X1, X2))proper#(X2)proper#(isNat(X))proper#(X)
proper#(U62(X1, X2))proper#(X2)proper#(cons(X1, X2))proper#(X1)
proper#(U41(X1, X2))proper#(X1)proper#(U61(X1, X2, X3))proper#(X3)
proper#(cons(X1, X2))proper#(X2)proper#(isNatIList(X))proper#(X)
proper#(U62(X1, X2))proper#(X1)proper#(U11(X))proper#(X)
proper#(U61(X1, X2, X3))proper#(X2)proper#(U42(X))proper#(X)
proper#(U51(X1, X2))proper#(X1)proper#(length(X))proper#(X)
proper#(s(X))proper#(X)proper#(isNatList(X))proper#(X)
proper#(U61(X1, X2, X3))proper#(X1)proper#(U51(X1, X2))proper#(X2)
proper#(U21(X))proper#(X)proper#(U52(X))proper#(X)
proper#(U31(X))proper#(X)

Problem 17: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

s#(mark(X))s#(X)s#(ok(X))s#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X))s#(X)s#(ok(X))s#(X)

Problem 18: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(U62(X1, X2))active#(X1)active#(U61(X1, X2, X3))active#(X1)
active#(U41(X1, X2))active#(X1)active#(U11(X))active#(X)
active#(U42(X))active#(X)active#(U31(X))active#(X)
active#(U51(X1, X2))active#(X1)active#(s(X))active#(X)
active#(U52(X))active#(X)active#(length(X))active#(X)
active#(U21(X))active#(X)active#(cons(X1, X2))active#(X1)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(U61(X1, X2, X3))active#(X1)active#(U62(X1, X2))active#(X1)
active#(U41(X1, X2))active#(X1)active#(U11(X))active#(X)
active#(U31(X))active#(X)active#(U42(X))active#(X)
active#(U51(X1, X2))active#(X1)active#(s(X))active#(X)
active#(U52(X))active#(X)active#(length(X))active#(X)
active#(U21(X))active#(X)active#(cons(X1, X2))active#(X1)

Problem 19: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U21#(ok(X))U21#(X)U21#(mark(X))U21#(X)

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

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, isNat, U62, U61, 0, s, U51, U42, isNatList, zeros, tt, U41, U52, length, U11, active, ok, U31, proper, U21, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U21#(ok(X))U21#(X)U21#(mark(X))U21#(X)