YES
The TRS could be proven terminating. The proof took 57498 ms.
The following DP Processors were used
Problem 1 was processed with processor ReductionPairSAT (3356ms).
| – Problem 2 was processed with processor DependencyGraph (113ms).
| | – Problem 3 was processed with processor ReductionPairSAT (2386ms).
| | | – Problem 4 was processed with processor ReductionPairSAT (1624ms).
| | | | – Problem 5 was processed with processor ReductionPairSAT (1648ms).
| | | | | – Problem 6 was processed with processor DependencyGraph (65ms).
| | | | | | – Problem 7 was processed with processor ReductionPairSAT (446ms).
| | | | | | – Problem 8 was processed with processor ReductionPairSAT (2521ms).
| | | | | | | – Problem 9 was processed with processor ReductionPairSAT (2204ms).
| | | | | | | | – Problem 10 was processed with processor ReductionPairSAT (807ms).
| | | | | | | | | – Problem 11 was processed with processor DependencyGraph (3ms).
| | | | | | | | | | – Problem 12 was processed with processor ReductionPairSAT (469ms).
| | | | | | | | | | – Problem 13 was processed with processor ReductionPairSAT (53ms).
| | | | | | | | | | | – Problem 14 was processed with processor ReductionPairSAT (50ms).
| | | | | | | | | | | | – Problem 15 was processed with processor ReductionPairSAT (9ms).
Problem 1: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(first(X1, X2)) | → | a__first#(mark(X1), mark(X2)) | | mark#(dbl(X)) | → | a__dbl#(mark(X)) |
| mark#(half(X)) | → | a__half#(mark(X)) | | a__half#(dbl(X)) | → | mark#(X) |
| a__half#(s(s(X))) | → | a__half#(mark(X)) | | mark#(recip(X)) | → | mark#(X) |
| a__first#(s(X), cons(Y, Z)) | → | mark#(Y) | | a__sqr#(s(X)) | → | a__dbl#(mark(X)) |
| a__dbl#(s(X)) | → | mark#(X) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(s(X)) | → | mark#(X) | | a__add#(s(X), Y) | → | mark#(Y) |
| mark#(add(X1, X2)) | → | mark#(X1) | | a__add#(s(X), Y) | → | mark#(X) |
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| a__sqr#(s(X)) | → | a__add#(a__sqr(mark(X)), a__dbl(mark(X))) | | a__terms#(N) | → | mark#(N) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | a__half#(s(s(X))) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | mark#(X) |
| a__add#(0, X) | → | mark#(X) | | mark#(dbl(X)) | → | mark#(X) |
| mark#(terms(X)) | → | mark#(X) | | mark#(sqr(X)) | → | mark#(X) |
| mark#(half(X)) | → | mark#(X) | | mark#(sqr(X)) | → | a__sqr#(mark(X)) |
| mark#(first(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | a__sqr#(mark(X)) |
| a__terms#(N) | → | a__sqr#(mark(N)) | | a__dbl#(s(X)) | → | a__dbl#(mark(X)) |
| a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Function Precedence
a__half# < mark# < recip < a__first# < a__half = terms = half = a__terms# = a__terms < cons = 0 < a__sqr# = a__sqr = sqr < nil < a__add# = dbl = a__add = add = a__dbl < a__dbl# = mark = s = first = a__first
Argument Filtering
a__half: 1
a__add#: 1 2
a__half#: collapses to 1
terms: 1
half: 1
dbl: 1
a__add: 1 2
add: 1 2
a__sqr#: 1
a__dbl#: 1
a__first#: collapses to 2
a__sqr: 1
cons: collapses to 1
a__terms#: 1
sqr: 1
mark: collapses to 1
recip: collapses to 1
mark#: collapses to 1
a__terms: 1
0: all arguments are removed from 0
s: 1
a__dbl: 1
first: 1 2
a__first: 1 2
nil: all arguments are removed from nil
Status
a__half: multiset
a__add#: multiset
terms: multiset
half: multiset
dbl: multiset
a__add: multiset
add: multiset
a__sqr#: multiset
a__dbl#: lexicographic with permutation 1 → 1
a__sqr: multiset
a__terms#: multiset
sqr: multiset
a__terms: multiset
0: multiset
s: lexicographic with permutation 1 → 1
a__dbl: multiset
first: lexicographic with permutation 1 → 2 2 → 1
a__first: lexicographic with permutation 1 → 2 2 → 1
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | mark(cons(X1, X2)) → cons(mark(X1), X2) |
| a__first(X1, X2) → first(X1, X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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#(first(X1, X2)) → a__first#(mark(X1), mark(X2)) |
Problem 2: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(dbl(X)) | → | a__dbl#(mark(X)) | | mark#(half(X)) | → | a__half#(mark(X)) |
| a__half#(dbl(X)) | → | mark#(X) | | a__half#(s(s(X))) | → | a__half#(mark(X)) |
| mark#(recip(X)) | → | mark#(X) | | a__first#(s(X), cons(Y, Z)) | → | mark#(Y) |
| a__sqr#(s(X)) | → | a__dbl#(mark(X)) | | a__dbl#(s(X)) | → | mark#(X) |
| mark#(add(X1, X2)) | → | mark#(X2) | | mark#(s(X)) | → | mark#(X) |
| a__add#(s(X), Y) | → | mark#(Y) | | mark#(add(X1, X2)) | → | mark#(X1) |
| a__add#(s(X), Y) | → | mark#(X) | | mark#(first(X1, X2)) | → | mark#(X2) |
| mark#(terms(X)) | → | a__terms#(mark(X)) | | a__sqr#(s(X)) | → | a__add#(a__sqr(mark(X)), a__dbl(mark(X))) |
| a__terms#(N) | → | mark#(N) | | mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) |
| a__half#(s(s(X))) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | mark#(X) | | a__add#(0, X) | → | mark#(X) |
| mark#(dbl(X)) | → | mark#(X) | | mark#(terms(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | a__sqr#(mark(X)) | | mark#(first(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | a__sqr#(mark(X)) | | a__dbl#(s(X)) | → | a__dbl#(mark(X)) |
| a__terms#(N) | → | a__sqr#(mark(N)) | | a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
The following SCCs where found
| mark#(dbl(X)) → a__dbl#(mark(X)) | mark#(half(X)) → a__half#(mark(X)) |
| a__half#(dbl(X)) → mark#(X) | a__half#(s(s(X))) → a__half#(mark(X)) |
| mark#(recip(X)) → mark#(X) | a__sqr#(s(X)) → a__dbl#(mark(X)) |
| a__dbl#(s(X)) → mark#(X) | mark#(add(X1, X2)) → mark#(X2) |
| mark#(s(X)) → mark#(X) | a__add#(s(X), Y) → mark#(Y) |
| mark#(add(X1, X2)) → mark#(X1) | a__add#(s(X), Y) → mark#(X) |
| mark#(first(X1, X2)) → mark#(X2) | mark#(terms(X)) → a__terms#(mark(X)) |
| a__sqr#(s(X)) → a__add#(a__sqr(mark(X)), a__dbl(mark(X))) | a__terms#(N) → mark#(N) |
| mark#(add(X1, X2)) → a__add#(mark(X1), mark(X2)) | a__half#(s(s(X))) → mark#(X) |
| mark#(cons(X1, X2)) → mark#(X1) | a__sqr#(s(X)) → mark#(X) |
| a__add#(0, X) → mark#(X) | mark#(dbl(X)) → mark#(X) |
| mark#(terms(X)) → mark#(X) | mark#(sqr(X)) → mark#(X) |
| mark#(half(X)) → mark#(X) | mark#(sqr(X)) → a__sqr#(mark(X)) |
| mark#(first(X1, X2)) → mark#(X1) | a__sqr#(s(X)) → a__sqr#(mark(X)) |
| a__dbl#(s(X)) → a__dbl#(mark(X)) | a__terms#(N) → a__sqr#(mark(N)) |
| a__add#(s(X), Y) → a__add#(mark(X), mark(Y)) |
Problem 3: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(dbl(X)) | → | a__dbl#(mark(X)) | | mark#(half(X)) | → | a__half#(mark(X)) |
| a__half#(dbl(X)) | → | mark#(X) | | a__half#(s(s(X))) | → | a__half#(mark(X)) |
| mark#(recip(X)) | → | mark#(X) | | a__sqr#(s(X)) | → | a__dbl#(mark(X)) |
| a__dbl#(s(X)) | → | mark#(X) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(s(X)) | → | mark#(X) | | a__add#(s(X), Y) | → | mark#(Y) |
| mark#(add(X1, X2)) | → | mark#(X1) | | a__add#(s(X), Y) | → | mark#(X) |
| mark#(terms(X)) | → | a__terms#(mark(X)) | | mark#(first(X1, X2)) | → | mark#(X2) |
| a__sqr#(s(X)) | → | a__add#(a__sqr(mark(X)), a__dbl(mark(X))) | | a__terms#(N) | → | mark#(N) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | a__half#(s(s(X))) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | mark#(X) |
| a__add#(0, X) | → | mark#(X) | | mark#(dbl(X)) | → | mark#(X) |
| mark#(terms(X)) | → | mark#(X) | | mark#(sqr(X)) | → | mark#(X) |
| mark#(half(X)) | → | mark#(X) | | mark#(sqr(X)) | → | a__sqr#(mark(X)) |
| mark#(first(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | a__sqr#(mark(X)) |
| a__dbl#(s(X)) | → | a__dbl#(mark(X)) | | a__terms#(N) | → | a__sqr#(mark(N)) |
| a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
Function Precedence
half = recip = cons < a__terms# = a__half# = terms = sqr = mark = a__sqr# = mark# = a__terms = 0 = a__dbl# = a__sqr < a__half = a__add# = dbl = add = a__add = a__dbl < s = a__first = first = nil
Argument Filtering
a__half: collapses to 1
a__terms#: 1
a__add#: 1 2
a__half#: collapses to 1
terms: 1
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__sqr#: 1
mark#: collapses to 1
a__terms: 1
0: all arguments are removed from 0
a__dbl#: collapses to 1
a__dbl: 1
s: 1
a__first: 1 2
first: 1 2
a__sqr: 1
nil: all arguments are removed from nil
cons: collapses to 1
Status
a__terms#: lexicographic with permutation 1 → 1
a__add#: lexicographic with permutation 1 → 1 2 → 2
terms: lexicographic with permutation 1 → 1
sqr: lexicographic with permutation 1 → 1
dbl: lexicographic with permutation 1 → 1
add: lexicographic with permutation 1 → 1 2 → 2
a__add: lexicographic with permutation 1 → 1 2 → 2
a__sqr#: lexicographic with permutation 1 → 1
a__terms: lexicographic with permutation 1 → 1
0: multiset
a__dbl: lexicographic with permutation 1 → 1
s: multiset
a__first: multiset
first: multiset
a__sqr: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | mark(cons(X1, X2)) → cons(mark(X1), X2) |
| a__first(X1, X2) → first(X1, X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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.
| a__add#(s(X), Y) → mark#(Y) |
Problem 4: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(dbl(X)) | → | a__dbl#(mark(X)) | | mark#(half(X)) | → | a__half#(mark(X)) |
| a__half#(dbl(X)) | → | mark#(X) | | a__half#(s(s(X))) | → | a__half#(mark(X)) |
| mark#(recip(X)) | → | mark#(X) | | a__sqr#(s(X)) | → | a__dbl#(mark(X)) |
| a__dbl#(s(X)) | → | mark#(X) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(s(X)) | → | mark#(X) | | mark#(add(X1, X2)) | → | mark#(X1) |
| a__add#(s(X), Y) | → | mark#(X) | | mark#(first(X1, X2)) | → | mark#(X2) |
| mark#(terms(X)) | → | a__terms#(mark(X)) | | a__sqr#(s(X)) | → | a__add#(a__sqr(mark(X)), a__dbl(mark(X))) |
| a__terms#(N) | → | mark#(N) | | mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) |
| a__half#(s(s(X))) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | mark#(X) | | a__add#(0, X) | → | mark#(X) |
| mark#(dbl(X)) | → | mark#(X) | | mark#(terms(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | a__sqr#(mark(X)) | | mark#(first(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | a__sqr#(mark(X)) | | a__terms#(N) | → | a__sqr#(mark(N)) |
| a__dbl#(s(X)) | → | a__dbl#(mark(X)) | | a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Function Precedence
cons < half < a__half < a__terms# = terms = sqr = a__sqr# = a__terms = a__sqr < recip < add = a__add < a__half# = dbl = mark# = a__dbl# = a__dbl < a__add# = mark = 0 = s = a__first = first = nil
Argument Filtering
a__half: collapses to 1
a__terms#: 1
a__add#: 1 2
a__half#: collapses to 1
terms: 1
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__sqr#: 1
mark#: collapses to 1
a__terms: 1
0: all arguments are removed from 0
a__dbl#: 1
a__dbl: 1
s: 1
a__first: 1 2
first: 1 2
a__sqr: 1
nil: all arguments are removed from nil
cons: collapses to 1
Status
a__terms#: lexicographic with permutation 1 → 1
a__add#: lexicographic with permutation 1 → 2 2 → 1
terms: lexicographic with permutation 1 → 1
sqr: lexicographic with permutation 1 → 1
dbl: lexicographic with permutation 1 → 1
add: multiset
a__add: multiset
a__sqr#: lexicographic with permutation 1 → 1
a__terms: lexicographic with permutation 1 → 1
0: multiset
a__dbl#: lexicographic with permutation 1 → 1
a__dbl: lexicographic with permutation 1 → 1
s: lexicographic with permutation 1 → 1
a__first: multiset
first: multiset
a__sqr: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | mark(cons(X1, X2)) → cons(mark(X1), X2) |
| a__first(X1, X2) → first(X1, X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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.
| a__half#(s(s(X))) → mark#(X) |
Problem 5: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(dbl(X)) | → | a__dbl#(mark(X)) | | mark#(half(X)) | → | a__half#(mark(X)) |
| a__half#(dbl(X)) | → | mark#(X) | | a__half#(s(s(X))) | → | a__half#(mark(X)) |
| mark#(recip(X)) | → | mark#(X) | | a__sqr#(s(X)) | → | a__dbl#(mark(X)) |
| a__dbl#(s(X)) | → | mark#(X) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(s(X)) | → | mark#(X) | | mark#(add(X1, X2)) | → | mark#(X1) |
| a__add#(s(X), Y) | → | mark#(X) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| mark#(first(X1, X2)) | → | mark#(X2) | | a__sqr#(s(X)) | → | a__add#(a__sqr(mark(X)), a__dbl(mark(X))) |
| a__terms#(N) | → | mark#(N) | | mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | mark#(X) |
| a__add#(0, X) | → | mark#(X) | | mark#(dbl(X)) | → | mark#(X) |
| mark#(terms(X)) | → | mark#(X) | | mark#(sqr(X)) | → | mark#(X) |
| mark#(half(X)) | → | mark#(X) | | mark#(sqr(X)) | → | a__sqr#(mark(X)) |
| mark#(first(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | a__sqr#(mark(X)) |
| a__dbl#(s(X)) | → | a__dbl#(mark(X)) | | a__terms#(N) | → | a__sqr#(mark(N)) |
| a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
Function Precedence
cons < mark = recip < half < terms = a__terms < a__terms# < a__half# = mark# < sqr = a__sqr# = a__sqr < add = a__add < a__add# = dbl = 0 = a__dbl# = a__dbl = nil < a__half = s = a__first = first
Argument Filtering
a__half: collapses to 1
a__terms#: 1
a__add#: 1 2
a__half#: collapses to 1
terms: 1
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__sqr#: 1
mark#: collapses to 1
a__terms: 1
0: all arguments are removed from 0
a__dbl#: 1
a__dbl: 1
s: 1
a__first: 1 2
first: 1 2
a__sqr: 1
nil: all arguments are removed from nil
cons: collapses to 1
Status
a__terms#: lexicographic with permutation 1 → 1
a__add#: lexicographic with permutation 1 → 1 2 → 2
terms: multiset
sqr: lexicographic with permutation 1 → 1
dbl: lexicographic with permutation 1 → 1
add: lexicographic with permutation 1 → 2 2 → 1
a__add: lexicographic with permutation 1 → 2 2 → 1
a__sqr#: lexicographic with permutation 1 → 1
a__terms: multiset
0: multiset
a__dbl#: lexicographic with permutation 1 → 1
a__dbl: lexicographic with permutation 1 → 1
s: lexicographic with permutation 1 → 1
a__first: lexicographic with permutation 1 → 2 2 → 1
first: lexicographic with permutation 1 → 2 2 → 1
a__sqr: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | mark(cons(X1, X2)) → cons(mark(X1), X2) |
| a__first(X1, X2) → first(X1, X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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.
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(dbl(X)) | → | a__dbl#(mark(X)) | | mark#(half(X)) | → | a__half#(mark(X)) |
| a__half#(dbl(X)) | → | mark#(X) | | a__half#(s(s(X))) | → | a__half#(mark(X)) |
| mark#(recip(X)) | → | mark#(X) | | a__sqr#(s(X)) | → | a__dbl#(mark(X)) |
| mark#(add(X1, X2)) | → | mark#(X2) | | mark#(s(X)) | → | mark#(X) |
| mark#(add(X1, X2)) | → | mark#(X1) | | a__add#(s(X), Y) | → | mark#(X) |
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| a__sqr#(s(X)) | → | a__add#(a__sqr(mark(X)), a__dbl(mark(X))) | | a__terms#(N) | → | mark#(N) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | mark#(X) | | a__add#(0, X) | → | mark#(X) |
| mark#(dbl(X)) | → | mark#(X) | | mark#(terms(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | a__sqr#(mark(X)) | | mark#(first(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | a__sqr#(mark(X)) | | a__terms#(N) | → | a__sqr#(mark(N)) |
| a__dbl#(s(X)) | → | a__dbl#(mark(X)) | | a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
The following SCCs where found
| mark#(half(X)) → a__half#(mark(X)) | a__half#(dbl(X)) → mark#(X) |
| a__half#(s(s(X))) → a__half#(mark(X)) | mark#(recip(X)) → mark#(X) |
| mark#(add(X1, X2)) → mark#(X2) | mark#(s(X)) → mark#(X) |
| mark#(add(X1, X2)) → mark#(X1) | a__add#(s(X), Y) → mark#(X) |
| mark#(first(X1, X2)) → mark#(X2) | mark#(terms(X)) → a__terms#(mark(X)) |
| a__sqr#(s(X)) → a__add#(a__sqr(mark(X)), a__dbl(mark(X))) | a__terms#(N) → mark#(N) |
| mark#(add(X1, X2)) → a__add#(mark(X1), mark(X2)) | mark#(cons(X1, X2)) → mark#(X1) |
| a__sqr#(s(X)) → mark#(X) | a__add#(0, X) → mark#(X) |
| mark#(dbl(X)) → mark#(X) | mark#(terms(X)) → mark#(X) |
| mark#(sqr(X)) → mark#(X) | mark#(half(X)) → mark#(X) |
| mark#(sqr(X)) → a__sqr#(mark(X)) | mark#(first(X1, X2)) → mark#(X1) |
| a__sqr#(s(X)) → a__sqr#(mark(X)) | a__terms#(N) → a__sqr#(mark(N)) |
| a__add#(s(X), Y) → a__add#(mark(X), mark(Y)) |
| a__dbl#(s(X)) → a__dbl#(mark(X)) |
Problem 7: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| a__dbl#(s(X)) | → | a__dbl#(mark(X)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Function Precedence
a__half = half < 0 < nil < cons < recip < a__first < first < sqr = mark = a__sqr < dbl = add = a__add = a__dbl# = a__dbl < terms = a__terms = s
Argument Filtering
a__half: collapses to 1
terms: all arguments are removed from terms
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__terms: all arguments are removed from a__terms
0: all arguments are removed from 0
a__dbl#: 1
a__dbl: 1
s: 1
a__first: collapses to 1
first: collapses to 1
a__sqr: 1
cons: collapses to 2
nil: all arguments are removed from nil
Status
terms: multiset
sqr: lexicographic with permutation 1 → 1
dbl: lexicographic with permutation 1 → 1
add: lexicographic with permutation 1 → 1 2 → 2
a__add: lexicographic with permutation 1 → 1 2 → 2
a__terms: multiset
0: multiset
a__dbl#: lexicographic with permutation 1 → 1
a__dbl: lexicographic with permutation 1 → 1
s: lexicographic with permutation 1 → 1
a__sqr: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | a__first(X1, X2) → first(X1, X2) |
| mark(cons(X1, X2)) → cons(mark(X1), X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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.
| a__dbl#(s(X)) → a__dbl#(mark(X)) |
Problem 8: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(half(X)) | → | a__half#(mark(X)) | | a__half#(dbl(X)) | → | mark#(X) |
| a__half#(s(s(X))) | → | a__half#(mark(X)) | | mark#(recip(X)) | → | mark#(X) |
| mark#(add(X1, X2)) | → | mark#(X2) | | mark#(s(X)) | → | mark#(X) |
| mark#(add(X1, X2)) | → | mark#(X1) | | a__add#(s(X), Y) | → | mark#(X) |
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| a__sqr#(s(X)) | → | a__add#(a__sqr(mark(X)), a__dbl(mark(X))) | | a__terms#(N) | → | mark#(N) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | mark#(X) | | a__add#(0, X) | → | mark#(X) |
| mark#(dbl(X)) | → | mark#(X) | | mark#(terms(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | a__sqr#(mark(X)) | | mark#(first(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | a__sqr#(mark(X)) | | a__terms#(N) | → | a__sqr#(mark(N)) |
| a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Function Precedence
half = cons < a__half < recip < a__terms# = terms = sqr = mark = a__sqr# = a__terms = a__sqr < dbl = a__dbl < add = a__add = 0 = nil < a__add# = a__half# = mark# = s = a__first = first
Argument Filtering
a__half: collapses to 1
a__terms#: 1
a__add#: 1 2
a__half#: collapses to 1
terms: 1
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__sqr#: 1
mark#: collapses to 1
a__terms: 1
0: all arguments are removed from 0
a__dbl: 1
s: 1
a__first: 1 2
first: 1 2
a__sqr: 1
nil: all arguments are removed from nil
cons: collapses to 1
Status
a__terms#: lexicographic with permutation 1 → 1
a__add#: lexicographic with permutation 1 → 2 2 → 1
terms: lexicographic with permutation 1 → 1
sqr: lexicographic with permutation 1 → 1
dbl: lexicographic with permutation 1 → 1
add: lexicographic with permutation 1 → 2 2 → 1
a__add: lexicographic with permutation 1 → 2 2 → 1
a__sqr#: lexicographic with permutation 1 → 1
a__terms: lexicographic with permutation 1 → 1
0: multiset
a__dbl: lexicographic with permutation 1 → 1
s: lexicographic with permutation 1 → 1
a__first: lexicographic with permutation 1 → 1 2 → 2
first: lexicographic with permutation 1 → 1 2 → 2
a__sqr: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | mark(cons(X1, X2)) → cons(mark(X1), X2) |
| a__first(X1, X2) → first(X1, X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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.
| a__sqr#(s(X)) → a__add#(a__sqr(mark(X)), a__dbl(mark(X))) |
Problem 9: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| a__terms#(N) | → | mark#(N) | | mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | mark#(X) |
| mark#(half(X)) | → | a__half#(mark(X)) | | a__add#(0, X) | → | mark#(X) |
| mark#(dbl(X)) | → | mark#(X) | | a__half#(dbl(X)) | → | mark#(X) |
| mark#(terms(X)) | → | mark#(X) | | a__half#(s(s(X))) | → | a__half#(mark(X)) |
| mark#(sqr(X)) | → | mark#(X) | | mark#(recip(X)) | → | mark#(X) |
| mark#(half(X)) | → | mark#(X) | | mark#(sqr(X)) | → | a__sqr#(mark(X)) |
| mark#(first(X1, X2)) | → | mark#(X1) | | mark#(add(X1, X2)) | → | mark#(X2) |
| a__sqr#(s(X)) | → | a__sqr#(mark(X)) | | a__terms#(N) | → | a__sqr#(mark(N)) |
| mark#(s(X)) | → | mark#(X) | | mark#(add(X1, X2)) | → | mark#(X1) |
| a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) | | a__add#(s(X), Y) | → | mark#(X) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
Function Precedence
cons < mark = 0 = a__first = first = nil < recip < a__terms# = terms = sqr = a__sqr# = a__terms = a__sqr < add = a__add = mark# < half = dbl = a__dbl < a__half = a__add# = a__half# = s
Argument Filtering
a__half: collapses to 1
a__terms#: 1
a__add#: 1 2
a__half#: collapses to 1
terms: 1
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__sqr#: 1
mark#: collapses to 1
a__terms: 1
0: all arguments are removed from 0
a__dbl: 1
s: 1
a__first: 1 2
first: 1 2
a__sqr: 1
nil: all arguments are removed from nil
cons: collapses to 1
Status
a__terms#: lexicographic with permutation 1 → 1
a__add#: lexicographic with permutation 1 → 2 2 → 1
terms: lexicographic with permutation 1 → 1
sqr: lexicographic with permutation 1 → 1
dbl: multiset
add: lexicographic with permutation 1 → 1 2 → 2
a__add: lexicographic with permutation 1 → 1 2 → 2
a__sqr#: lexicographic with permutation 1 → 1
a__terms: lexicographic with permutation 1 → 1
0: multiset
a__dbl: multiset
s: lexicographic with permutation 1 → 1
a__first: lexicographic with permutation 1 → 1 2 → 2
first: lexicographic with permutation 1 → 1 2 → 2
a__sqr: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | a__first(X1, X2) → first(X1, X2) |
| mark(cons(X1, X2)) → cons(mark(X1), X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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.
Problem 10: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | mark#(X) | | mark#(half(X)) | → | a__half#(mark(X)) |
| a__add#(0, X) | → | mark#(X) | | mark#(dbl(X)) | → | mark#(X) |
| a__half#(dbl(X)) | → | mark#(X) | | mark#(terms(X)) | → | mark#(X) |
| a__half#(s(s(X))) | → | a__half#(mark(X)) | | mark#(sqr(X)) | → | mark#(X) |
| mark#(recip(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | a__sqr#(mark(X)) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(first(X1, X2)) | → | mark#(X1) | | a__sqr#(s(X)) | → | a__sqr#(mark(X)) |
| mark#(s(X)) | → | mark#(X) | | a__terms#(N) | → | a__sqr#(mark(N)) |
| mark#(add(X1, X2)) | → | mark#(X1) | | a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) |
| a__add#(s(X), Y) | → | mark#(X) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Function Precedence
terms = a__terms < a__terms# < a__half# < recip < sqr = a__sqr < 0 = nil < cons < a__half = half = dbl = a__dbl < a__add# = mark = add = a__add = a__sqr# < mark# = s = a__first = first
Argument Filtering
a__half: collapses to 1
a__terms#: 1
a__add#: 1 2
a__half#: collapses to 1
terms: 1
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__sqr#: collapses to 1
mark#: collapses to 1
a__terms: 1
0: all arguments are removed from 0
a__dbl: 1
s: 1
a__first: 1 2
first: 1 2
a__sqr: 1
nil: all arguments are removed from nil
cons: collapses to 1
Status
a__terms#: lexicographic with permutation 1 → 1
a__add#: lexicographic with permutation 1 → 2 2 → 1
terms: lexicographic with permutation 1 → 1
sqr: multiset
dbl: lexicographic with permutation 1 → 1
add: lexicographic with permutation 1 → 2 2 → 1
a__add: lexicographic with permutation 1 → 2 2 → 1
a__terms: lexicographic with permutation 1 → 1
0: multiset
a__dbl: lexicographic with permutation 1 → 1
s: lexicographic with permutation 1 → 1
a__first: multiset
first: multiset
a__sqr: multiset
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | a__first(X1, X2) → first(X1, X2) |
| mark(cons(X1, X2)) → cons(mark(X1), X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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#(first(X1, X2)) → mark#(X2) | mark#(terms(X)) → a__terms#(mark(X)) |
| a__sqr#(s(X)) → mark#(X) | a__add#(0, X) → mark#(X) |
| mark#(dbl(X)) → mark#(X) | a__half#(dbl(X)) → mark#(X) |
| mark#(terms(X)) → mark#(X) | a__half#(s(s(X))) → a__half#(mark(X)) |
| mark#(sqr(X)) → mark#(X) | mark#(sqr(X)) → a__sqr#(mark(X)) |
| mark#(add(X1, X2)) → mark#(X2) | mark#(first(X1, X2)) → mark#(X1) |
| a__terms#(N) → a__sqr#(mark(N)) | mark#(s(X)) → mark#(X) |
| mark#(add(X1, X2)) → mark#(X1) | a__add#(s(X), Y) → a__add#(mark(X), mark(Y)) |
| a__add#(s(X), Y) → mark#(X) |
Problem 11: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(recip(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__sqr#(s(X)) | → | a__sqr#(mark(X)) | | mark#(half(X)) | → | a__half#(mark(X)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
The following SCCs where found
| a__sqr#(s(X)) → a__sqr#(mark(X)) |
| mark#(recip(X)) → mark#(X) | mark#(half(X)) → mark#(X) |
| mark#(cons(X1, X2)) → mark#(X1) |
Problem 12: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| a__sqr#(s(X)) | → | a__sqr#(mark(X)) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
Function Precedence
recip = first < a__sqr# = a__first < 0 = nil < sqr = a__sqr < a__half < dbl = a__dbl < half < add = a__add < terms = mark = a__terms = s = cons
Argument Filtering
a__half: collapses to 1
terms: all arguments are removed from terms
sqr: 1
half: collapses to 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
a__sqr#: 1
a__terms: all arguments are removed from a__terms
0: all arguments are removed from 0
a__dbl: 1
s: 1
a__first: collapses to 1
first: collapses to 1
a__sqr: 1
cons: all arguments are removed from cons
nil: all arguments are removed from nil
Status
terms: multiset
sqr: lexicographic with permutation 1 → 1
dbl: lexicographic with permutation 1 → 1
add: lexicographic with permutation 1 → 2 2 → 1
a__add: lexicographic with permutation 1 → 2 2 → 1
a__sqr#: lexicographic with permutation 1 → 1
a__terms: multiset
0: multiset
a__dbl: lexicographic with permutation 1 → 1
s: lexicographic with permutation 1 → 1
a__sqr: lexicographic with permutation 1 → 1
cons: multiset
nil: multiset
Usable Rules
| a__terms(X) → terms(X) | a__first(X1, X2) → first(X1, X2) |
| mark(cons(X1, X2)) → cons(mark(X1), X2) | a__half(dbl(X)) → mark(X) |
| a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) | mark(half(X)) → a__half(mark(X)) |
| mark(sqr(X)) → a__sqr(mark(X)) | a__half(X) → half(X) |
| a__half(s(s(X))) → s(a__half(mark(X))) | a__first(0, X) → nil |
| a__add(X1, X2) → add(X1, X2) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | mark(nil) → nil |
| a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(X) → dbl(X) |
| mark(terms(X)) → a__terms(mark(X)) | mark(0) → 0 |
| a__half(0) → 0 | mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) |
| a__dbl(0) → 0 | a__sqr(0) → 0 |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__half(s(0)) → 0 |
| a__sqr(X) → sqr(X) | mark(s(X)) → s(mark(X)) |
| mark(recip(X)) → recip(mark(X)) | a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) |
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.
| a__sqr#(s(X)) → a__sqr#(mark(X)) |
Problem 13: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(recip(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
Function Precedence
half = cons < recip < a__half = terms = sqr = mark = dbl = add = a__add = mark# = a__terms = 0 = a__dbl = s = a__first = first = a__sqr = nil
Argument Filtering
a__half: all arguments are removed from a__half
terms: all arguments are removed from terms
sqr: all arguments are removed from sqr
half: collapses to 1
mark: all arguments are removed from mark
dbl: all arguments are removed from dbl
recip: collapses to 1
add: all arguments are removed from add
a__add: all arguments are removed from a__add
mark#: collapses to 1
a__terms: all arguments are removed from a__terms
0: all arguments are removed from 0
a__dbl: 1
s: all arguments are removed from s
a__first: 1 2
first: all arguments are removed from first
a__sqr: all arguments are removed from a__sqr
cons: 1 2
nil: all arguments are removed from nil
Status
a__half: multiset
terms: multiset
sqr: multiset
mark: multiset
dbl: multiset
add: multiset
a__add: multiset
a__terms: multiset
0: multiset
a__dbl: lexicographic with permutation 1 → 1
s: multiset
a__first: lexicographic with permutation 1 → 1 2 → 2
first: multiset
a__sqr: multiset
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.
| mark#(cons(X1, X2)) → mark#(X1) |
Problem 14: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(recip(X)) | → | mark#(X) | | mark#(half(X)) | → | mark#(X) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Function Precedence
half < mark# < recip < a__half = terms = sqr = mark = dbl = add = a__add = a__terms = 0 = a__dbl = s = a__first = first = a__sqr = cons = nil
Argument Filtering
a__half: all arguments are removed from a__half
terms: all arguments are removed from terms
sqr: all arguments are removed from sqr
half: 1
mark: all arguments are removed from mark
dbl: all arguments are removed from dbl
recip: collapses to 1
add: all arguments are removed from add
a__add: all arguments are removed from a__add
mark#: collapses to 1
a__terms: all arguments are removed from a__terms
0: all arguments are removed from 0
a__dbl: 1
s: all arguments are removed from s
a__first: 1 2
first: collapses to 2
a__sqr: all arguments are removed from a__sqr
cons: 1 2
nil: all arguments are removed from nil
Status
a__half: multiset
terms: multiset
sqr: multiset
half: multiset
mark: multiset
dbl: multiset
add: multiset
a__add: multiset
a__terms: multiset
0: multiset
a__dbl: lexicographic with permutation 1 → 1
s: multiset
a__first: lexicographic with permutation 1 → 2 2 → 1
a__sqr: 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.
| mark#(half(X)) → mark#(X) |
Problem 15: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(recip(X)) | → | mark#(X) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(a__dbl(mark(X)))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | a__half(0) | → | 0 |
| a__half(s(0)) | → | 0 | | a__half(s(s(X))) | → | s(a__half(mark(X))) |
| a__half(dbl(X)) | → | mark(X) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(half(X)) | → | a__half(mark(X)) | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(recip(X)) | → | recip(mark(X)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(nil) | → | nil |
| a__terms(X) | → | terms(X) | | a__sqr(X) | → | sqr(X) |
| a__add(X1, X2) | → | add(X1, X2) | | a__dbl(X) | → | dbl(X) |
| a__first(X1, X2) | → | first(X1, X2) | | a__half(X) | → | half(X) |
Original Signature
Termination of terms over the following signature is verified: a__half, terms, sqr, half, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
Function Precedence
mark# < recip < a__half = terms = sqr = half = mark = dbl = add = a__add = a__terms = 0 = a__dbl = s = a__first = first = a__sqr = cons = nil
Argument Filtering
a__half: all arguments are removed from a__half
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: 1
add: 1 2
a__add: all arguments are removed from a__add
mark#: 1
a__terms: all arguments are removed from a__terms
0: all arguments are removed from 0
a__dbl: collapses to 1
s: all arguments are removed from s
a__first: collapses to 1
first: all arguments are removed from first
a__sqr: all arguments are removed from a__sqr
cons: 1 2
nil: all arguments are removed from nil
Status
a__half: multiset
terms: multiset
sqr: multiset
half: multiset
mark: multiset
dbl: multiset
recip: lexicographic with permutation 1 → 1
add: lexicographic with permutation 1 → 2 2 → 1
a__add: multiset
mark#: multiset
a__terms: multiset
0: multiset
s: multiset
first: multiset
a__sqr: 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.
| mark#(recip(X)) → mark#(X) |