YES

The TRS could be proven terminating. The proof took 2956 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (912ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (0ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (0ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (0ms).
 |    | – Problem 12 was processed with processor SubtermCriterion (0ms).
 | – Problem 10 was processed with processor SubtermCriterion (0ms).
 | – Problem 11 was processed with processor PolynomialLinearRange4iUR (1273ms).
 |    | – Problem 13 was processed with processor PolynomialLinearRange4iUR (646ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2)) → proper#(X1)top#(ok(X)) → top#(active(X))
cons#(ok(X1), ok(X2)) → cons#(X1, X2)proper#(and(X1, X2)) → and#(proper(X1), proper(X2))
from#(ok(X)) → from#(X)active#(first(s(X), cons(Y, Z))) → cons#(Y, first(X, Z))
active#(if(X1, X2, X3)) → active#(X1)active#(add(X1, X2)) → add#(active(X1), X2)
proper#(and(X1, X2)) → proper#(X2)first#(mark(X1), X2) → first#(X1, X2)
top#(mark(X)) → proper#(X)proper#(from(X)) → proper#(X)
proper#(add(X1, X2)) → proper#(X2)active#(first(X1, X2)) → active#(X2)
top#(mark(X)) → top#(proper(X))proper#(cons(X1, X2)) → proper#(X2)
proper#(first(X1, X2)) → first#(proper(X1), proper(X2))proper#(add(X1, X2)) → proper#(X1)
add#(mark(X1), X2) → add#(X1, X2)and#(mark(X1), X2) → and#(X1, X2)
active#(first(X1, X2)) → active#(X1)proper#(first(X1, X2)) → proper#(X2)
active#(from(X)) → s#(X)proper#(s(X)) → proper#(X)
active#(add(s(X), Y)) → add#(X, Y)if#(mark(X1), X2, X3) → if#(X1, X2, X3)
proper#(add(X1, X2)) → add#(proper(X1), proper(X2))active#(first(X1, X2)) → first#(X1, active(X2))
and#(ok(X1), ok(X2)) → and#(X1, X2)add#(ok(X1), ok(X2)) → add#(X1, X2)
proper#(and(X1, X2)) → proper#(X1)top#(ok(X)) → active#(X)
active#(first(s(X), cons(Y, Z))) → first#(X, Z)active#(and(X1, X2)) → and#(active(X1), X2)
active#(add(s(X), Y)) → s#(add(X, Y))active#(from(X)) → cons#(X, from(s(X)))
proper#(from(X)) → from#(proper(X))if#(ok(X1), ok(X2), ok(X3)) → if#(X1, X2, X3)
first#(X1, mark(X2)) → first#(X1, X2)active#(add(X1, X2)) → active#(X1)
proper#(if(X1, X2, X3)) → proper#(X1)proper#(if(X1, X2, X3)) → proper#(X2)
s#(ok(X)) → s#(X)first#(ok(X1), ok(X2)) → first#(X1, X2)
active#(first(X1, X2)) → first#(active(X1), X2)proper#(cons(X1, X2)) → cons#(proper(X1), proper(X2))
proper#(if(X1, X2, X3)) → proper#(X3)proper#(s(X)) → s#(proper(X))
proper#(first(X1, X2)) → proper#(X1)active#(if(X1, X2, X3)) → if#(active(X1), X2, X3)
active#(and(X1, X2)) → active#(X1)proper#(if(X1, X2, X3)) → if#(proper(X1), proper(X2), proper(X3))
active#(from(X)) → from#(s(X))

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

The following SCCs where found

active#(first(X1, X2)) → active#(X2)active#(if(X1, X2, X3)) → active#(X1)
active#(add(X1, X2)) → active#(X1)active#(and(X1, X2)) → active#(X1)
active#(first(X1, X2)) → active#(X1)
add#(mark(X1), X2) → add#(X1, X2)add#(ok(X1), ok(X2)) → add#(X1, X2)
proper#(cons(X1, X2)) → proper#(X1)proper#(if(X1, X2, X3)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(if(X1, X2, X3)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X1)proper#(and(X1, X2)) → proper#(X1)
proper#(first(X1, X2)) → proper#(X2)proper#(s(X)) → proper#(X)
proper#(and(X1, X2)) → proper#(X2)proper#(first(X1, X2)) → proper#(X1)
proper#(if(X1, X2, X3)) → proper#(X3)proper#(from(X)) → proper#(X)
proper#(add(X1, X2)) → proper#(X2)
cons#(ok(X1), ok(X2)) → cons#(X1, X2)
if#(mark(X1), X2, X3) → if#(X1, X2, X3)if#(ok(X1), ok(X2), ok(X3)) → if#(X1, X2, X3)
s#(ok(X)) → s#(X)
and#(ok(X1), ok(X2)) → and#(X1, X2)and#(mark(X1), X2) → and#(X1, X2)
from#(ok(X)) → from#(X)
top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))
first#(ok(X1), ok(X2)) → first#(X1, X2)first#(mark(X1), X2) → first#(X1, X2)
first#(X1, mark(X2)) → first#(X1, X2)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, 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 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

active#(first(X1, X2)) → active#(X2)active#(if(X1, X2, X3)) → active#(X1)
active#(add(X1, X2)) → active#(X1)active#(and(X1, X2)) → active#(X1)
active#(first(X1, X2)) → active#(X1)

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(first(X1, X2)) → active#(X2)active#(if(X1, X2, X3)) → active#(X1)
active#(add(X1, X2)) → active#(X1)active#(and(X1, X2)) → active#(X1)
active#(first(X1, X2)) → active#(X1)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2)) → proper#(X1)proper#(if(X1, X2, X3)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(if(X1, X2, X3)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X1)proper#(and(X1, X2)) → proper#(X1)
proper#(first(X1, X2)) → proper#(X2)proper#(s(X)) → proper#(X)
proper#(and(X1, X2)) → proper#(X2)proper#(if(X1, X2, X3)) → proper#(X3)
proper#(first(X1, X2)) → proper#(X1)proper#(from(X)) → proper#(X)
proper#(add(X1, X2)) → proper#(X2)

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(cons(X1, X2)) → proper#(X1)proper#(if(X1, X2, X3)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(if(X1, X2, X3)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X1)proper#(and(X1, X2)) → proper#(X1)
proper#(first(X1, X2)) → proper#(X2)proper#(s(X)) → proper#(X)
proper#(and(X1, X2)) → proper#(X2)proper#(if(X1, X2, X3)) → proper#(X3)
proper#(first(X1, X2)) → proper#(X1)proper#(from(X)) → proper#(X)
proper#(add(X1, X2)) → proper#(X2)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

from#(ok(X)) → from#(X)

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

from#(ok(X)) → from#(X)

Problem 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 12: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, top, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 11: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top

Strategy

Polynomial Interpretation

Improved Usable rules

proper(false) → ok(false)and(ok(X1), ok(X2)) → ok(and(X1, X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(and(false, Y)) → mark(false)
first(X1, mark(X2)) → mark(first(X1, X2))active(first(0, X)) → mark(nil)
proper(add(X1, X2)) → add(proper(X1), proper(X2))active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
add(mark(X1), X2) → mark(add(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
active(first(X1, X2)) → first(active(X1), X2)proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
active(add(X1, X2)) → add(active(X1), X2)proper(s(X)) → s(proper(X))
active(and(true, X)) → mark(X)active(from(X)) → mark(cons(X, from(s(X))))
first(ok(X1), ok(X2)) → ok(first(X1, X2))active(and(X1, X2)) → and(active(X1), X2)
proper(first(X1, X2)) → first(proper(X1), proper(X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))first(mark(X1), X2) → mark(first(X1, X2))
s(ok(X)) → ok(s(X))active(add(s(X), Y)) → mark(s(add(X, Y)))
from(ok(X)) → ok(from(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
active(if(false, X, Y)) → mark(Y)proper(true) → ok(true)
add(ok(X1), ok(X2)) → ok(add(X1, X2))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)active(add(0, X)) → mark(X)
and(mark(X1), X2) → mark(and(X1, X2))proper(0) → ok(0)
active(if(true, X, Y)) → mark(X)proper(from(X)) → from(proper(X))
active(first(X1, X2)) → first(X1, active(X2))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

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

Problem 13: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(true, X)) → mark(X)active(and(false, Y)) → mark(false)
active(if(true, X, Y)) → mark(X)active(if(false, X, Y)) → mark(Y)
active(add(0, X)) → mark(X)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(and(X1, X2)) → and(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)active(add(X1, X2)) → add(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
add(mark(X1), X2) → mark(add(X1, X2))first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(true) → ok(true)proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(first(X1, X2)) → first(proper(X1), proper(X2))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
add(ok(X1), ok(X2)) → ok(add(X1, X2))s(ok(X)) → ok(s(X))
first(ok(X1), ok(X2)) → ok(first(X1, X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
from(ok(X)) → ok(from(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, top, nil, cons

Strategy

Polynomial Interpretation

Improved Usable rules

if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))and(ok(X1), ok(X2)) → ok(and(X1, X2))
first(mark(X1), X2) → mark(first(X1, X2))active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(and(false, Y)) → mark(false)active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)first(X1, mark(X2)) → mark(first(X1, X2))
active(if(false, X, Y)) → mark(Y)active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
add(ok(X1), ok(X2)) → ok(add(X1, X2))add(mark(X1), X2) → mark(add(X1, X2))
active(first(X1, X2)) → first(active(X1), X2)active(add(X1, X2)) → add(active(X1), X2)
active(add(0, X)) → mark(X)and(mark(X1), X2) → mark(and(X1, X2))
active(and(true, X)) → mark(X)active(from(X)) → mark(cons(X, from(s(X))))
first(ok(X1), ok(X2)) → ok(first(X1, X2))active(if(true, X, Y)) → mark(X)
active(and(X1, X2)) → and(active(X1), X2)active(first(X1, X2)) → first(X1, active(X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

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