YES

The TRS could be proven terminating. The proof took 2147 ms.

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (737ms).
 | – Problem 2 was processed with processor PolynomialOrderingProcessor (764ms).
 |    | – Problem 3 was processed with processor DependencyGraph (1ms).
 |    |    | – Problem 4 was processed with processor PolynomialOrderingProcessor (25ms).

Problem 1: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

1#(1(x))0#(x)1#(0(x))0#(0(0(1(x))))
1#(0(x))1#(x)0#(1(x))1#(x)
1#(1(x))0#(0(x))1#(0(x))0#(1(x))
1#(1(x))0#(0(0(0(x))))1#(0(x))0#(0(1(x)))
1#(1(x))0#(0(0(x)))0#(0(x))0#(x)

Rewrite Rules

1(0(x))0(0(0(1(x))))0(1(x))1(x)
1(1(x))0(0(0(0(x))))0(0(x))0(x)

Original Signature

Termination of terms over the following signature is verified: 1, 0

Strategy


Polynomial Interpretation

Improved Usable rules

1(0(x))0(0(0(1(x))))0(1(x))1(x)
0(0(x))0(x)1(1(x))0(0(0(0(x))))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

1#(1(x))0#(x)1#(1(x))0#(0(x))
1#(1(x))0#(0(0(0(x))))1#(1(x))0#(0(0(x)))

Problem 2: PolynomialOrderingProcessor



Dependency Pair Problem

Dependency Pairs

0#(1(x))1#(x)1#(0(x))1#(x)
1#(0(x))0#(0(0(1(x))))1#(0(x))0#(1(x))
1#(0(x))0#(0(1(x)))0#(0(x))0#(x)

Rewrite Rules

1(0(x))0(0(0(1(x))))0(1(x))1(x)
1(1(x))0(0(0(0(x))))0(0(x))0(x)

Original Signature

Termination of terms over the following signature is verified: 1, 0

Strategy


Polynomial Interpretation

Improved Usable rules

1(0(x))0(0(0(1(x))))0(1(x))1(x)
0(0(x))0(x)1(1(x))0(0(0(0(x))))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

1#(0(x))0#(0(0(1(x))))1#(0(x))1#(x)
1#(0(x))0#(1(x))1#(0(x))0#(0(1(x)))

Problem 3: DependencyGraph



Dependency Pair Problem

Dependency Pairs

0#(1(x))1#(x)0#(0(x))0#(x)

Rewrite Rules

1(0(x))0(0(0(1(x))))0(1(x))1(x)
1(1(x))0(0(0(0(x))))0(0(x))0(x)

Original Signature

Termination of terms over the following signature is verified: 1, 0

Strategy


The following SCCs where found

0#(0(x)) → 0#(x)

Problem 4: PolynomialOrderingProcessor



Dependency Pair Problem

Dependency Pairs

0#(0(x))0#(x)

Rewrite Rules

1(0(x))0(0(0(1(x))))0(1(x))1(x)
1(1(x))0(0(0(0(x))))0(0(x))0(x)

Original Signature

Termination of terms over the following signature is verified: 1, 0

Strategy


Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

0#(0(x))0#(x)