Termination w.r.t. Q proof of /tmp/tmpiNADe-/dup09.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:

0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(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(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(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₁ > 0₁ > *₁

and weight map:

*_1=2
1_1=2
0_1=2
#_1=2
dummyConstant=1
$_1=1