TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60006 ms.
The following DP Processors were used
Problem 1 was processed with processor ReductionPairSAT (7062ms).
| – Problem 2 was processed with processor DependencyGraph (251ms).
| | – Problem 3 was processed with processor ReductionPairSAT (7843ms).
| | | – Problem 4 was processed with processor DependencyGraph (208ms).
| | | | – Problem 5 was processed with processor ReductionPairSAT (1409ms).
| | | | – Problem 6 remains open; application of the following processors failed [ReductionPairSAT (2084ms)].
The following open problems remain:
Open Dependency Pair Problem 6
Dependency Pairs
| 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#(recip(X)) | → | mark#(X) | | mark#(sqr(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) |
| a__add#(s(X), Y) | → | mark#(Y) | | 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)) | | 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(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) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
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#(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)) |
| 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#(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)) | | 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(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) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, nil, cons
Strategy
Function Precedence
recip = 0 < a__terms# = terms = sqr = a__sqr# = a__terms = a__sqr < dbl = a__dbl# = a__dbl = a__first = first < nil < mark = add = a__add < a__add# = mark# = s = a__first# = cons
Argument Filtering
a__terms#: 1
a__add#: 1 2
terms: 1
sqr: 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
mark#: collapses to 1
a__sqr#: 1
a__terms: 1
0: all arguments are removed from 0
a__dbl#: 1
a__dbl: 1
s: 1
a__first#: collapses to 2
a__first: 1 2
first: 1 2
a__sqr: 1
cons: collapses to 1
nil: all arguments are removed from nil
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: multiset
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#: multiset
a__dbl: multiset
s: multiset
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) | a__first(X1, X2) → first(X1, X2) |
| mark(cons(X1, X2)) → cons(mark(X1), X2) | mark(terms(X)) → a__terms(mark(X)) |
| mark(0) → 0 | a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) |
| mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) | mark(sqr(X)) → a__sqr(mark(X)) |
| a__first(0, X) → nil | a__dbl(0) → 0 |
| a__sqr(0) → 0 | a__add(X1, X2) → add(X1, X2) |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | a__sqr(X) → sqr(X) |
| mark(recip(X)) → recip(mark(X)) | mark(s(X)) → s(mark(X)) |
| mark(nil) → nil | a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) |
| a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(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#(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#(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#(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#(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)) | | 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(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) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, 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#(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)) |
| 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#(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#(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)) |
| 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#(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)) | | 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(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) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, cons, nil
Strategy
Function Precedence
cons < a__terms# = terms = a__terms < recip = a__dbl# < sqr = a__sqr# = a__sqr < add = a__add < a__add# = mark < dbl = mark# = 0 = a__dbl < s = a__first = first = nil
Argument Filtering
a__terms#: 1
a__add#: 1 2
terms: 1
sqr: 1
mark: collapses to 1
dbl: 1
recip: collapses to 1
add: 1 2
a__add: 1 2
mark#: collapses to 1
a__sqr#: 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
cons: collapses to 1
nil: all arguments are removed from nil
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__sqr#: multiset
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 → 2 2 → 1
first: lexicographic with permutation 1 → 2 2 → 1
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) | mark(terms(X)) → a__terms(mark(X)) |
| mark(0) → 0 | a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) |
| mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) | mark(sqr(X)) → a__sqr(mark(X)) |
| a__first(0, X) → nil | a__dbl(0) → 0 |
| a__sqr(0) → 0 | a__add(X1, X2) → add(X1, X2) |
| a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) | a__dbl(s(X)) → s(s(a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | a__sqr(X) → sqr(X) |
| mark(recip(X)) → recip(mark(X)) | mark(s(X)) → s(mark(X)) |
| mark(nil) → nil | a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) |
| a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__add(0, X) → mark(X) | a__dbl(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.
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(dbl(X)) | → | a__dbl#(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) | | 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)) | | 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#(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)) | | 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(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) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, nil, cons
Strategy
The following SCCs where found
| 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#(recip(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)) |
| a__add#(s(X), Y) → mark#(Y) | mark#(add(X1, X2)) → mark#(X1) |
| a__add#(s(X), Y) → a__add#(mark(X), mark(Y)) | a__add#(s(X), Y) → mark#(X) |
| a__dbl#(s(X)) → a__dbl#(mark(X)) |
Problem 5: 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)) | | 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(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) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, mark, recip, add, a__add, a__terms, 0, s, a__dbl, a__first, first, a__sqr, nil, cons
Strategy
Function Precedence
0 < recip < a__first < first < sqr = dbl = a__dbl = a__sqr = nil < mark = add = a__add = a__dbl# < terms = a__terms = s = cons
Argument Filtering
terms: all arguments are removed from terms
sqr: 1
mark: collapses to 1
dbl: 1
recip: all arguments are removed from recip
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
first: collapses to 1
a__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
recip: multiset
add: lexicographic with permutation 1 → 2 2 → 1
a__add: lexicographic with permutation 1 → 2 2 → 1
a__terms: multiset
0: multiset
a__dbl#: 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) | mark(cons(X1, X2)) → cons(mark(X1), X2) |
| a__first(X1, X2) → first(X1, X2) | mark(terms(X)) → a__terms(mark(X)) |
| mark(0) → 0 | a__add(s(X), Y) → s(a__add(mark(X), mark(Y))) |
| mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) | mark(sqr(X)) → a__sqr(mark(X)) |
| a__first(0, X) → nil | a__dbl(0) → 0 |
| a__sqr(0) → 0 | a__add(X1, X2) → add(X1, X2) |
| a__dbl(s(X)) → s(s(a__dbl(mark(X)))) | a__sqr(s(X)) → s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) |
| mark(dbl(X)) → a__dbl(mark(X)) | a__sqr(X) → sqr(X) |
| mark(recip(X)) → recip(mark(X)) | mark(s(X)) → s(mark(X)) |
| mark(nil) → nil | a__terms(N) → cons(recip(a__sqr(mark(N))), terms(s(N))) |
| a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z)) | mark(add(X1, X2)) → a__add(mark(X1), mark(X2)) |
| a__dbl(X) → dbl(X) | a__add(0, X) → mark(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.
| a__dbl#(s(X)) → a__dbl#(mark(X)) |