YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(x0))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(x0)))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))

Proof

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
0#(1(2(1(x0)))) → 0#(1(2(x0)))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(x0))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(x0)))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))))))))
0#(1(2(1(x0)))) → 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))))))))

1.1 Reduction Pair Processor

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the naturals
[2(x1)] =
0 0 0 0
0 0 0 0
0 1 0 0
1 0 0 0
· x1 +
0 0 0 0
0 0 0 0
0 0 0 0
0 0 0 0
[0#(x1)] =
0 0 1 1
0 0 0 0
0 0 0 0
0 0 0 0
· x1 +
0 0 0 0
0 0 0 0
0 0 0 0
0 0 0 0
[1(x1)] =
0 1 0 0
1 0 0 0
0 0 0 1
0 0 1 0
· x1 +
0 0 0 0
1 0 0 0
0 0 0 0
0 0 0 0
[0(x1)] =
0 0 0 0
0 0 0 1
0 1 0 0
0 0 1 1
· x1 +
0 0 0 0
0 0 0 0
0 0 0 0
0 0 0 0
all pairs could be removed.

1.1.1 P is empty

There are no pairs anymore.