TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60003 ms.
The following DP Processors were used
Problem 1 was processed with processor ReductionPairSAT (3100ms).
| – Problem 2 was processed with processor ReductionPairSAT (2522ms).
| | – Problem 3 was processed with processor DependencyGraph (54ms).
| | | – Problem 4 was processed with processor ReductionPairSAT (2673ms).
| | | | – Problem 5 was processed with processor ReductionPairSAT (3055ms).
| | | | | – Problem 6 was processed with processor ReductionPairSAT (3483ms).
| | | | | | – Problem 7 was processed with processor ReductionPairSAT (2511ms).
| | | | | | | – Problem 8 remains open; application of the following processors failed [DependencyGraph (24ms), ReductionPairSAT (timeout)].
The following open problems remain:
Open Dependency Pair Problem 8
Dependency Pairs
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(x(X1, X2)) | → | mark#(X2) |
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) |
| mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) | | a__plus#(N, s(M)) | → | mark#(N) |
| a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) | | a__x#(N, s(M)) | → | mark#(M) |
| mark#(x(X1, X2)) | → | mark#(X1) | | a__plus#(N, s(M)) | → | mark#(M) |
| mark#(plus(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, x, and, a__and
Problem 1: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | a__x#(N, s(M)) | → | mark#(N) |
| mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) | | mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) |
| a__x#(N, s(M)) | → | mark#(M) | | a__plus#(N, s(M)) | → | mark#(M) |
| mark#(plus(X1, X2)) | → | mark#(X1) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(x(X1, X2)) | → | mark#(X2) | | mark#(plus(X1, X2)) | → | mark#(X2) |
| mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) | | a__and#(tt, X) | → | mark#(X) |
| a__plus#(N, s(M)) | → | mark#(N) | | a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) |
| mark#(s(X)) | → | mark#(X) | | a__x#(N, s(M)) | → | a__plus#(a__x(mark(N), mark(M)), mark(N)) |
| a__plus#(N, 0) | → | mark#(N) | | mark#(x(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, a__and, and, x
Strategy
Function Precedence
a__x# = a__x = x < mark < plus = a__plus < a__and# = mark# = a__and = and = 0 = s = tt = a__plus#
Argument Filtering
plus: 1 2
a__and#: collapses to 2
a__plus: 1 2
a__x#: 1 2
mark: collapses to 1
mark#: collapses to 1
a__and: 1 2
and: 1 2
0: all arguments are removed from 0
s: 1
tt: all arguments are removed from tt
a__plus#: 1 2
a__x: 1 2
x: 1 2
Status
plus: lexicographic with permutation 1 → 2 2 → 1
a__plus: lexicographic with permutation 1 → 2 2 → 1
a__x#: lexicographic with permutation 1 → 2 2 → 1
a__and: lexicographic with permutation 1 → 2 2 → 1
and: lexicographic with permutation 1 → 2 2 → 1
0: multiset
s: lexicographic with permutation 1 → 1
tt: multiset
a__plus#: lexicographic with permutation 1 → 2 2 → 1
a__x: lexicographic with permutation 1 → 2 2 → 1
x: lexicographic with permutation 1 → 2 2 → 1
Usable Rules
| mark(tt) → tt | mark(0) → 0 |
| a__plus(N, 0) → mark(N) | a__plus(X1, X2) → plus(X1, X2) |
| a__and(X1, X2) → and(X1, X2) | a__and(tt, X) → mark(X) |
| a__x(X1, X2) → x(X1, X2) | a__x(N, s(M)) → a__plus(a__x(mark(N), mark(M)), mark(N)) |
| mark(and(X1, X2)) → a__and(mark(X1), X2) | a__plus(N, s(M)) → s(a__plus(mark(N), mark(M))) |
| mark(s(X)) → s(mark(X)) | mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2)) |
| a__x(N, 0) → 0 | mark(x(X1, X2)) → a__x(mark(X1), mark(X2)) |
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 2: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | a__x#(N, s(M)) | → | mark#(N) |
| mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) | | mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) |
| a__x#(N, s(M)) | → | mark#(M) | | a__plus#(N, s(M)) | → | mark#(M) |
| mark#(plus(X1, X2)) | → | mark#(X1) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(x(X1, X2)) | → | mark#(X2) | | mark#(plus(X1, X2)) | → | mark#(X2) |
| mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) | | a__and#(tt, X) | → | mark#(X) |
| a__plus#(N, s(M)) | → | mark#(N) | | a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) |
| a__plus#(N, 0) | → | mark#(N) | | a__x#(N, s(M)) | → | a__plus#(a__x(mark(N), mark(M)), mark(N)) |
| mark#(x(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, x, and, a__and
Strategy
Function Precedence
mark < a__x# = a__x = x < plus = a__plus = a__plus# < a__and# = mark# = a__and = and = 0 = s = tt
Argument Filtering
plus: 1 2
a__and#: collapses to 2
a__plus: 1 2
a__x#: 1 2
mark: collapses to 1
mark#: collapses to 1
a__and: 1 2
and: 1 2
0: all arguments are removed from 0
s: 1
tt: all arguments are removed from tt
a__plus#: 1 2
a__x: 1 2
x: 1 2
Status
plus: lexicographic with permutation 1 → 1 2 → 2
a__plus: lexicographic with permutation 1 → 1 2 → 2
a__x#: lexicographic with permutation 1 → 1 2 → 2
a__and: lexicographic with permutation 1 → 1 2 → 2
and: lexicographic with permutation 1 → 1 2 → 2
0: multiset
s: lexicographic with permutation 1 → 1
tt: multiset
a__plus#: lexicographic with permutation 1 → 1 2 → 2
a__x: lexicographic with permutation 1 → 1 2 → 2
x: lexicographic with permutation 1 → 1 2 → 2
Usable Rules
| mark(tt) → tt | mark(0) → 0 |
| a__plus(N, 0) → mark(N) | a__plus(X1, X2) → plus(X1, X2) |
| a__and(X1, X2) → and(X1, X2) | a__and(tt, X) → mark(X) |
| a__x(X1, X2) → x(X1, X2) | a__x(N, s(M)) → a__plus(a__x(mark(N), mark(M)), mark(N)) |
| mark(and(X1, X2)) → a__and(mark(X1), X2) | a__plus(N, s(M)) → s(a__plus(mark(N), mark(M))) |
| mark(s(X)) → s(mark(X)) | mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2)) |
| a__x(N, 0) → 0 | mark(x(X1, X2)) → a__x(mark(X1), mark(X2)) |
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#(and(X1, X2)) → a__and#(mark(X1), X2) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | a__x#(N, s(M)) | → | mark#(N) |
| mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) | | mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) |
| a__x#(N, s(M)) | → | mark#(M) | | a__plus#(N, s(M)) | → | mark#(M) |
| mark#(plus(X1, X2)) | → | mark#(X1) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(x(X1, X2)) | → | mark#(X2) | | mark#(plus(X1, X2)) | → | mark#(X2) |
| a__and#(tt, X) | → | mark#(X) | | a__plus#(N, s(M)) | → | mark#(N) |
| a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) | | a__x#(N, s(M)) | → | a__plus#(a__x(mark(N), mark(M)), mark(N)) |
| a__plus#(N, 0) | → | mark#(N) | | mark#(x(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, a__and, and, x
Strategy
The following SCCs where found
| a__plus#(N, s(M)) → a__plus#(mark(N), mark(M)) | a__x#(N, s(M)) → mark#(N) |
| mark#(plus(X1, X2)) → a__plus#(mark(X1), mark(X2)) | mark#(x(X1, X2)) → a__x#(mark(X1), mark(X2)) |
| a__x#(N, s(M)) → mark#(M) | a__plus#(N, s(M)) → mark#(M) |
| mark#(plus(X1, X2)) → mark#(X1) | mark#(and(X1, X2)) → mark#(X1) |
| mark#(x(X1, X2)) → mark#(X2) | mark#(plus(X1, X2)) → mark#(X2) |
| a__plus#(N, s(M)) → mark#(N) | a__x#(N, s(M)) → a__x#(mark(N), mark(M)) |
| a__plus#(N, 0) → mark#(N) | a__x#(N, s(M)) → a__plus#(a__x(mark(N), mark(M)), mark(N)) |
| mark#(x(X1, X2)) → mark#(X1) |
Problem 4: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | a__x#(N, s(M)) | → | mark#(N) |
| mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) | | mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) |
| a__x#(N, s(M)) | → | mark#(M) | | mark#(plus(X1, X2)) | → | mark#(X1) |
| a__plus#(N, s(M)) | → | mark#(M) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(x(X1, X2)) | → | mark#(X2) | | mark#(plus(X1, X2)) | → | mark#(X2) |
| a__plus#(N, s(M)) | → | mark#(N) | | a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) |
| a__plus#(N, 0) | → | mark#(N) | | a__x#(N, s(M)) | → | a__plus#(a__x(mark(N), mark(M)), mark(N)) |
| mark#(x(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, a__and, and, x
Strategy
Function Precedence
tt < 0 < a__x# = a__x = x < plus = a__plus = mark = a__plus# < mark# = a__and = and = s
Argument Filtering
plus: 1 2
a__plus: 1 2
a__x#: 1 2
mark: collapses to 1
mark#: collapses to 1
a__and: 1 2
and: 1 2
0: all arguments are removed from 0
s: 1
tt: all arguments are removed from tt
a__plus#: 1 2
a__x: 1 2
x: 1 2
Status
plus: multiset
a__plus: multiset
a__x#: lexicographic with permutation 1 → 1 2 → 2
a__and: lexicographic with permutation 1 → 1 2 → 2
and: lexicographic with permutation 1 → 1 2 → 2
0: multiset
s: lexicographic with permutation 1 → 1
tt: multiset
a__plus#: multiset
a__x: lexicographic with permutation 1 → 1 2 → 2
x: lexicographic with permutation 1 → 1 2 → 2
Usable Rules
| mark(tt) → tt | mark(0) → 0 |
| a__plus(N, 0) → mark(N) | a__plus(X1, X2) → plus(X1, X2) |
| a__and(X1, X2) → and(X1, X2) | a__and(tt, X) → mark(X) |
| a__x(X1, X2) → x(X1, X2) | a__x(N, s(M)) → a__plus(a__x(mark(N), mark(M)), mark(N)) |
| mark(and(X1, X2)) → a__and(mark(X1), X2) | a__plus(N, s(M)) → s(a__plus(mark(N), mark(M))) |
| mark(s(X)) → s(mark(X)) | mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2)) |
| a__x(N, 0) → 0 | mark(x(X1, X2)) → a__x(mark(X1), mark(X2)) |
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__x#(N, s(M)) → mark#(N) |
Problem 5: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) |
| mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) | | a__x#(N, s(M)) | → | mark#(M) |
| mark#(plus(X1, X2)) | → | mark#(X1) | | a__plus#(N, s(M)) | → | mark#(M) |
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(x(X1, X2)) | → | mark#(X2) |
| mark#(plus(X1, X2)) | → | mark#(X2) | | a__plus#(N, s(M)) | → | mark#(N) |
| a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) | | a__plus#(N, 0) | → | mark#(N) |
| a__x#(N, s(M)) | → | a__plus#(a__x(mark(N), mark(M)), mark(N)) | | mark#(x(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, x, and, a__and
Strategy
Function Precedence
tt < mark = 0 < a__x# = a__x = x < plus = a__plus = a__and = and = a__plus# < mark# = s
Argument Filtering
plus: 1 2
a__plus: 1 2
a__x#: 1 2
mark: collapses to 1
mark#: collapses to 1
a__and: 1 2
and: 1 2
0: all arguments are removed from 0
s: 1
tt: all arguments are removed from tt
a__plus#: 1 2
a__x: 1 2
x: 1 2
Status
plus: lexicographic with permutation 1 → 2 2 → 1
a__plus: lexicographic with permutation 1 → 2 2 → 1
a__x#: lexicographic with permutation 1 → 1 2 → 2
a__and: lexicographic with permutation 1 → 1 2 → 2
and: lexicographic with permutation 1 → 1 2 → 2
0: multiset
s: lexicographic with permutation 1 → 1
tt: multiset
a__plus#: lexicographic with permutation 1 → 2 2 → 1
a__x: lexicographic with permutation 1 → 1 2 → 2
x: lexicographic with permutation 1 → 1 2 → 2
Usable Rules
| mark(tt) → tt | mark(0) → 0 |
| a__plus(N, 0) → mark(N) | a__plus(X1, X2) → plus(X1, X2) |
| a__and(X1, X2) → and(X1, X2) | a__and(tt, X) → mark(X) |
| a__x(X1, X2) → x(X1, X2) | a__x(N, s(M)) → a__plus(a__x(mark(N), mark(M)), mark(N)) |
| mark(and(X1, X2)) → a__and(mark(X1), X2) | a__plus(N, s(M)) → s(a__plus(mark(N), mark(M))) |
| mark(s(X)) → s(mark(X)) | mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2)) |
| a__x(N, 0) → 0 | mark(x(X1, X2)) → a__x(mark(X1), mark(X2)) |
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__plus#(N, 0) → mark#(N) |
Problem 6: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) |
| mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) | | a__x#(N, s(M)) | → | mark#(M) |
| mark#(plus(X1, X2)) | → | mark#(X1) | | a__plus#(N, s(M)) | → | mark#(M) |
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(x(X1, X2)) | → | mark#(X2) |
| mark#(plus(X1, X2)) | → | mark#(X2) | | a__plus#(N, s(M)) | → | mark#(N) |
| a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) | | a__x#(N, s(M)) | → | a__plus#(a__x(mark(N), mark(M)), mark(N)) |
| mark#(x(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, a__and, and, x
Strategy
Function Precedence
tt < 0 < a__x# = a__x = x < plus = a__plus = a__plus# < mark = mark# = a__and = and = s
Argument Filtering
plus: 1 2
a__plus: 1 2
a__x#: 1 2
mark: collapses to 1
mark#: collapses to 1
a__and: 1 2
and: 1 2
0: all arguments are removed from 0
s: 1
tt: all arguments are removed from tt
a__plus#: 1 2
a__x: 1 2
x: 1 2
Status
plus: multiset
a__plus: multiset
a__x#: multiset
a__and: lexicographic with permutation 1 → 2 2 → 1
and: lexicographic with permutation 1 → 2 2 → 1
0: multiset
s: multiset
tt: multiset
a__plus#: multiset
a__x: multiset
x: multiset
Usable Rules
| mark(tt) → tt | mark(0) → 0 |
| a__plus(N, 0) → mark(N) | a__plus(X1, X2) → plus(X1, X2) |
| a__and(X1, X2) → and(X1, X2) | a__and(tt, X) → mark(X) |
| a__x(X1, X2) → x(X1, X2) | a__x(N, s(M)) → a__plus(a__x(mark(N), mark(M)), mark(N)) |
| mark(and(X1, X2)) → a__and(mark(X1), X2) | a__plus(N, s(M)) → s(a__plus(mark(N), mark(M))) |
| mark(s(X)) → s(mark(X)) | mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2)) |
| a__x(N, 0) → 0 | mark(x(X1, X2)) → a__x(mark(X1), mark(X2)) |
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__x#(N, s(M)) → a__plus#(a__x(mark(N), mark(M)), mark(N)) |
Problem 7: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(x(X1, X2)) | → | mark#(X2) |
| a__plus#(N, s(M)) | → | a__plus#(mark(N), mark(M)) | | mark#(plus(X1, X2)) | → | mark#(X2) |
| mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) | | mark#(x(X1, X2)) | → | a__x#(mark(X1), mark(X2)) |
| a__plus#(N, s(M)) | → | mark#(N) | | a__x#(N, s(M)) | → | a__x#(mark(N), mark(M)) |
| a__x#(N, s(M)) | → | mark#(M) | | mark#(x(X1, X2)) | → | mark#(X1) |
| a__plus#(N, s(M)) | → | mark#(M) | | mark#(plus(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__and(tt, X) | → | mark(X) | | a__plus(N, 0) | → | mark(N) |
| a__plus(N, s(M)) | → | s(a__plus(mark(N), mark(M))) | | a__x(N, 0) | → | 0 |
| a__x(N, s(M)) | → | a__plus(a__x(mark(N), mark(M)), mark(N)) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | | mark(x(X1, X2)) | → | a__x(mark(X1), mark(X2)) |
| mark(tt) | → | tt | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | a__and(X1, X2) | → | and(X1, X2) |
| a__plus(X1, X2) | → | plus(X1, X2) | | a__x(X1, X2) | → | x(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, mark, a__x, x, and, a__and
Strategy
Function Precedence
tt < a__x = x < plus = a__plus < a__x# = mark = mark# = a__and = and = 0 = s = a__plus#
Argument Filtering
plus: 1 2
a__plus: 1 2
a__x#: collapses to 2
mark: collapses to 1
mark#: collapses to 1
a__and: 1 2
and: 1 2
0: all arguments are removed from 0
s: 1
tt: all arguments are removed from tt
a__plus#: 1 2
a__x: 1 2
x: 1 2
Status
plus: lexicographic with permutation 1 → 2 2 → 1
a__plus: lexicographic with permutation 1 → 2 2 → 1
a__and: lexicographic with permutation 1 → 2 2 → 1
and: lexicographic with permutation 1 → 2 2 → 1
0: multiset
s: lexicographic with permutation 1 → 1
tt: multiset
a__plus#: lexicographic with permutation 1 → 1 2 → 2
a__x: lexicographic with permutation 1 → 2 2 → 1
x: lexicographic with permutation 1 → 2 2 → 1
Usable Rules
| mark(tt) → tt | mark(0) → 0 |
| a__plus(N, 0) → mark(N) | a__plus(X1, X2) → plus(X1, X2) |
| a__and(X1, X2) → and(X1, X2) | a__and(tt, X) → mark(X) |
| a__x(X1, X2) → x(X1, X2) | a__x(N, s(M)) → a__plus(a__x(mark(N), mark(M)), mark(N)) |
| mark(and(X1, X2)) → a__and(mark(X1), X2) | a__plus(N, s(M)) → s(a__plus(mark(N), mark(M))) |
| mark(s(X)) → s(mark(X)) | mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2)) |
| a__x(N, 0) → 0 | mark(x(X1, X2)) → a__x(mark(X1), mark(X2)) |
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#(plus(X1, X2)) → mark#(X2) |