TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (6444ms).
 | – 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 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 12 was processed with processor ReductionPairSAT (87ms).
 |    |    | – Problem 16 was processed with processor ReductionPairSAT (71ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (4ms).
 |    | – Problem 13 was processed with processor ReductionPairSAT (89ms).
 |    |    | – Problem 17 was processed with processor ReductionPairSAT (27ms).
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 14 was processed with processor ReductionPairSAT (121ms).
 |    |    | – Problem 18 was processed with processor ReductionPairSAT (69ms).
 | – Problem 11 was processed with processor ReductionPairSAT (23557ms).
 |    | – Problem 15 remains open; application of the following processors failed [DependencyGraph (975ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 15

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))active#(first(0, X)) → mark#(nil)
active#(add(s(X), Y)) → mark#(s(add(X, Y)))active#(half(s(0))) → mark#(0)
mark#(sqr(X)) → active#(sqr(mark(X)))active#(dbl(s(X))) → mark#(s(s(dbl(X))))
active#(sqr(0)) → mark#(0)mark#(recip(X)) → mark#(X)
active#(half(0)) → mark#(0)active#(first(s(X), cons(Y, Z))) → mark#(cons(Y, first(X, Z)))
active#(sqr(s(X))) → mark#(s(add(sqr(X), dbl(X))))mark#(add(X1, X2)) → mark#(X2)
mark#(half(X)) → active#(half(mark(X)))mark#(add(X1, X2)) → active#(add(mark(X1), mark(X2)))
mark#(s(X)) → mark#(X)mark#(add(X1, X2)) → mark#(X1)
mark#(recip(X)) → active#(recip(mark(X)))mark#(0) → active#(0)
mark#(first(X1, X2)) → mark#(X2)mark#(s(X)) → active#(s(mark(X)))
mark#(cons(X1, X2)) → mark#(X1)mark#(first(X1, X2)) → active#(first(mark(X1), mark(X2)))
mark#(dbl(X)) → active#(dbl(mark(X)))active#(half(dbl(X))) → mark#(X)
active#(add(0, X)) → mark#(X)mark#(terms(X)) → active#(terms(mark(X)))
mark#(dbl(X)) → mark#(X)mark#(terms(X)) → mark#(X)
mark#(sqr(X)) → mark#(X)mark#(half(X)) → mark#(X)
active#(dbl(0)) → mark#(0)mark#(first(X1, X2)) → mark#(X1)
active#(half(s(s(X)))) → mark#(s(half(X)))active#(terms(N)) → mark#(cons(recip(sqr(N)), terms(s(N))))

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

active#(first(0, X)) → mark#(nil)mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(half(X)) → half#(mark(X))add#(X1, mark(X2)) → add#(X1, X2)
active#(add(s(X), Y)) → mark#(s(add(X, Y)))active#(sqr(s(X))) → s#(add(sqr(X), dbl(X)))
recip#(active(X)) → recip#(X)active#(dbl(s(X))) → s#(dbl(X))
active#(terms(N)) → terms#(s(N))half#(active(X)) → half#(X)
active#(first(s(X), cons(Y, Z))) → cons#(Y, first(X, Z))mark#(s(X)) → s#(mark(X))
first#(X1, active(X2)) → first#(X1, X2)terms#(mark(X)) → terms#(X)
mark#(recip(X)) → mark#(X)active#(first(s(X), cons(Y, Z))) → mark#(cons(Y, first(X, Z)))
mark#(add(X1, X2)) → mark#(X2)mark#(dbl(X)) → dbl#(mark(X))
mark#(half(X)) → active#(half(mark(X)))mark#(add(X1, X2)) → active#(add(mark(X1), mark(X2)))
mark#(s(X)) → mark#(X)active#(dbl(s(X))) → dbl#(X)
first#(mark(X1), X2) → first#(X1, X2)mark#(add(X1, X2)) → mark#(X1)
mark#(recip(X)) → active#(recip(mark(X)))mark#(recip(X)) → recip#(mark(X))
active#(sqr(s(X))) → dbl#(X)active#(dbl(s(X))) → s#(s(dbl(X)))
terms#(active(X)) → terms#(X)mark#(cons(X1, X2)) → mark#(X1)
mark#(dbl(X)) → active#(dbl(mark(X)))active#(sqr(s(X))) → sqr#(X)
active#(add(0, X)) → mark#(X)active#(terms(N)) → sqr#(N)
add#(mark(X1), X2) → add#(X1, X2)mark#(terms(X)) → active#(terms(mark(X)))
cons#(X1, active(X2)) → cons#(X1, X2)mark#(sqr(X)) → mark#(X)
mark#(half(X)) → mark#(X)active#(add(s(X), Y)) → add#(X, Y)
active#(half(s(s(X)))) → half#(X)mark#(add(X1, X2)) → add#(mark(X1), mark(X2))
first#(active(X1), X2) → first#(X1, X2)active#(sqr(s(X))) → add#(sqr(X), dbl(X))
active#(dbl(0)) → mark#(0)add#(active(X1), X2) → add#(X1, X2)
mark#(first(X1, X2)) → mark#(X1)active#(half(s(s(X)))) → mark#(s(half(X)))
active#(terms(N)) → mark#(cons(recip(sqr(N)), terms(s(N))))mark#(sqr(X)) → sqr#(mark(X))
cons#(mark(X1), X2) → cons#(X1, X2)active#(half(s(0))) → mark#(0)
mark#(sqr(X)) → active#(sqr(mark(X)))active#(dbl(s(X))) → mark#(s(s(dbl(X))))
active#(first(s(X), cons(Y, Z))) → first#(X, Z)active#(sqr(0)) → mark#(0)
mark#(nil) → active#(nil)active#(half(0)) → mark#(0)
active#(add(s(X), Y)) → s#(add(X, Y))active#(sqr(s(X))) → mark#(s(add(sqr(X), dbl(X))))
sqr#(active(X)) → sqr#(X)add#(X1, active(X2)) → add#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)mark#(cons(X1, X2)) → cons#(mark(X1), X2)
mark#(first(X1, X2)) → first#(mark(X1), mark(X2))half#(mark(X)) → half#(X)
first#(X1, mark(X2)) → first#(X1, X2)mark#(0) → active#(0)
mark#(first(X1, X2)) → mark#(X2)mark#(s(X)) → active#(s(mark(X)))
mark#(first(X1, X2)) → active#(first(mark(X1), mark(X2)))active#(half(dbl(X))) → mark#(X)
active#(terms(N)) → cons#(recip(sqr(N)), terms(s(N)))cons#(active(X1), X2) → cons#(X1, X2)
dbl#(mark(X)) → dbl#(X)active#(terms(N)) → recip#(sqr(N))
mark#(dbl(X)) → mark#(X)mark#(terms(X)) → mark#(X)
active#(half(s(s(X)))) → s#(half(X))s#(mark(X)) → s#(X)
mark#(terms(X)) → terms#(mark(X))sqr#(mark(X)) → sqr#(X)
active#(terms(N)) → s#(N)s#(active(X)) → s#(X)
dbl#(active(X)) → dbl#(X)recip#(mark(X)) → recip#(X)

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

The following SCCs where found

half#(mark(X)) → half#(X)half#(active(X)) → half#(X)
sqr#(mark(X)) → sqr#(X)sqr#(active(X)) → sqr#(X)
mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))active#(first(0, X)) → mark#(nil)
active#(add(s(X), Y)) → mark#(s(add(X, Y)))active#(half(s(0))) → mark#(0)
mark#(sqr(X)) → active#(sqr(mark(X)))active#(dbl(s(X))) → mark#(s(s(dbl(X))))
active#(sqr(0)) → mark#(0)mark#(recip(X)) → mark#(X)
mark#(nil) → active#(nil)active#(half(0)) → mark#(0)
active#(first(s(X), cons(Y, Z))) → mark#(cons(Y, first(X, Z)))active#(sqr(s(X))) → mark#(s(add(sqr(X), dbl(X))))
mark#(add(X1, X2)) → mark#(X2)mark#(half(X)) → active#(half(mark(X)))
mark#(s(X)) → mark#(X)mark#(add(X1, X2)) → active#(add(mark(X1), mark(X2)))
mark#(add(X1, X2)) → mark#(X1)mark#(recip(X)) → active#(recip(mark(X)))
mark#(first(X1, X2)) → mark#(X2)mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))mark#(first(X1, X2)) → active#(first(mark(X1), mark(X2)))
mark#(cons(X1, X2)) → mark#(X1)mark#(dbl(X)) → active#(dbl(mark(X)))
active#(half(dbl(X))) → mark#(X)active#(add(0, X)) → mark#(X)
mark#(terms(X)) → active#(terms(mark(X)))mark#(dbl(X)) → mark#(X)
mark#(terms(X)) → mark#(X)mark#(sqr(X)) → mark#(X)
mark#(half(X)) → mark#(X)active#(dbl(0)) → mark#(0)
mark#(first(X1, X2)) → mark#(X1)active#(half(s(s(X)))) → mark#(s(half(X)))
active#(terms(N)) → mark#(cons(recip(sqr(N)), terms(s(N))))
dbl#(mark(X)) → dbl#(X)dbl#(active(X)) → dbl#(X)
recip#(active(X)) → recip#(X)recip#(mark(X)) → recip#(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)
terms#(mark(X)) → terms#(X)terms#(active(X)) → terms#(X)
first#(active(X1), X2) → first#(X1, X2)first#(mark(X1), X2) → first#(X1, X2)
first#(X1, mark(X2)) → first#(X1, X2)first#(X1, active(X2)) → first#(X1, X2)
add#(active(X1), X2) → add#(X1, X2)add#(X1, mark(X2)) → add#(X1, X2)
add#(X1, active(X2)) → add#(X1, X2)add#(mark(X1), X2) → add#(X1, X2)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

half#(mark(X)) → half#(X)half#(active(X)) → half#(X)

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

half#(mark(X)) → half#(X)half#(active(X)) → half#(X)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

terms#(mark(X)) → terms#(X)terms#(active(X)) → terms#(X)

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

terms#(mark(X)) → terms#(X)terms#(active(X)) → terms#(X)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, 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 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

recip#(active(X)) → recip#(X)recip#(mark(X)) → recip#(X)

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

recip#(active(X)) → recip#(X)recip#(mark(X)) → recip#(X)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

dbl#(mark(X)) → dbl#(X)dbl#(active(X)) → dbl#(X)

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

dbl#(mark(X)) → dbl#(X)dbl#(active(X)) → dbl#(X)

Problem 7: 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(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, 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 12: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Function Precedence

mark = active < terms = sqr = half = dbl = recip = add = cons# = 0 = s = first = cons = nil

Argument Filtering

terms: all arguments are removed from terms
sqr: all arguments are removed from sqr
half: collapses to 1
mark: 1
dbl: all arguments are removed from dbl
recip: all arguments are removed from recip
add: all arguments are removed from add
cons#: collapses to 2
0: all arguments are removed from 0
s: all arguments are removed from s
active: collapses to 1
first: all arguments are removed from first
cons: collapses to 2
nil: all arguments are removed from nil

Status

terms: multiset
sqr: multiset
mark: multiset
dbl: multiset
recip: multiset
add: multiset
0: multiset
s: multiset
first: 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.

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

Problem 16: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Function Precedence

active < terms = sqr = half = mark = dbl = recip = add = cons# = 0 = s = first = cons = nil

Argument Filtering

terms: all arguments are removed from terms
sqr: collapses to 1
half: all arguments are removed from half
mark: collapses to 1
dbl: all arguments are removed from dbl
recip: all arguments are removed from recip
add: all arguments are removed from add
cons#: collapses to 2
0: all arguments are removed from 0
s: all arguments are removed from s
active: 1
first: collapses to 2
cons: 1
nil: all arguments are removed from nil

Status

terms: multiset
half: multiset
dbl: multiset
recip: multiset
add: multiset
0: multiset
s: multiset
active: multiset
cons: lexicographic with permutation 1 → 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, active(X2)) → cons#(X1, X2)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

sqr#(mark(X)) → sqr#(X)sqr#(active(X)) → sqr#(X)

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

sqr#(mark(X)) → sqr#(X)sqr#(active(X)) → sqr#(X)

Problem 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 13: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Function Precedence

mark < first# < active < terms = sqr = half = dbl = recip = add = 0 = s = first = cons = nil

Argument Filtering

terms: all arguments are removed from terms
sqr: 1
half: 1
mark: collapses to 1
dbl: all arguments are removed from dbl
recip: collapses to 1
add: 1 2
first#: 2
0: all arguments are removed from 0
s: all arguments are removed from s
active: 1
first: 1 2
cons: 1 2
nil: all arguments are removed from nil

Status

terms: multiset
sqr: lexicographic with permutation 1 → 1
half: lexicographic with permutation 1 → 1
dbl: multiset
add: lexicographic with permutation 1 → 2 2 → 1
first#: multiset
0: multiset
s: multiset
active: lexicographic with permutation 1 → 1
first: 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.

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

Problem 17: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Function Precedence

terms = sqr = half = mark = dbl = recip = add = first# = 0 = s = active = first = cons = nil

Argument Filtering

terms: all arguments are removed from terms
sqr: all arguments are removed from sqr
half: all arguments are removed from half
mark: 1
dbl: all arguments are removed from dbl
recip: all arguments are removed from recip
add: all arguments are removed from add
first#: collapses to 2
0: all arguments are removed from 0
s: 1
active: all arguments are removed from active
first: 1 2
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

terms: multiset
sqr: multiset
half: multiset
mark: multiset
dbl: multiset
recip: multiset
add: multiset
0: multiset
s: lexicographic with permutation 1 → 1
active: multiset
first: lexicographic with permutation 1 → 2 2 → 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.

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

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 14: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Function Precedence

add# < mark < active < terms = sqr = half = dbl = recip = add = 0 = s = first = cons = nil

Argument Filtering

terms: all arguments are removed from terms
sqr: collapses to 1
half: collapses to 1
mark: 1
dbl: collapses to 1
recip: collapses to 1
add: collapses to 2
0: all arguments are removed from 0
s: collapses to 1
active: collapses to 1
add#: 1 2
first: 1 2
cons: collapses to 2
nil: all arguments are removed from nil

Status

terms: multiset
mark: multiset
0: multiset
add#: lexicographic with permutation 1 → 1 2 → 2
first: 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.

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

Problem 18: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Function Precedence

terms = sqr = half = mark = dbl = recip = add = 0 = s = active = add# = first = cons = nil

Argument Filtering

terms: all arguments are removed from terms
sqr: all arguments are removed from sqr
half: collapses to 1
mark: collapses to 1
dbl: all arguments are removed from dbl
recip: all arguments are removed from recip
add: all arguments are removed from add
0: all arguments are removed from 0
s: all arguments are removed from s
active: 1
add#: collapses to 2
first: 1 2
cons: 1 2
nil: all arguments are removed from nil

Status

terms: multiset
sqr: multiset
dbl: multiset
recip: multiset
add: multiset
0: multiset
s: multiset
active: lexicographic with permutation 1 → 1
first: 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.

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

Problem 11: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))active#(first(0, X)) → mark#(nil)
active#(add(s(X), Y)) → mark#(s(add(X, Y)))active#(half(s(0))) → mark#(0)
mark#(sqr(X)) → active#(sqr(mark(X)))active#(dbl(s(X))) → mark#(s(s(dbl(X))))
active#(sqr(0)) → mark#(0)mark#(recip(X)) → mark#(X)
mark#(nil) → active#(nil)active#(half(0)) → mark#(0)
active#(first(s(X), cons(Y, Z))) → mark#(cons(Y, first(X, Z)))active#(sqr(s(X))) → mark#(s(add(sqr(X), dbl(X))))
mark#(add(X1, X2)) → mark#(X2)mark#(half(X)) → active#(half(mark(X)))
mark#(add(X1, X2)) → active#(add(mark(X1), mark(X2)))mark#(s(X)) → mark#(X)
mark#(add(X1, X2)) → mark#(X1)mark#(recip(X)) → active#(recip(mark(X)))
mark#(0) → active#(0)mark#(first(X1, X2)) → mark#(X2)
mark#(s(X)) → active#(s(mark(X)))mark#(cons(X1, X2)) → mark#(X1)
mark#(first(X1, X2)) → active#(first(mark(X1), mark(X2)))mark#(dbl(X)) → active#(dbl(mark(X)))
active#(half(dbl(X))) → mark#(X)active#(add(0, X)) → mark#(X)
mark#(terms(X)) → active#(terms(mark(X)))mark#(dbl(X)) → mark#(X)
mark#(terms(X)) → mark#(X)mark#(sqr(X)) → mark#(X)
mark#(half(X)) → mark#(X)active#(dbl(0)) → mark#(0)
mark#(first(X1, X2)) → mark#(X1)active#(half(s(s(X)))) → mark#(s(half(X)))
active#(terms(N)) → mark#(cons(recip(sqr(N)), terms(s(N))))

Rewrite Rules

active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))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(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(half(X)) → active(half(mark(X)))
terms(mark(X)) → terms(X)terms(active(X)) → terms(X)
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)
recip(mark(X)) → recip(X)recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)first(X1, active(X2)) → first(X1, X2)
half(mark(X)) → half(X)half(active(X)) → half(X)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, half, mark, dbl, recip, add, 0, s, active, first, cons, nil

Strategy

Function Precedence

active < terms = sqr = half = mark = dbl = recip = add = mark# = 0 = s = active# = first = cons = nil

Argument Filtering

terms: all arguments are removed from terms
sqr: all arguments are removed from sqr
half: all arguments are removed from half
mark: all arguments are removed from mark
dbl: all arguments are removed from dbl
recip: all arguments are removed from recip
add: all arguments are removed from add
mark#: all arguments are removed from mark#
0: all arguments are removed from 0
s: all arguments are removed from s
active: collapses to 1
active#: collapses to 1
first: all arguments are removed from first
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

terms: multiset
sqr: multiset
half: multiset
mark: multiset
dbl: multiset
recip: multiset
add: multiset
mark#: multiset
0: multiset
s: multiset
first: multiset
cons: multiset
nil: multiset

Usable Rules

mark(sqr(X)) → active(sqr(mark(X)))cons(active(X1), X2) → cons(X1, X2)
active(sqr(0)) → mark(0)half(mark(X)) → half(X)
mark(recip(X)) → active(recip(mark(X)))mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))mark(s(X)) → active(s(mark(X)))
active(first(0, X)) → mark(nil)add(X1, mark(X2)) → add(X1, X2)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))first(X1, mark(X2)) → first(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)terms(active(X)) → terms(X)
first(active(X1), X2) → first(X1, X2)recip(mark(X)) → recip(X)
first(X1, active(X2)) → first(X1, X2)add(X1, active(X2)) → add(X1, X2)
active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))add(mark(X1), X2) → add(X1, X2)
active(half(s(s(X)))) → mark(s(half(X)))mark(nil) → active(nil)
dbl(mark(X)) → dbl(X)mark(0) → active(0)
s(active(X)) → s(X)mark(half(X)) → active(half(mark(X)))
cons(X1, active(X2)) → cons(X1, X2)active(half(dbl(X))) → mark(X)
sqr(mark(X)) → sqr(X)first(mark(X1), X2) → first(X1, X2)
add(active(X1), X2) → add(X1, X2)terms(mark(X)) → terms(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(half(0)) → mark(0)
active(half(s(0))) → mark(0)active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
half(active(X)) → half(X)cons(mark(X1), X2) → cons(X1, X2)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(terms(X)) → active(terms(mark(X)))
active(add(0, X)) → mark(X)s(mark(X)) → s(X)
recip(active(X)) → recip(X)sqr(active(X)) → sqr(X)
mark(dbl(X)) → active(dbl(mark(X)))dbl(active(X)) → dbl(X)

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.

mark#(nil) → active#(nil)