YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a12(a12(a12(a12(x0)))) → x0
a13(a13(a13(a13(x0)))) → x0
a14(a14(a14(a14(x0)))) → x0
a15(a15(a15(a15(x0)))) → x0
a16(a16(a16(a16(x0)))) → x0
a23(a23(a23(a23(x0)))) → x0
a24(a24(a24(a24(x0)))) → x0
a25(a25(a25(a25(x0)))) → x0
a26(a26(a26(a26(x0)))) → x0
a34(a34(a34(a34(x0)))) → x0
a35(a35(a35(a35(x0)))) → x0
a36(a36(a36(a36(x0)))) → x0
a45(a45(a45(a45(x0)))) → x0
a46(a46(a46(a46(x0)))) → x0
a56(a56(a56(a56(x0)))) → x0
a13(a13(x0)) → a12(a12(a23(a23(a12(a12(x0))))))
a14(a14(x0)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x0))))))))))
a15(a15(x0)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x0))))))))))))))
a16(a16(x0)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x0))))))))))))))))))
a24(a24(x0)) → a23(a23(a34(a34(a23(a23(x0))))))
a25(a25(x0)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x0))))))))))
a26(a26(x0)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x0))))))))))))))
a35(a35(x0)) → a34(a34(a45(a45(a34(a34(x0))))))
a36(a36(x0)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x0))))))))))
a46(a46(x0)) → a45(a45(a56(a56(a45(a45(x0))))))
a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x0)))))))))))) → x0
a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x0)))))))))))) → x0
a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x0)))))))))))) → x0
a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x0)))))))))))) → x0
a12(a12(a34(a34(x0)))) → a34(a34(a12(a12(x0))))
a12(a12(a45(a45(x0)))) → a45(a45(a12(a12(x0))))
a12(a12(a56(a56(x0)))) → a56(a56(a12(a12(x0))))
a23(a23(a45(a45(x0)))) → a45(a45(a23(a23(x0))))
a23(a23(a56(a56(x0)))) → a56(a56(a23(a23(x0))))
a34(a34(a56(a56(x0)))) → a56(a56(a34(a34(x0))))

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[a16(x1)] = 6 · x1 + -∞
[a26(x1)] = 4 · x1 + -∞
[a13(x1)] = 4 · x1 + -∞
[a15(x1)] = 4 · x1 + -∞
[a23(x1)] = 0 · x1 + -∞
[a35(x1)] = 2 · x1 + -∞
[a12(x1)] = 1 · x1 + -∞
[a25(x1)] = 5 · x1 + -∞
[a56(x1)] = 0 · x1 + -∞
[a45(x1)] = 2 · x1 + -∞
[a36(x1)] = 4 · x1 + -∞
[a34(x1)] = 0 · x1 + -∞
[a46(x1)] = 6 · x1 + -∞
[a24(x1)] = 2 · x1 + -∞
[a14(x1)] = 4 · x1 + -∞
the rules
a23(a23(a23(a23(x0)))) → x0
a34(a34(a34(a34(x0)))) → x0
a56(a56(a56(a56(x0)))) → x0
a15(a15(x0)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x0))))))))))))))
a16(a16(x0)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x0))))))))))))))))))
a26(a26(x0)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x0))))))))))))))
a35(a35(x0)) → a34(a34(a45(a45(a34(a34(x0))))))
a36(a36(x0)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x0))))))))))
a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x0)))))))))))) → x0
a12(a12(a34(a34(x0)))) → a34(a34(a12(a12(x0))))
a12(a12(a45(a45(x0)))) → a45(a45(a12(a12(x0))))
a12(a12(a56(a56(x0)))) → a56(a56(a12(a12(x0))))
a23(a23(a45(a45(x0)))) → a45(a45(a23(a23(x0))))
a23(a23(a56(a56(x0)))) → a56(a56(a23(a23(x0))))
a34(a34(a56(a56(x0)))) → a56(a56(a34(a34(x0))))
remain.

1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[a16(x1)] = 8 · x1 + -∞
[a26(x1)] = 4 · x1 + -∞
[a15(x1)] = 4 · x1 + -∞
[a23(x1)] = 2 · x1 + -∞
[a35(x1)] = 6 · x1 + -∞
[a12(x1)] = 0 · x1 + -∞
[a56(x1)] = 0 · x1 + -∞
[a45(x1)] = 0 · x1 + -∞
[a36(x1)] = 1 · x1 + -∞
[a34(x1)] = 0 · x1 + -∞
the rules
a34(a34(a34(a34(x0)))) → x0
a56(a56(a56(a56(x0)))) → x0
a15(a15(x0)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x0))))))))))))))
a26(a26(x0)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x0))))))))))))))
a12(a12(a34(a34(x0)))) → a34(a34(a12(a12(x0))))
a12(a12(a45(a45(x0)))) → a45(a45(a12(a12(x0))))
a12(a12(a56(a56(x0)))) → a56(a56(a12(a12(x0))))
a23(a23(a45(a45(x0)))) → a45(a45(a23(a23(x0))))
a23(a23(a56(a56(x0)))) → a56(a56(a23(a23(x0))))
a34(a34(a56(a56(x0)))) → a56(a56(a34(a34(x0))))
remain.

1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[a26(x1)] = 11 · x1 + -∞
[a15(x1)] = 0 · x1 + -∞
[a23(x1)] = 0 · x1 + -∞
[a12(x1)] = 0 · x1 + -∞
[a56(x1)] = 3 · x1 + -∞
[a45(x1)] = 0 · x1 + -∞
[a34(x1)] = 0 · x1 + -∞
the rules
a34(a34(a34(a34(x0)))) → x0
a15(a15(x0)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x0))))))))))))))
a12(a12(a34(a34(x0)))) → a34(a34(a12(a12(x0))))
a12(a12(a45(a45(x0)))) → a45(a45(a12(a12(x0))))
a12(a12(a56(a56(x0)))) → a56(a56(a12(a12(x0))))
a23(a23(a45(a45(x0)))) → a45(a45(a23(a23(x0))))
a23(a23(a56(a56(x0)))) → a56(a56(a23(a23(x0))))
a34(a34(a56(a56(x0)))) → a56(a56(a34(a34(x0))))
remain.

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[a15(x1)] = 8 · x1 + -∞
[a23(x1)] = 0 · x1 + -∞
[a12(x1)] = 0 · x1 + -∞
[a56(x1)] = 0 · x1 + -∞
[a45(x1)] = 0 · x1 + -∞
[a34(x1)] = 0 · x1 + -∞
the rules
a34(a34(a34(a34(x0)))) → x0
a12(a12(a34(a34(x0)))) → a34(a34(a12(a12(x0))))
a12(a12(a45(a45(x0)))) → a45(a45(a12(a12(x0))))
a12(a12(a56(a56(x0)))) → a56(a56(a12(a12(x0))))
a23(a23(a45(a45(x0)))) → a45(a45(a23(a23(x0))))
a23(a23(a56(a56(x0)))) → a56(a56(a23(a23(x0))))
a34(a34(a56(a56(x0)))) → a56(a56(a34(a34(x0))))
remain.

1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1 R is empty

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