YES
Termination w.r.t. Q proof of ../tpdb/SRS/Marche/turing_add.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:
1(q0(1(x1))) → 0(1(q1(x1)))
1(q0(0(x1))) → 0(0(q1(x1)))
1(q1(1(x1))) → 1(1(q1(x1)))
1(q1(0(x1))) → 1(0(q1(x1)))
0(q1(x1)) → q2(1(x1))
1(q2(x1)) → q2(1(x1))
0(q2(x1)) → 0(q0(x1))
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
1(q0(1(x1))) → 0(1(q1(x1)))
1(q0(0(x1))) → 0(0(q1(x1)))
1(q1(1(x1))) → 1(1(q1(x1)))
1(q1(0(x1))) → 1(0(q1(x1)))
0(q1(x1)) → q2(1(x1))
1(q2(x1)) → q2(1(x1))
0(q2(x1)) → 0(q0(x1))
Q is empty.
We use [27] with the following order to prove termination.
Knuth-Bendix order [24] with precedence:
q11 > 11 > 01 > q21 > q01
and weight map:
q0_1=2
q2_1=2
0_1=2
1_1=2
q1_1=2
dummyConstant=1