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 (2780ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 | – Problem 3 was processed with processor SubtermCriterion (3ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (4810ms), DependencyGraph (26ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (5ms), ReductionPairSAT (8077ms), DependencyGraph (3ms), SizeChangePrinciple (timeout)].
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (3ms).
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).
 | – Problem 12 was processed with processor SubtermCriterion (1ms).

The following open problems remain:



Open Dependency Pair Problem 7

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, top, nil, cons


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2))proper#(X1)proper#(length(X))length#(proper(X))
top#(ok(X))top#(active(X))proper#(U11(X1, X2))proper#(X1)
U11#(ok(X1), ok(X2))U11#(X1, X2)cons#(ok(X1), ok(X2))cons#(X1, X2)
proper#(isNatIList(X))isNatIList#(proper(X))U11#(mark(X1), X2)U11#(X1, X2)
proper#(U11(X1, X2))U11#(proper(X1), proper(X2))proper#(and(X1, X2))and#(proper(X1), proper(X2))
active#(cons(X1, X2))cons#(active(X1), X2)active#(length(cons(N, L)))U11#(and(isNatList(L), isNat(N)), L)
proper#(U11(X1, X2))proper#(X2)active#(isNat(length(V1)))isNatList#(V1)
proper#(and(X1, X2))proper#(X2)length#(ok(X))length#(X)
active#(isNatList(cons(V1, V2)))isNatList#(V2)active#(U11(tt, L))s#(length(L))
active#(U11(X1, X2))active#(X1)top#(mark(X))proper#(X)
length#(mark(X))length#(X)top#(mark(X))top#(proper(X))
proper#(cons(X1, X2))proper#(X2)proper#(isNatIList(X))proper#(X)
active#(length(X))active#(X)isNat#(ok(X))isNat#(X)
and#(mark(X1), X2)and#(X1, X2)isNatList#(ok(X))isNatList#(X)
isNatIList#(ok(X))isNatIList#(X)active#(isNatIList(cons(V1, V2)))isNat#(V1)
active#(U11(tt, L))length#(L)proper#(s(X))proper#(X)
proper#(isNatList(X))isNatList#(proper(X))active#(isNatList(cons(V1, V2)))isNat#(V1)
active#(cons(X1, X2))active#(X1)cons#(mark(X1), X2)cons#(X1, X2)
active#(isNatIList(cons(V1, V2)))and#(isNat(V1), isNatIList(V2))and#(ok(X1), ok(X2))and#(X1, X2)
proper#(and(X1, X2))proper#(X1)top#(ok(X))active#(X)
active#(length(cons(N, L)))isNatList#(L)active#(and(X1, X2))and#(active(X1), X2)
active#(length(cons(N, L)))isNat#(N)proper#(isNatList(X))proper#(X)
proper#(isNat(X))isNat#(proper(X))active#(isNat(s(V1)))isNat#(V1)
active#(isNatIList(cons(V1, V2)))isNatIList#(V2)proper#(isNat(X))proper#(X)
active#(length(X))length#(active(X))active#(isNatList(cons(V1, V2)))and#(isNat(V1), isNatList(V2))
active#(length(cons(N, L)))and#(isNatList(L), isNat(N))active#(U11(X1, X2))U11#(active(X1), X2)
active#(s(X))s#(active(X))s#(ok(X))s#(X)
active#(isNatIList(V))isNatList#(V)s#(mark(X))s#(X)
proper#(length(X))proper#(X)proper#(cons(X1, X2))cons#(proper(X1), proper(X2))
active#(s(X))active#(X)proper#(s(X))s#(proper(X))
active#(zeros)cons#(0, zeros)active#(and(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


The following SCCs where found

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

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

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

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

active#(s(X)) → active#(X)active#(length(X)) → active#(X)
active#(and(X1, X2)) → active#(X1)active#(U11(X1, X2)) → active#(X1)
active#(cons(X1, X2)) → active#(X1)

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

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

proper#(length(X)) → proper#(X)proper#(s(X)) → proper#(X)
proper#(isNat(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(U11(X1, X2)) → proper#(X2)proper#(cons(X1, X2)) → proper#(X2)
proper#(and(X1, X2)) → proper#(X2)proper#(U11(X1, X2)) → proper#(X1)
proper#(isNatIList(X)) → proper#(X)proper#(isNatList(X)) → proper#(X)
proper#(and(X1, X2)) → proper#(X1)

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

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

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(s(X))active#(X)active#(length(X))active#(X)
active#(and(X1, X2))active#(X1)active#(U11(X1, X2))active#(X1)
active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(s(X))active#(X)active#(length(X))active#(X)
active#(and(X1, X2))active#(X1)active#(U11(X1, X2))active#(X1)
active#(cons(X1, X2))active#(X1)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 9: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(length(X))proper#(X)proper#(s(X))proper#(X)
proper#(isNat(X))proper#(X)proper#(cons(X1, X2))proper#(X1)
proper#(U11(X1, X2))proper#(X2)proper#(cons(X1, X2))proper#(X2)
proper#(and(X1, X2))proper#(X2)proper#(U11(X1, X2))proper#(X1)
proper#(isNatIList(X))proper#(X)proper#(isNatList(X))proper#(X)
proper#(and(X1, X2))proper#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(s(X))proper#(X)proper#(length(X))proper#(X)
proper#(cons(X1, X2))proper#(X1)proper#(isNat(X))proper#(X)
proper#(U11(X1, X2))proper#(X2)proper#(and(X1, X2))proper#(X2)
proper#(cons(X1, X2))proper#(X2)proper#(U11(X1, X2))proper#(X1)
proper#(isNatIList(X))proper#(X)proper#(isNatList(X))proper#(X)
proper#(and(X1, X2))proper#(X1)

Problem 11: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 12: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(isNatList(V1))active(isNat(s(V1)))mark(isNat(V1))
active(isNatIList(V))mark(isNatList(V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(and(isNat(V1), isNatList(V2)))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U11(and(isNatList(L), isNat(N)), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(s(X))s(proper(X))proper(length(X))length(proper(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(isNat(X))isNat(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))s(ok(X))ok(s(X))
length(ok(X))ok(length(X))and(ok(X1), ok(X2))ok(and(X1, X2))
isNat(ok(X))ok(isNat(X))isNatList(ok(X))ok(isNatList(X))
isNatIList(ok(X))ok(isNatIList(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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