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)ttmark(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)ttmark(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) → ttmark(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) → 0mark(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#(s(X)) → mark#(X)

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)ttmark(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) → ttmark(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) → 0mark(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)ttmark(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)ttmark(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) → ttmark(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) → 0mark(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)ttmark(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) → ttmark(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) → 0mark(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)ttmark(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) → ttmark(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) → 0mark(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)ttmark(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) → ttmark(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) → 0mark(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)