YES
Termination w.r.t. Q proof of ../tpdb/SRS/Marche/s6.srs
Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
a12(a12(x1)) → x1
a13(a13(x1)) → x1
a14(a14(x1)) → x1
a15(a15(x1)) → x1
a16(a16(x1)) → x1
a23(a23(x1)) → x1
a24(a24(x1)) → x1
a25(a25(x1)) → x1
a26(a26(x1)) → x1
a34(a34(x1)) → x1
a35(a35(x1)) → x1
a36(a36(x1)) → x1
a45(a45(x1)) → x1
a46(a46(x1)) → x1
a56(a56(x1)) → x1
a13(x1) → a12(a23(a12(x1)))
a14(x1) → a12(a23(a34(a23(a12(x1)))))
a15(x1) → a12(a23(a34(a45(a34(a23(a12(x1)))))))
a16(x1) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
a24(x1) → a23(a34(a23(x1)))
a25(x1) → a23(a34(a45(a34(a23(x1)))))
a26(x1) → a23(a34(a45(a56(a45(a34(a23(x1)))))))
a35(x1) → a34(a45(a34(x1)))
a36(x1) → a34(a45(a56(a45(a34(x1)))))
a46(x1) → a45(a56(a45(x1)))
a12(a23(a12(a23(a12(a23(x1)))))) → x1
a23(a34(a23(a34(a23(a34(x1)))))) → x1
a34(a45(a34(a45(a34(a45(x1)))))) → x1
a45(a56(a45(a56(a45(a56(x1)))))) → x1
a12(a34(x1)) → a34(a12(x1))
a12(a45(x1)) → a45(a12(x1))
a12(a56(x1)) → a56(a12(x1))
a23(a45(x1)) → a45(a23(x1))
a23(a56(x1)) → a56(a23(x1))
a34(a56(x1)) → a56(a34(x1))
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a12(a12(x1)) → x1
a13(a13(x1)) → x1
a14(a14(x1)) → x1
a15(a15(x1)) → x1
a16(a16(x1)) → x1
a23(a23(x1)) → x1
a24(a24(x1)) → x1
a25(a25(x1)) → x1
a26(a26(x1)) → x1
a34(a34(x1)) → x1
a35(a35(x1)) → x1
a36(a36(x1)) → x1
a45(a45(x1)) → x1
a46(a46(x1)) → x1
a56(a56(x1)) → x1
a13(x1) → a12(a23(a12(x1)))
a14(x1) → a12(a23(a34(a23(a12(x1)))))
a15(x1) → a12(a23(a34(a45(a34(a23(a12(x1)))))))
a16(x1) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
a24(x1) → a23(a34(a23(x1)))
a25(x1) → a23(a34(a45(a34(a23(x1)))))
a26(x1) → a23(a34(a45(a56(a45(a34(a23(x1)))))))
a35(x1) → a34(a45(a34(x1)))
a36(x1) → a34(a45(a56(a45(a34(x1)))))
a46(x1) → a45(a56(a45(x1)))
a12(a23(a12(a23(a12(a23(x1)))))) → x1
a23(a34(a23(a34(a23(a34(x1)))))) → x1
a34(a45(a34(a45(a34(a45(x1)))))) → x1
a45(a56(a45(a56(a45(a56(x1)))))) → x1
a12(a34(x1)) → a34(a12(x1))
a12(a45(x1)) → a45(a12(x1))
a12(a56(x1)) → a56(a12(x1))
a23(a45(x1)) → a45(a23(x1))
a23(a56(x1)) → a56(a23(x1))
a34(a56(x1)) → a56(a34(x1))
Q is empty.
We use [27] with the following order to prove termination.
Knuth-Bendix order [24] with precedence:
a231 > a451
a231 > a561
a121 > a451
a121 > a341 > a561
and weight map:
a13_1=4
a36_1=6
a16_1=10
a35_1=4
a15_1=8
a26_1=8
a25_1=6
a14_1=6
a45_1=1
a56_1=1
a23_1=1
a24_1=4
a34_1=1
a12_1=1
a46_1=4
dummyConstant=1