TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (4956ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (688ms), PolynomialLinearRange4iUR (2500ms), DependencyGraph (659ms), PolynomialLinearRange8NegiUR (7500ms), DependencyGraph (703ms), ReductionPairSAT (13059ms), DependencyGraph (686ms), ReductionPairSAT (12692ms), DependencyGraph (687ms), ReductionPairSAT (12840ms), DependencyGraph (660ms), SizeChangePrinciple (timeout)].
 | – 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 11 was processed with processor ReductionPairSAT (132ms).
 |    |    | – Problem 14 was processed with processor ReductionPairSAT (25ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 12 was processed with processor ReductionPairSAT (114ms).
 |    |    | – Problem 15 was processed with processor ReductionPairSAT (66ms).
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 13 was processed with processor ReductionPairSAT (34ms).
 |    |    | – Problem 16 was processed with processor ReductionPairSAT (24ms).

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

mark#(U11(X1, X2)) → mark#(X1)mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(isNat(X)) → active#(isNat(X))mark#(tt) → active#(tt)
active#(length(nil)) → mark#(0)active#(isNatList(nil)) → mark#(tt)
active#(isNat(s(V1))) → mark#(isNat(V1))mark#(nil) → active#(nil)
active#(isNatIList(V)) → mark#(isNatList(V))mark#(and(X1, X2)) → active#(and(mark(X1), X2))
mark#(length(X)) → mark#(X)mark#(s(X)) → mark#(X)
active#(isNatIList(zeros)) → mark#(tt)mark#(U11(X1, X2)) → active#(U11(mark(X1), X2))
mark#(zeros) → active#(zeros)mark#(isNatIList(X)) → active#(isNatIList(X))
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
active#(isNatIList(cons(V1, V2))) → mark#(and(isNat(V1), isNatIList(V2)))active#(isNat(0)) → mark#(tt)
active#(U11(tt, L)) → mark#(s(length(L)))mark#(cons(X1, X2)) → mark#(X1)
active#(and(tt, X)) → mark#(X)mark#(and(X1, X2)) → mark#(X1)
active#(isNatList(cons(V1, V2))) → mark#(and(isNat(V1), isNatList(V2)))active#(isNat(length(V1))) → mark#(isNatList(V1))
active#(zeros) → mark#(cons(0, zeros))active#(length(cons(N, L))) → mark#(U11(and(isNatList(L), isNat(N)), L))
mark#(isNatList(X)) → active#(isNatList(X))mark#(length(X)) → active#(length(mark(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(U11(X1, X2)) → mark#(X1)
active#(length(nil)) → mark#(0)U11#(mark(X1), X2) → U11#(X1, X2)
mark#(s(X)) → s#(mark(X))active#(isNat(s(V1))) → mark#(isNat(V1))
active#(length(cons(N, L))) → U11#(and(isNatList(L), isNat(N)), L)active#(isNat(length(V1))) → isNatList#(V1)
length#(active(X)) → length#(X)active#(isNatIList(V)) → mark#(isNatList(V))
isNat#(active(X)) → isNat#(X)mark#(s(X)) → mark#(X)
mark#(U11(X1, X2)) → active#(U11(mark(X1), X2))active#(U11(tt, L)) → s#(length(L))
active#(isNatList(cons(V1, V2))) → isNatList#(V2)mark#(isNatIList(X)) → active#(isNatIList(X))
isNatList#(active(X)) → isNatList#(X)length#(mark(X)) → length#(X)
U11#(active(X1), X2) → U11#(X1, X2)active#(isNatIList(cons(V1, V2))) → mark#(and(isNat(V1), isNatIList(V2)))
mark#(and(X1, X2)) → and#(mark(X1), X2)active#(isNat(0)) → mark#(tt)
isNatIList#(active(X)) → isNatIList#(X)active#(U11(tt, L)) → mark#(s(length(L)))
mark#(cons(X1, X2)) → mark#(X1)and#(mark(X1), X2) → and#(X1, X2)
isNatIList#(mark(X)) → isNatIList#(X)mark#(isNatIList(X)) → isNatIList#(X)
active#(isNatIList(cons(V1, V2))) → isNat#(V1)U11#(X1, mark(X2)) → U11#(X1, X2)
U11#(X1, active(X2)) → U11#(X1, X2)active#(isNatList(cons(V1, V2))) → mark#(and(isNat(V1), isNatList(V2)))
mark#(and(X1, X2)) → mark#(X1)cons#(X1, active(X2)) → cons#(X1, X2)
active#(U11(tt, L)) → length#(L)active#(length(cons(N, L))) → mark#(U11(and(isNatList(L), isNat(N)), L))
active#(isNatList(cons(V1, V2))) → isNat#(V1)and#(active(X1), X2) → and#(X1, X2)
mark#(isNat(X)) → active#(isNat(X))and#(X1, active(X2)) → and#(X1, X2)
cons#(mark(X1), X2) → cons#(X1, X2)mark#(tt) → active#(tt)
active#(isNatIList(cons(V1, V2))) → and#(isNat(V1), isNatIList(V2))isNat#(mark(X)) → isNat#(X)
mark#(isNat(X)) → isNat#(X)active#(length(cons(N, L))) → isNatList#(L)
active#(isNatList(nil)) → mark#(tt)mark#(nil) → active#(nil)
mark#(U11(X1, X2)) → U11#(mark(X1), X2)active#(length(cons(N, L))) → isNat#(N)
mark#(and(X1, X2)) → active#(and(mark(X1), X2))mark#(length(X)) → mark#(X)
active#(isNatIList(zeros)) → mark#(tt)cons#(X1, mark(X2)) → cons#(X1, X2)
mark#(zeros) → active#(zeros)mark#(cons(X1, X2)) → cons#(mark(X1), X2)
active#(isNat(s(V1))) → isNat#(V1)and#(X1, mark(X2)) → and#(X1, X2)
mark#(length(X)) → length#(mark(X))mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))active#(isNatIList(cons(V1, V2))) → isNatIList#(V2)
active#(isNatList(cons(V1, V2))) → and#(isNat(V1), isNatList(V2))active#(length(cons(N, L))) → and#(isNatList(L), isNat(N))
cons#(active(X1), X2) → cons#(X1, X2)active#(and(tt, X)) → mark#(X)
active#(isNatIList(V)) → isNatList#(V)s#(mark(X)) → s#(X)
active#(isNat(length(V1))) → mark#(isNatList(V1))mark#(isNatList(X)) → isNatList#(X)
isNatList#(mark(X)) → isNatList#(X)active#(zeros) → cons#(0, zeros)
active#(zeros) → mark#(cons(0, zeros))s#(active(X)) → s#(X)
mark#(length(X)) → active#(length(mark(X)))mark#(isNatList(X)) → active#(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

The following SCCs where found

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

Problem 3: 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, 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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, 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 4: 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, 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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, 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 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)cons#(active(X1), 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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, 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 11: ReductionPairSAT

Dependency Pair Problem

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, 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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Function Precedence

mark < active < isNatIList = and = isNat = cons# = 0 = isNatList = s = zeros = tt = length = U11 = cons = nil

Argument Filtering

isNatIList: all arguments are removed from isNatIList
mark: collapses to 1
and: collapses to 1
isNat: collapses to 1
cons#: collapses to 2
0: all arguments are removed from 0
isNatList: 1
s: all arguments are removed from s
zeros: all arguments are removed from zeros
tt: all arguments are removed from tt
length: 1
active: 1
U11: 2
cons: 1 2
nil: all arguments are removed from nil

Status

isNatIList: multiset
0: multiset
isNatList: lexicographic with permutation 1 → 1
s: multiset
zeros: multiset
tt: multiset
length: lexicographic with permutation 1 → 1
active: multiset
U11: lexicographic with permutation 2 → 1
cons: lexicographic with permutation 1 → 1 2 → 2
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 14: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

cons#(X1, mark(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Function Precedence

mark < cons# < isNatIList = and = isNat = 0 = isNatList = s = zeros = tt = length = active = U11 = cons = nil

Argument Filtering

isNatIList: all arguments are removed from isNatIList
mark: 1
and: all arguments are removed from and
isNat: all arguments are removed from isNat
cons#: collapses to 2
0: all arguments are removed from 0
isNatList: all arguments are removed from isNatList
s: all arguments are removed from s
zeros: all arguments are removed from zeros
tt: all arguments are removed from tt
length: all arguments are removed from length
active: all arguments are removed from active
U11: 1 2
cons: 1 2
nil: all arguments are removed from nil

Status

isNatIList: multiset
mark: multiset
and: multiset
isNat: multiset
0: multiset
isNatList: multiset
s: multiset
zeros: multiset
tt: multiset
length: multiset
active: multiset
U11: lexicographic with permutation 1 → 1 2 → 2
cons: lexicographic with permutation 1 → 2 2 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 6: 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, 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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, 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 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, 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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, 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

length#(mark(X)) → length#(X)length#(active(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, 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 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

U11#(X1, active(X2)) → U11#(X1, X2)U11#(active(X1), X2) → U11#(X1, X2)
U11#(mark(X1), X2) → U11#(X1, X2)U11#(X1, mark(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 12: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

U11#(X1, active(X2)) → U11#(X1, X2)U11#(X1, mark(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Function Precedence

active < mark < U11# = isNatIList = and = isNat = 0 = isNatList = s = zeros = tt = length = U11 = cons = nil

Argument Filtering

U11#: collapses to 2
isNatIList: all arguments are removed from isNatIList
mark: 1
and: collapses to 2
isNat: all arguments are removed from isNat
0: all arguments are removed from 0
isNatList: all arguments are removed from isNatList
s: all arguments are removed from s
zeros: all arguments are removed from zeros
tt: all arguments are removed from tt
length: all arguments are removed from length
active: collapses to 1
U11: 1 2
cons: collapses to 2
nil: all arguments are removed from nil

Status

isNatIList: multiset
mark: multiset
isNat: multiset
0: multiset
isNatList: multiset
s: multiset
zeros: multiset
tt: multiset
length: multiset
U11: lexicographic with permutation 1 → 2 2 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 15: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

U11#(X1, active(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Function Precedence

U11# = isNatIList = mark = and = isNat = 0 = isNatList = s = zeros = tt = length = active = U11 = cons = nil

Argument Filtering

U11#: 2
isNatIList: 1
mark: 1
and: all arguments are removed from and
isNat: all arguments are removed from isNat
0: all arguments are removed from 0
isNatList: 1
s: 1
zeros: all arguments are removed from zeros
tt: all arguments are removed from tt
length: all arguments are removed from length
active: 1
U11: collapses to 1
cons: 1 2
nil: all arguments are removed from nil

Status

U11#: multiset
isNatIList: lexicographic with permutation 1 → 1
mark: lexicographic with permutation 1 → 1
and: multiset
isNat: multiset
0: multiset
isNatList: lexicographic with permutation 1 → 1
s: lexicographic with permutation 1 → 1
zeros: multiset
tt: multiset
length: multiset
active: multiset
cons: lexicographic with permutation 1 → 2 2 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

U11#(X1, active(X2)) → U11#(X1, X2)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

and#(active(X1), X2) → and#(X1, X2)and#(X1, active(X2)) → and#(X1, X2)
and#(mark(X1), X2) → and#(X1, X2)and#(X1, mark(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 13: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

and#(X1, active(X2)) → and#(X1, X2)and#(X1, mark(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Function Precedence

mark = active < isNatIList = and# = and = isNat = 0 = isNatList = s = zeros = tt = length = U11 = cons = nil

Argument Filtering

isNatIList: collapses to 1
and#: collapses to 2
mark: 1
and: 1 2
isNat: all arguments are removed from isNat
0: all arguments are removed from 0
isNatList: all arguments are removed from isNatList
s: all arguments are removed from s
zeros: all arguments are removed from zeros
tt: all arguments are removed from tt
length: all arguments are removed from length
active: collapses to 1
U11: 1 2
cons: 1 2
nil: all arguments are removed from nil

Status

mark: multiset
and: lexicographic with permutation 1 → 2 2 → 1
isNat: multiset
0: multiset
isNatList: multiset
s: multiset
zeros: multiset
tt: multiset
length: multiset
U11: lexicographic with permutation 1 → 1 2 → 2
cons: lexicographic with permutation 1 → 1 2 → 2
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 16: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

and#(X1, active(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))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNatIList(X)) → active(isNatIList(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(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Original Signature

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

Strategy

Function Precedence

active < isNatIList = and# = mark = and = isNat = 0 = isNatList = s = zeros = tt = length = U11 = cons = nil

Argument Filtering

isNatIList: collapses to 1
and#: collapses to 2
mark: all arguments are removed from mark
and: all arguments are removed from and
isNat: all arguments are removed from isNat
0: all arguments are removed from 0
isNatList: all arguments are removed from isNatList
s: all arguments are removed from s
zeros: all arguments are removed from zeros
tt: all arguments are removed from tt
length: all arguments are removed from length
active: 1
U11: 1
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

mark: multiset
and: multiset
isNat: multiset
0: multiset
isNatList: multiset
s: multiset
zeros: multiset
tt: multiset
length: multiset
active: multiset
U11: lexicographic with permutation 1 → 1
cons: multiset
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

and#(X1, active(X2)) → and#(X1, X2)