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:
q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))
Q is empty.
We use [27] with the following order to prove termination.
Knuth-Bendix order [24] with precedence:
q11 > 1'1 > q21
q11 > 01 > q21
0'1 > q21
q31 > 1'1 > q21
and weight map:
q1_1=30
1_1=15
q0_1=27
0'_1=7
q4_1=9
1'_1=8
q2_1=29
b_1=1
0_1=17
dummyConstant=1
q3_1=18