YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

1(1(x0)) → 4(3(x0))
1(2(x0)) → 2(1(x0))
2(2(x0)) → 1(1(1(x0)))
3(3(x0)) → 5(6(x0))
3(4(x0)) → 1(1(x0))
4(4(x0)) → 3(x0)
5(5(x0)) → 6(2(x0))
5(6(x0)) → 1(2(x0))
6(6(x0)) → 2(1(x0))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
1(1(x0)) → 3(4(x0))
2(1(x0)) → 1(2(x0))
2(2(x0)) → 1(1(1(x0)))
3(3(x0)) → 6(5(x0))
4(3(x0)) → 1(1(x0))
4(4(x0)) → 3(x0)
5(5(x0)) → 2(6(x0))
6(5(x0)) → 2(1(x0))
6(6(x0)) → 1(2(x0))

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
1#(1(x0)) → 4#(x0)
1#(1(x0)) → 3#(4(x0))
2#(1(x0)) → 2#(x0)
2#(1(x0)) → 1#(2(x0))
2#(2(x0)) → 1#(x0)
2#(2(x0)) → 1#(1(x0))
2#(2(x0)) → 1#(1(1(x0)))
3#(3(x0)) → 5#(x0)
3#(3(x0)) → 6#(5(x0))
4#(3(x0)) → 1#(x0)
4#(3(x0)) → 1#(1(x0))
4#(4(x0)) → 3#(x0)
5#(5(x0)) → 6#(x0)
5#(5(x0)) → 2#(6(x0))
6#(5(x0)) → 1#(x0)
6#(5(x0)) → 2#(1(x0))
6#(6(x0)) → 2#(x0)
6#(6(x0)) → 1#(2(x0))

1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals
[6(x1)] = 1 · x1 + 20
[3#(x1)] = 1 · x1 + 10
[3(x1)] = 1 · x1 + 21
[2(x1)] = 1 · x1 + 24
[5(x1)] = 1 · x1 + 22
[5#(x1)] = 1 · x1 + 24
[1(x1)] = 1 · x1 + 16
[4#(x1)] = 1 · x1 + 0
[6#(x1)] = 1 · x1 + 9
[2#(x1)] = 1 · x1 + 13
[1#(x1)] = 1 · x1 + 5
[4(x1)] = 1 · x1 + 11
the pairs
1#(1(x0)) → 3#(4(x0))
2#(1(x0)) → 1#(2(x0))
2#(2(x0)) → 1#(1(1(x0)))
3#(3(x0)) → 6#(5(x0))
4#(3(x0)) → 1#(1(x0))
6#(6(x0)) → 1#(2(x0))
remain.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.