YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

1(2(1(x0))) → 2(0(2(x0)))
0(2(1(x0))) → 1(0(2(x0)))
L(2(1(x0))) → L(1(0(2(x0))))
1(2(0(x0))) → 2(0(1(x0)))
1(2(R(x0))) → 2(0(1(R(x0))))
0(2(0(x0))) → 1(0(1(x0)))
L(2(0(x0))) → L(1(0(1(x0))))
0(2(R(x0))) → 1(0(1(R(x0))))

Proof

1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[R(x1)] =
2 0
0 0
· x1 +
1 0
1 0
[2(x1)] =
1 2
0 0
· x1 +
2 0
3 0
[L(x1)] =
1 1
2 0
· x1 +
1 0
0 0
[1(x1)] =
1 0
0 1
· x1 +
1 0
0 0
[0(x1)] =
1 0
0 0
· x1 +
0 0
0 0
the rules
1(2(1(x0))) → 2(0(2(x0)))
0(2(1(x0))) → 1(0(2(x0)))
1(2(0(x0))) → 2(0(1(x0)))
0(2(0(x0))) → 1(0(1(x0)))
remain.

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight function
prec(0) = 2 weight(0) = 1
prec(2) = 0 weight(2) = 1
prec(1) = 1 weight(1) = 1
all rules could be removed.

1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.