TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (20944ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 24 remains open; application of the following processors failed [DependencyGraph (16ms), PolynomialLinearRange4iUR (5ms)].
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 25 remains open; application of the following processors failed [DependencyGraph (6ms), PolynomialLinearRange4iUR (10ms)].
 | – Problem 4 was processed with processor DependencyGraph (3984ms).
 |    | – Problem 30 remains open; application of the following processors failed [PolynomialLinearRange4iUR (8ms)].
 | – Problem 5 was processed with processor SubtermCriterion (4ms).
 | – Problem 6 was processed with processor DependencyGraph (4106ms).
 |    | – Problem 31 remains open; application of the following processors failed [PolynomialLinearRange4iUR (7ms)].
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor DependencyGraph (3983ms).
 |    | – Problem 32 remains open; application of the following processors failed [PolynomialLinearRange4iUR (25ms), DependencyGraph (3871ms)].
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 | – Problem 11 was processed with processor DependencyGraph (3991ms).
 |    | – Problem 33 remains open; application of the following processors failed [PolynomialLinearRange4iUR (23ms), DependencyGraph (timeout)].
 | – Problem 12 was processed with processor SubtermCriterion (3ms).
 | – Problem 13 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3827ms), PolynomialLinearRange4iUR (7ms)].
 | – Problem 14 was processed with processor DependencyGraph (3975ms).
 |    | – Problem 34 remains open; application of the following processors failed [PolynomialLinearRange4iUR (833ms), DependencyGraph (3964ms)].
 | – Problem 15 was processed with processor SubtermCriterion (1ms).
 | – Problem 16 was processed with processor SubtermCriterion (2ms).
 | – Problem 17 was processed with processor DependencyGraph (4098ms).
 |    | – Problem 29 remains open; application of the following processors failed [PolynomialLinearRange4iUR (8ms)].
 | – Problem 18 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 26 remains open; application of the following processors failed [DependencyGraph (6ms), PolynomialLinearRange4iUR (7ms)].
 | – Problem 19 was processed with processor SubtermCriterion (1ms).
 | – Problem 20 was processed with processor SubtermCriterion (1ms).
 | – Problem 21 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 27 remains open; application of the following processors failed [DependencyGraph (6ms), PolynomialLinearRange4iUR (1ms)].
 | – Problem 22 was processed with processor SubtermCriterion (1ms).
 | – Problem 23 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 28 remains open; application of the following processors failed [DependencyGraph (44ms), PolynomialLinearRange4iUR (5ms)].

The following open problems remain:



Open Dependency Pair Problem 34

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, nil, cons




Open Dependency Pair Problem 32

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, nil, cons




Open Dependency Pair Problem 33

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, nil, cons




Open Dependency Pair Problem 25

Dependency Pairs

cons#(X1, active(X2))cons#(X1, X2)cons#(X1, mark(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil




Open Dependency Pair Problem 24

Dependency Pairs

U61#(X1, X2, active(X3))U61#(X1, X2, X3)U61#(X1, X2, mark(X3))U61#(X1, X2, X3)
U61#(X1, mark(X2), X3)U61#(X1, X2, X3)U61#(X1, active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil




Open Dependency Pair Problem 27

Dependency Pairs

U62#(X1, active(X2))U62#(X1, X2)U62#(X1, mark(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil




Open Dependency Pair Problem 26

Dependency Pairs

U51#(X1, mark(X2))U51#(X1, X2)U51#(X1, active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil




Open Dependency Pair Problem 29

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, nil, cons




Open Dependency Pair Problem 28

Dependency Pairs

U41#(X1, mark(X2))U41#(X1, X2)U41#(X1, active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil




Open Dependency Pair Problem 13

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, nil, cons




Open Dependency Pair Problem 31

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, nil, cons




Open Dependency Pair Problem 30

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, nil, cons


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

U62#(X1, active(X2))U62#(X1, X2)mark#(U51(X1, X2))U51#(mark(X1), X2)
active#(U41(tt, V2))isNatIList#(V2)active#(length(nil))mark#(0)
U62#(active(X1), X2)U62#(X1, X2)active#(U51(tt, V2))U52#(isNatList(V2))
active#(U51(tt, V2))isNatList#(V2)U61#(X1, active(X2), X3)U61#(X1, X2, X3)
U61#(X1, X2, mark(X3))U61#(X1, X2, X3)U51#(mark(X1), X2)U51#(X1, X2)
active#(isNat(length(V1)))isNatList#(V1)isNat#(active(X))isNat#(X)
mark#(s(X))mark#(X)mark#(U42(X))U42#(mark(X))
active#(U62(tt, L))length#(L)length#(mark(X))length#(X)
U62#(X1, mark(X2))U62#(X1, X2)mark#(cons(X1, X2))mark#(X1)
mark#(U51(X1, X2))active#(U51(mark(X1), X2))mark#(U52(X))mark#(X)
U41#(active(X1), X2)U41#(X1, X2)active#(isNatIList(cons(V1, V2)))isNat#(V1)
active#(U31(tt))mark#(tt)mark#(U42(X))active#(U42(mark(X)))
active#(length(cons(N, L)))mark#(U61(isNatList(L), L, N))mark#(U31(X))mark#(X)
active#(U61(tt, L, N))U62#(isNat(N), L)active#(U42(tt))mark#(tt)
mark#(U62(X1, X2))active#(U62(mark(X1), X2))U51#(X1, active(X2))U51#(X1, X2)
U61#(active(X1), X2, X3)U61#(X1, X2, X3)cons#(mark(X1), X2)cons#(X1, X2)
mark#(tt)active#(tt)mark#(U11(X))mark#(X)
mark#(U62(X1, X2))mark#(X1)mark#(U21(X))mark#(X)
mark#(U52(X))active#(U52(mark(X)))active#(isNat(length(V1)))U11#(isNatList(V1))
active#(U41(tt, V2))U42#(isNatIList(V2))mark#(length(X))mark#(X)
active#(isNatList(cons(V1, V2)))mark#(U51(isNat(V1), V2))cons#(X1, mark(X2))cons#(X1, X2)
mark#(U41(X1, X2))mark#(X1)mark#(U11(X))active#(U11(mark(X)))
U41#(X1, active(X2))U41#(X1, X2)mark#(zeros)active#(zeros)
U61#(mark(X1), X2, X3)U61#(X1, X2, X3)active#(isNat(s(V1)))isNat#(V1)
U11#(mark(X))U11#(X)mark#(0)active#(0)
active#(isNatIList(cons(V1, V2)))mark#(U41(isNat(V1), V2))mark#(s(X))active#(s(mark(X)))
active#(isNat(s(V1)))U21#(isNat(V1))mark#(U61(X1, X2, X3))U61#(mark(X1), X2, X3)
cons#(active(X1), X2)cons#(X1, X2)active#(isNatList(cons(V1, V2)))U51#(isNat(V1), V2)
U51#(X1, mark(X2))U51#(X1, X2)isNatList#(mark(X))isNatList#(X)
mark#(isNatList(X))isNatList#(X)active#(zeros)cons#(0, zeros)
mark#(U31(X))U31#(mark(X))active#(isNatIList(V))U31#(isNatList(V))
mark#(U21(X))U21#(mark(X))active#(U61(tt, L, N))mark#(U62(isNat(N), L))
mark#(cons(X1, X2))active#(cons(mark(X1), X2))mark#(U21(X))active#(U21(mark(X)))
U11#(active(X))U11#(X)active#(U21(tt))mark#(tt)
active#(U41(tt, V2))mark#(U42(isNatIList(V2)))active#(isNatIList(cons(V1, V2)))U41#(isNat(V1), V2)
active#(isNat(length(V1)))mark#(U11(isNatList(V1)))U42#(active(X))U42#(X)
mark#(s(X))s#(mark(X))mark#(U41(X1, X2))active#(U41(mark(X1), X2))
U42#(mark(X))U42#(X)mark#(U52(X))U52#(mark(X))
length#(active(X))length#(X)U52#(active(X))U52#(X)
active#(length(cons(N, L)))U61#(isNatList(L), L, N)active#(isNatIList(V))mark#(U31(isNatList(V)))
U62#(mark(X1), X2)U62#(X1, X2)mark#(isNatIList(X))active#(isNatIList(X))
U61#(X1, mark(X2), X3)U61#(X1, X2, X3)isNatList#(active(X))isNatList#(X)
U41#(X1, mark(X2))U41#(X1, X2)isNatIList#(active(X))isNatIList#(X)
active#(isNat(0))mark#(tt)active#(U61(tt, L, N))isNat#(N)
isNatIList#(mark(X))isNatIList#(X)mark#(isNatIList(X))isNatIList#(X)
mark#(U41(X1, X2))U41#(mark(X1), X2)cons#(X1, active(X2))cons#(X1, X2)
active#(U62(tt, L))mark#(s(length(L)))active#(U52(tt))mark#(tt)
active#(isNatList(cons(V1, V2)))isNat#(V1)U31#(mark(X))U31#(X)
mark#(U62(X1, X2))U62#(mark(X1), X2)mark#(isNat(X))active#(isNat(X))
mark#(U11(X))U11#(mark(X))mark#(U61(X1, X2, X3))active#(U61(mark(X1), X2, X3))
mark#(U61(X1, X2, X3))mark#(X1)mark#(U42(X))mark#(X)
U51#(active(X1), X2)U51#(X1, X2)mark#(isNat(X))isNat#(X)
isNat#(mark(X))isNat#(X)mark#(U51(X1, X2))mark#(X1)
active#(U11(tt))mark#(tt)active#(length(cons(N, L)))isNatList#(L)
active#(isNatList(nil))mark#(tt)mark#(nil)active#(nil)
active#(U62(tt, L))s#(length(L))active#(isNatIList(zeros))mark#(tt)
U41#(mark(X1), X2)U41#(X1, X2)mark#(cons(X1, X2))cons#(mark(X1), X2)
mark#(length(X))length#(mark(X))U31#(active(X))U31#(X)
U21#(mark(X))U21#(X)U21#(active(X))U21#(X)
mark#(U31(X))active#(U31(mark(X)))active#(isNat(s(V1)))mark#(U21(isNat(V1)))
active#(isNatIList(V))isNatList#(V)U61#(X1, X2, active(X3))U61#(X1, X2, X3)
s#(mark(X))s#(X)U52#(mark(X))U52#(X)
active#(zeros)mark#(cons(0, zeros))s#(active(X))s#(X)
active#(U51(tt, V2))mark#(U52(isNatList(V2)))mark#(length(X))active#(length(mark(X)))
mark#(isNatList(X))active#(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


The following SCCs where found

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

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

isNatIList#(active(X)) → isNatIList#(X)isNatIList#(mark(X)) → isNatIList#(X)

length#(mark(X)) → length#(X)length#(active(X)) → length#(X)

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

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

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

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

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

isNat#(active(X)) → isNat#(X)isNat#(mark(X)) → isNat#(X)

U42#(mark(X)) → U42#(X)U42#(active(X)) → U42#(X)

U52#(active(X)) → U52#(X)U52#(mark(X)) → U52#(X)

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

U11#(active(X)) → U11#(X)U11#(mark(X)) → U11#(X)

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

isNatList#(mark(X)) → isNatList#(X)isNatList#(active(X)) → isNatList#(X)

U31#(active(X)) → U31#(X)U31#(mark(X)) → U31#(X)

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

s#(mark(X)) → s#(X)s#(active(X)) → s#(X)

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

U21#(mark(X)) → U21#(X)U21#(active(X)) → U21#(X)

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U61#(X1, X2, active(X3))U61#(X1, X2, X3)U61#(X1, X2, mark(X3))U61#(X1, X2, X3)
U61#(active(X1), X2, X3)U61#(X1, X2, X3)U61#(mark(X1), X2, X3)U61#(X1, X2, X3)
U61#(X1, mark(X2), X3)U61#(X1, X2, X3)U61#(X1, active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2))cons#(X1, X2)cons#(mark(X1), X2)cons#(X1, X2)
cons#(active(X1), X2)cons#(X1, X2)cons#(X1, mark(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


The following SCCs where found

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

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatIList#(active(X))isNatIList#(X)isNatIList#(mark(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatIList#(active(X))isNatIList#(X)isNatIList#(mark(X))isNatIList#(X)

Problem 6: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


The following SCCs where found

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

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatList#(mark(X))isNatList#(X)isNatList#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatList#(mark(X))isNatList#(X)isNatList#(active(X))isNatList#(X)

Problem 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U11#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U11#(active(X))U11#(X)U11#(mark(X))U11#(X)

Problem 9: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


The following SCCs where found

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

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U21#(mark(X))U21#(X)U21#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U21#(mark(X))U21#(X)U21#(active(X))U21#(X)

Problem 11: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


The following SCCs where found

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

Problem 12: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

s#(mark(X))s#(X)s#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X))s#(X)s#(active(X))s#(X)

Problem 14: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


The following SCCs where found

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

Problem 15: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U42#(mark(X))U42#(X)U42#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U42#(mark(X))U42#(X)U42#(active(X))U42#(X)

Problem 16: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U31#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U31#(active(X))U31#(X)U31#(mark(X))U31#(X)

Problem 17: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


The following SCCs where found

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

Problem 18: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U51#(X1, mark(X2))U51#(X1, X2)U51#(mark(X1), X2)U51#(X1, X2)
U51#(X1, active(X2))U51#(X1, X2)U51#(active(X1), 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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 19: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNat#(active(X))isNat#(X)isNat#(mark(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNat#(active(X))isNat#(X)isNat#(mark(X))isNat#(X)

Problem 20: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

length#(mark(X))length#(X)length#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

length#(mark(X))length#(X)length#(active(X))length#(X)

Problem 21: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U62#(X1, active(X2))U62#(X1, X2)U62#(X1, mark(X2))U62#(X1, X2)
U62#(active(X1), 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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 22: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U52#(active(X))U52#(X)U52#(mark(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U52#(active(X))U52#(X)U52#(mark(X))U52#(X)

Problem 23: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U41#(X1, mark(X2))U41#(X1, X2)U41#(X1, active(X2))U41#(X1, X2)
U41#(mark(X1), X2)U41#(X1, X2)U41#(active(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))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X))active(U11(mark(X)))
mark(tt)active(tt)mark(U21(X))active(U21(mark(X)))
mark(U31(X))active(U31(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U42(X))active(U42(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(nil)active(nil)cons(mark(X1), X2)cons(X1, X2)
cons(X1, mark(X2))cons(X1, X2)cons(active(X1), X2)cons(X1, X2)
cons(X1, active(X2))cons(X1, X2)U11(mark(X))U11(X)
U11(active(X))U11(X)U21(mark(X))U21(X)
U21(active(X))U21(X)U31(mark(X))U31(X)
U31(active(X))U31(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U42(mark(X))U42(X)
U42(active(X))U42(X)isNatIList(mark(X))isNatIList(X)
isNatIList(active(X))isNatIList(X)U51(mark(X1), X2)U51(X1, X2)
U51(X1, mark(X2))U51(X1, X2)U51(active(X1), X2)U51(X1, X2)
U51(X1, active(X2))U51(X1, X2)U52(mark(X))U52(X)
U52(active(X))U52(X)isNatList(mark(X))isNatList(X)
isNatList(active(X))isNatList(X)U61(mark(X1), X2, X3)U61(X1, X2, X3)
U61(X1, mark(X2), X3)U61(X1, X2, X3)U61(X1, X2, mark(X3))U61(X1, X2, X3)
U61(active(X1), X2, X3)U61(X1, X2, X3)U61(X1, active(X2), X3)U61(X1, X2, X3)
U61(X1, X2, active(X3))U61(X1, X2, X3)U62(mark(X1), X2)U62(X1, X2)
U62(X1, mark(X2))U62(X1, X2)U62(active(X1), X2)U62(X1, X2)
U62(X1, active(X2))U62(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)s(mark(X))s(X)
s(active(X))s(X)length(mark(X))length(X)
length(active(X))length(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, U31, U21, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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