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:
0(*(x1)) → *(1(x1))
1(*(x1)) → 0(#(x1))
#(0(x1)) → 0(#(x1))
#(1(x1)) → 1(#(x1))
#($(x1)) → *($(x1))
#(#(x1)) → #(x1)
#(*(x1)) → *(x1)
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
0(*(x1)) → *(1(x1))
1(*(x1)) → 0(#(x1))
#(0(x1)) → 0(#(x1))
#(1(x1)) → 1(#(x1))
#($(x1)) → *($(x1))
#(#(x1)) → #(x1)
#(*(x1)) → *(x1)
Q is empty.
We use [27] with the following order to prove termination.
Knuth-Bendix order [24] with precedence:
#1 > 11 > 01 > *1
and weight map:
*_1=1
1_1=1
0_1=1
#_1=1
dummyConstant=1
$_1=1