MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

begin(end(x0)) → rewrite(end(x0))
begin(q0(x0)) → rotate(cut(Cq0(guess(x0))))
begin(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(x(x0)) → rotate(cut(Cx(guess(x0))))
begin(q1(x0)) → rotate(cut(Cq1(guess(x0))))
begin(y(x0)) → rotate(cut(Cy(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(q2(x0)) → rotate(cut(Cq2(guess(x0))))
begin(q3(x0)) → rotate(cut(Cq3(guess(x0))))
begin(bl(x0)) → rotate(cut(Cbl(guess(x0))))
begin(q4(x0)) → rotate(cut(Cq4(guess(x0))))
guess(q0(x0)) → Cq0(guess(x0))
guess(a(x0)) → Ca(guess(x0))
guess(x(x0)) → Cx(guess(x0))
guess(q1(x0)) → Cq1(guess(x0))
guess(y(x0)) → Cy(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(q2(x0)) → Cq2(guess(x0))
guess(q3(x0)) → Cq3(guess(x0))
guess(bl(x0)) → Cbl(guess(x0))
guess(q4(x0)) → Cq4(guess(x0))
guess(q0(x0)) → moveleft(Bq0(wait(x0)))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(x(x0)) → moveleft(Bx(wait(x0)))
guess(q1(x0)) → moveleft(Bq1(wait(x0)))
guess(y(x0)) → moveleft(By(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(q2(x0)) → moveleft(Bq2(wait(x0)))
guess(q3(x0)) → moveleft(Bq3(wait(x0)))
guess(bl(x0)) → moveleft(Bbl(wait(x0)))
guess(q4(x0)) → moveleft(Bq4(wait(x0)))
guess(end(x0)) → finish(end(x0))
Cq0(moveleft(Bq0(x0))) → moveleft(Bq0(Aq0(x0)))
Ca(moveleft(Bq0(x0))) → moveleft(Bq0(Aa(x0)))
Cx(moveleft(Bq0(x0))) → moveleft(Bq0(Ax(x0)))
Cq1(moveleft(Bq0(x0))) → moveleft(Bq0(Aq1(x0)))
Cy(moveleft(Bq0(x0))) → moveleft(Bq0(Ay(x0)))
Cb(moveleft(Bq0(x0))) → moveleft(Bq0(Ab(x0)))
Cq2(moveleft(Bq0(x0))) → moveleft(Bq0(Aq2(x0)))
Cq3(moveleft(Bq0(x0))) → moveleft(Bq0(Aq3(x0)))
Cbl(moveleft(Bq0(x0))) → moveleft(Bq0(Abl(x0)))
Cq4(moveleft(Bq0(x0))) → moveleft(Bq0(Aq4(x0)))
Cq0(moveleft(Ba(x0))) → moveleft(Ba(Aq0(x0)))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Cx(moveleft(Ba(x0))) → moveleft(Ba(Ax(x0)))
Cq1(moveleft(Ba(x0))) → moveleft(Ba(Aq1(x0)))
Cy(moveleft(Ba(x0))) → moveleft(Ba(Ay(x0)))
Cb(moveleft(Ba(x0))) → moveleft(Ba(Ab(x0)))
Cq2(moveleft(Ba(x0))) → moveleft(Ba(Aq2(x0)))
Cq3(moveleft(Ba(x0))) → moveleft(Ba(Aq3(x0)))
Cbl(moveleft(Ba(x0))) → moveleft(Ba(Abl(x0)))
Cq4(moveleft(Ba(x0))) → moveleft(Ba(Aq4(x0)))
Cq0(moveleft(Bx(x0))) → moveleft(Bx(Aq0(x0)))
Ca(moveleft(Bx(x0))) → moveleft(Bx(Aa(x0)))
Cx(moveleft(Bx(x0))) → moveleft(Bx(Ax(x0)))
Cq1(moveleft(Bx(x0))) → moveleft(Bx(Aq1(x0)))
Cy(moveleft(Bx(x0))) → moveleft(Bx(Ay(x0)))
Cb(moveleft(Bx(x0))) → moveleft(Bx(Ab(x0)))
Cq2(moveleft(Bx(x0))) → moveleft(Bx(Aq2(x0)))
Cq3(moveleft(Bx(x0))) → moveleft(Bx(Aq3(x0)))
Cbl(moveleft(Bx(x0))) → moveleft(Bx(Abl(x0)))
Cq4(moveleft(Bx(x0))) → moveleft(Bx(Aq4(x0)))
Cq0(moveleft(Bq1(x0))) → moveleft(Bq1(Aq0(x0)))
Ca(moveleft(Bq1(x0))) → moveleft(Bq1(Aa(x0)))
Cx(moveleft(Bq1(x0))) → moveleft(Bq1(Ax(x0)))
Cq1(moveleft(Bq1(x0))) → moveleft(Bq1(Aq1(x0)))
Cy(moveleft(Bq1(x0))) → moveleft(Bq1(Ay(x0)))
Cb(moveleft(Bq1(x0))) → moveleft(Bq1(Ab(x0)))
Cq2(moveleft(Bq1(x0))) → moveleft(Bq1(Aq2(x0)))
Cq3(moveleft(Bq1(x0))) → moveleft(Bq1(Aq3(x0)))
Cbl(moveleft(Bq1(x0))) → moveleft(Bq1(Abl(x0)))
Cq4(moveleft(Bq1(x0))) → moveleft(Bq1(Aq4(x0)))
Cq0(moveleft(By(x0))) → moveleft(By(Aq0(x0)))
Ca(moveleft(By(x0))) → moveleft(By(Aa(x0)))
Cx(moveleft(By(x0))) → moveleft(By(Ax(x0)))
Cq1(moveleft(By(x0))) → moveleft(By(Aq1(x0)))
Cy(moveleft(By(x0))) → moveleft(By(Ay(x0)))
Cb(moveleft(By(x0))) → moveleft(By(Ab(x0)))
Cq2(moveleft(By(x0))) → moveleft(By(Aq2(x0)))
Cq3(moveleft(By(x0))) → moveleft(By(Aq3(x0)))
Cbl(moveleft(By(x0))) → moveleft(By(Abl(x0)))
Cq4(moveleft(By(x0))) → moveleft(By(Aq4(x0)))
Cq0(moveleft(Bb(x0))) → moveleft(Bb(Aq0(x0)))
Ca(moveleft(Bb(x0))) → moveleft(Bb(Aa(x0)))
Cx(moveleft(Bb(x0))) → moveleft(Bb(Ax(x0)))
Cq1(moveleft(Bb(x0))) → moveleft(Bb(Aq1(x0)))
Cy(moveleft(Bb(x0))) → moveleft(Bb(Ay(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
Cq2(moveleft(Bb(x0))) → moveleft(Bb(Aq2(x0)))
Cq3(moveleft(Bb(x0))) → moveleft(Bb(Aq3(x0)))
Cbl(moveleft(Bb(x0))) → moveleft(Bb(Abl(x0)))
Cq4(moveleft(Bb(x0))) → moveleft(Bb(Aq4(x0)))
Cq0(moveleft(Bq2(x0))) → moveleft(Bq2(Aq0(x0)))
Ca(moveleft(Bq2(x0))) → moveleft(Bq2(Aa(x0)))
Cx(moveleft(Bq2(x0))) → moveleft(Bq2(Ax(x0)))
Cq1(moveleft(Bq2(x0))) → moveleft(Bq2(Aq1(x0)))
Cy(moveleft(Bq2(x0))) → moveleft(Bq2(Ay(x0)))
Cb(moveleft(Bq2(x0))) → moveleft(Bq2(Ab(x0)))
Cq2(moveleft(Bq2(x0))) → moveleft(Bq2(Aq2(x0)))
Cq3(moveleft(Bq2(x0))) → moveleft(Bq2(Aq3(x0)))
Cbl(moveleft(Bq2(x0))) → moveleft(Bq2(Abl(x0)))
Cq4(moveleft(Bq2(x0))) → moveleft(Bq2(Aq4(x0)))
Cq0(moveleft(Bq3(x0))) → moveleft(Bq3(Aq0(x0)))
Ca(moveleft(Bq3(x0))) → moveleft(Bq3(Aa(x0)))
Cx(moveleft(Bq3(x0))) → moveleft(Bq3(Ax(x0)))
Cq1(moveleft(Bq3(x0))) → moveleft(Bq3(Aq1(x0)))
Cy(moveleft(Bq3(x0))) → moveleft(Bq3(Ay(x0)))
Cb(moveleft(Bq3(x0))) → moveleft(Bq3(Ab(x0)))
Cq2(moveleft(Bq3(x0))) → moveleft(Bq3(Aq2(x0)))
Cq3(moveleft(Bq3(x0))) → moveleft(Bq3(Aq3(x0)))
Cbl(moveleft(Bq3(x0))) → moveleft(Bq3(Abl(x0)))
Cq4(moveleft(Bq3(x0))) → moveleft(Bq3(Aq4(x0)))
Cq0(moveleft(Bbl(x0))) → moveleft(Bbl(Aq0(x0)))
Ca(moveleft(Bbl(x0))) → moveleft(Bbl(Aa(x0)))
Cx(moveleft(Bbl(x0))) → moveleft(Bbl(Ax(x0)))
Cq1(moveleft(Bbl(x0))) → moveleft(Bbl(Aq1(x0)))
Cy(moveleft(Bbl(x0))) → moveleft(Bbl(Ay(x0)))
Cb(moveleft(Bbl(x0))) → moveleft(Bbl(Ab(x0)))
Cq2(moveleft(Bbl(x0))) → moveleft(Bbl(Aq2(x0)))
Cq3(moveleft(Bbl(x0))) → moveleft(Bbl(Aq3(x0)))
Cbl(moveleft(Bbl(x0))) → moveleft(Bbl(Abl(x0)))
Cq4(moveleft(Bbl(x0))) → moveleft(Bbl(Aq4(x0)))
Cq0(moveleft(Bq4(x0))) → moveleft(Bq4(Aq0(x0)))
Ca(moveleft(Bq4(x0))) → moveleft(Bq4(Aa(x0)))
Cx(moveleft(Bq4(x0))) → moveleft(Bq4(Ax(x0)))
Cq1(moveleft(Bq4(x0))) → moveleft(Bq4(Aq1(x0)))
Cy(moveleft(Bq4(x0))) → moveleft(Bq4(Ay(x0)))
Cb(moveleft(Bq4(x0))) → moveleft(Bq4(Ab(x0)))
Cq2(moveleft(Bq4(x0))) → moveleft(Bq4(Aq2(x0)))
Cq3(moveleft(Bq4(x0))) → moveleft(Bq4(Aq3(x0)))
Cbl(moveleft(Bq4(x0))) → moveleft(Bq4(Abl(x0)))
Cq4(moveleft(Bq4(x0))) → moveleft(Bq4(Aq4(x0)))
cut(moveleft(Bq0(x0))) → Dq0(cut(goright(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Bx(x0))) → Dx(cut(goright(x0)))
cut(moveleft(Bq1(x0))) → Dq1(cut(goright(x0)))
cut(moveleft(By(x0))) → Dy(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(Bq2(x0))) → Dq2(cut(goright(x0)))
cut(moveleft(Bq3(x0))) → Dq3(cut(goright(x0)))
cut(moveleft(Bbl(x0))) → Dbl(cut(goright(x0)))
cut(moveleft(Bq4(x0))) → Dq4(cut(goright(x0)))
goright(Aq0(x0)) → Cq0(goright(x0))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ax(x0)) → Cx(goright(x0))
goright(Aq1(x0)) → Cq1(goright(x0))
goright(Ay(x0)) → Cy(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(Aq2(x0)) → Cq2(goright(x0))
goright(Aq3(x0)) → Cq3(goright(x0))
goright(Abl(x0)) → Cbl(goright(x0))
goright(Aq4(x0)) → Cq4(goright(x0))
goright(wait(q0(x0))) → moveleft(Bq0(wait(x0)))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(x(x0))) → moveleft(Bx(wait(x0)))
goright(wait(q1(x0))) → moveleft(Bq1(wait(x0)))
goright(wait(y(x0))) → moveleft(By(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(q2(x0))) → moveleft(Bq2(wait(x0)))
goright(wait(q3(x0))) → moveleft(Bq3(wait(x0)))
goright(wait(bl(x0))) → moveleft(Bbl(wait(x0)))
goright(wait(q4(x0))) → moveleft(Bq4(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Cq0(finish(x0)) → finish(q0(x0))
Ca(finish(x0)) → finish(a(x0))
Cx(finish(x0)) → finish(x(x0))
Cq1(finish(x0)) → finish(q1(x0))
Cy(finish(x0)) → finish(y(x0))
Cb(finish(x0)) → finish(b(x0))
Cq2(finish(x0)) → finish(q2(x0))
Cq3(finish(x0)) → finish(q3(x0))
Cbl(finish(x0)) → finish(bl(x0))
Cq4(finish(x0)) → finish(q4(x0))
cut(finish(x0)) → finish2(x0)
Dq0(finish2(x0)) → finish2(q0(x0))
Da(finish2(x0)) → finish2(a(x0))
Dx(finish2(x0)) → finish2(x(x0))
Dq1(finish2(x0)) → finish2(q1(x0))
Dy(finish2(x0)) → finish2(y(x0))
Db(finish2(x0)) → finish2(b(x0))
Dq2(finish2(x0)) → finish2(q2(x0))
Dq3(finish2(x0)) → finish2(q3(x0))
Dbl(finish2(x0)) → finish2(bl(x0))
Dq4(finish2(x0)) → finish2(q4(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(q0(a(x0))) → begin(x(q1(x0)))
rewrite(q1(a(x0))) → begin(a(q1(x0)))
rewrite(q1(y(x0))) → begin(y(q1(x0)))
rewrite(a(q1(b(x0)))) → begin(q2(a(y(x0))))
rewrite(a(q2(a(x0)))) → begin(q2(a(a(x0))))
rewrite(a(q2(y(x0)))) → begin(q2(a(y(x0))))
rewrite(y(q1(b(x0)))) → begin(q2(y(y(x0))))
rewrite(y(q2(a(x0)))) → begin(q2(y(a(x0))))
rewrite(y(q2(y(x0)))) → begin(q2(y(y(x0))))
rewrite(q2(x(x0))) → begin(x(q0(x0)))
rewrite(q0(y(x0))) → begin(y(q3(x0)))
rewrite(q3(y(x0))) → begin(y(q3(x0)))
rewrite(q3(bl(x0))) → begin(bl(q4(x0)))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) → rewrite(end(x0))
begin(q0(x0)) → rotate(cut(Cq0(guess(x0))))
begin(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(x(x0)) → rotate(cut(Cx(guess(x0))))
begin(q1(x0)) → rotate(cut(Cq1(guess(x0))))
begin(y(x0)) → rotate(cut(Cy(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(q2(x0)) → rotate(cut(Cq2(guess(x0))))
begin(q3(x0)) → rotate(cut(Cq3(guess(x0))))
begin(bl(x0)) → rotate(cut(Cbl(guess(x0))))
begin(q4(x0)) → rotate(cut(Cq4(guess(x0))))
guess(q0(x0)) → Cq0(guess(x0))
guess(a(x0)) → Ca(guess(x0))
guess(x(x0)) → Cx(guess(x0))
guess(q1(x0)) → Cq1(guess(x0))
guess(y(x0)) → Cy(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(q2(x0)) → Cq2(guess(x0))
guess(q3(x0)) → Cq3(guess(x0))
guess(bl(x0)) → Cbl(guess(x0))
guess(q4(x0)) → Cq4(guess(x0))
guess(q0(x0)) → moveleft(Bq0(wait(x0)))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(x(x0)) → moveleft(Bx(wait(x0)))
guess(q1(x0)) → moveleft(Bq1(wait(x0)))
guess(y(x0)) → moveleft(By(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(q2(x0)) → moveleft(Bq2(wait(x0)))
guess(q3(x0)) → moveleft(Bq3(wait(x0)))
guess(bl(x0)) → moveleft(Bbl(wait(x0)))
guess(q4(x0)) → moveleft(Bq4(wait(x0)))
guess(end(x0)) → finish(end(x0))
Cq0(moveleft(Bq0(x0))) → moveleft(Bq0(Aq0(x0)))
Ca(moveleft(Bq0(x0))) → moveleft(Bq0(Aa(x0)))
Cx(moveleft(Bq0(x0))) → moveleft(Bq0(Ax(x0)))
Cq1(moveleft(Bq0(x0))) → moveleft(Bq0(Aq1(x0)))
Cy(moveleft(Bq0(x0))) → moveleft(Bq0(Ay(x0)))
Cb(moveleft(Bq0(x0))) → moveleft(Bq0(Ab(x0)))
Cq2(moveleft(Bq0(x0))) → moveleft(Bq0(Aq2(x0)))
Cq3(moveleft(Bq0(x0))) → moveleft(Bq0(Aq3(x0)))
Cbl(moveleft(Bq0(x0))) → moveleft(Bq0(Abl(x0)))
Cq4(moveleft(Bq0(x0))) → moveleft(Bq0(Aq4(x0)))
Cq0(moveleft(Ba(x0))) → moveleft(Ba(Aq0(x0)))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Cx(moveleft(Ba(x0))) → moveleft(Ba(Ax(x0)))
Cq1(moveleft(Ba(x0))) → moveleft(Ba(Aq1(x0)))
Cy(moveleft(Ba(x0))) → moveleft(Ba(Ay(x0)))
Cb(moveleft(Ba(x0))) → moveleft(Ba(Ab(x0)))
Cq2(moveleft(Ba(x0))) → moveleft(Ba(Aq2(x0)))
Cq3(moveleft(Ba(x0))) → moveleft(Ba(Aq3(x0)))
Cbl(moveleft(Ba(x0))) → moveleft(Ba(Abl(x0)))
Cq4(moveleft(Ba(x0))) → moveleft(Ba(Aq4(x0)))
Cq0(moveleft(Bx(x0))) → moveleft(Bx(Aq0(x0)))
Ca(moveleft(Bx(x0))) → moveleft(Bx(Aa(x0)))
Cx(moveleft(Bx(x0))) → moveleft(Bx(Ax(x0)))
Cq1(moveleft(Bx(x0))) → moveleft(Bx(Aq1(x0)))
Cy(moveleft(Bx(x0))) → moveleft(Bx(Ay(x0)))
Cb(moveleft(Bx(x0))) → moveleft(Bx(Ab(x0)))
Cq2(moveleft(Bx(x0))) → moveleft(Bx(Aq2(x0)))
Cq3(moveleft(Bx(x0))) → moveleft(Bx(Aq3(x0)))
Cbl(moveleft(Bx(x0))) → moveleft(Bx(Abl(x0)))
Cq4(moveleft(Bx(x0))) → moveleft(Bx(Aq4(x0)))
Cq0(moveleft(Bq1(x0))) → moveleft(Bq1(Aq0(x0)))
Ca(moveleft(Bq1(x0))) → moveleft(Bq1(Aa(x0)))
Cx(moveleft(Bq1(x0))) → moveleft(Bq1(Ax(x0)))
Cq1(moveleft(Bq1(x0))) → moveleft(Bq1(Aq1(x0)))
Cy(moveleft(Bq1(x0))) → moveleft(Bq1(Ay(x0)))
Cb(moveleft(Bq1(x0))) → moveleft(Bq1(Ab(x0)))
Cq2(moveleft(Bq1(x0))) → moveleft(Bq1(Aq2(x0)))
Cq3(moveleft(Bq1(x0))) → moveleft(Bq1(Aq3(x0)))
Cbl(moveleft(Bq1(x0))) → moveleft(Bq1(Abl(x0)))
Cq4(moveleft(Bq1(x0))) → moveleft(Bq1(Aq4(x0)))
Cq0(moveleft(By(x0))) → moveleft(By(Aq0(x0)))
Ca(moveleft(By(x0))) → moveleft(By(Aa(x0)))
Cx(moveleft(By(x0))) → moveleft(By(Ax(x0)))
Cq1(moveleft(By(x0))) → moveleft(By(Aq1(x0)))
Cy(moveleft(By(x0))) → moveleft(By(Ay(x0)))
Cb(moveleft(By(x0))) → moveleft(By(Ab(x0)))
Cq2(moveleft(By(x0))) → moveleft(By(Aq2(x0)))
Cq3(moveleft(By(x0))) → moveleft(By(Aq3(x0)))
Cbl(moveleft(By(x0))) → moveleft(By(Abl(x0)))
Cq4(moveleft(By(x0))) → moveleft(By(Aq4(x0)))
Cq0(moveleft(Bb(x0))) → moveleft(Bb(Aq0(x0)))
Ca(moveleft(Bb(x0))) → moveleft(Bb(Aa(x0)))
Cx(moveleft(Bb(x0))) → moveleft(Bb(Ax(x0)))
Cq1(moveleft(Bb(x0))) → moveleft(Bb(Aq1(x0)))
Cy(moveleft(Bb(x0))) → moveleft(Bb(Ay(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
Cq2(moveleft(Bb(x0))) → moveleft(Bb(Aq2(x0)))
Cq3(moveleft(Bb(x0))) → moveleft(Bb(Aq3(x0)))
Cbl(moveleft(Bb(x0))) → moveleft(Bb(Abl(x0)))
Cq4(moveleft(Bb(x0))) → moveleft(Bb(Aq4(x0)))
Cq0(moveleft(Bq2(x0))) → moveleft(Bq2(Aq0(x0)))
Ca(moveleft(Bq2(x0))) → moveleft(Bq2(Aa(x0)))
Cx(moveleft(Bq2(x0))) → moveleft(Bq2(Ax(x0)))
Cq1(moveleft(Bq2(x0))) → moveleft(Bq2(Aq1(x0)))
Cy(moveleft(Bq2(x0))) → moveleft(Bq2(Ay(x0)))
Cb(moveleft(Bq2(x0))) → moveleft(Bq2(Ab(x0)))
Cq2(moveleft(Bq2(x0))) → moveleft(Bq2(Aq2(x0)))
Cq3(moveleft(Bq2(x0))) → moveleft(Bq2(Aq3(x0)))
Cbl(moveleft(Bq2(x0))) → moveleft(Bq2(Abl(x0)))
Cq4(moveleft(Bq2(x0))) → moveleft(Bq2(Aq4(x0)))
Cq0(moveleft(Bq3(x0))) → moveleft(Bq3(Aq0(x0)))
Ca(moveleft(Bq3(x0))) → moveleft(Bq3(Aa(x0)))
Cx(moveleft(Bq3(x0))) → moveleft(Bq3(Ax(x0)))
Cq1(moveleft(Bq3(x0))) → moveleft(Bq3(Aq1(x0)))
Cy(moveleft(Bq3(x0))) → moveleft(Bq3(Ay(x0)))
Cb(moveleft(Bq3(x0))) → moveleft(Bq3(Ab(x0)))
Cq2(moveleft(Bq3(x0))) → moveleft(Bq3(Aq2(x0)))
Cq3(moveleft(Bq3(x0))) → moveleft(Bq3(Aq3(x0)))
Cbl(moveleft(Bq3(x0))) → moveleft(Bq3(Abl(x0)))
Cq4(moveleft(Bq3(x0))) → moveleft(Bq3(Aq4(x0)))
Cq0(moveleft(Bbl(x0))) → moveleft(Bbl(Aq0(x0)))
Ca(moveleft(Bbl(x0))) → moveleft(Bbl(Aa(x0)))
Cx(moveleft(Bbl(x0))) → moveleft(Bbl(Ax(x0)))
Cq1(moveleft(Bbl(x0))) → moveleft(Bbl(Aq1(x0)))
Cy(moveleft(Bbl(x0))) → moveleft(Bbl(Ay(x0)))
Cb(moveleft(Bbl(x0))) → moveleft(Bbl(Ab(x0)))
Cq2(moveleft(Bbl(x0))) → moveleft(Bbl(Aq2(x0)))
Cq3(moveleft(Bbl(x0))) → moveleft(Bbl(Aq3(x0)))
Cbl(moveleft(Bbl(x0))) → moveleft(Bbl(Abl(x0)))
Cq4(moveleft(Bbl(x0))) → moveleft(Bbl(Aq4(x0)))
Cq0(moveleft(Bq4(x0))) → moveleft(Bq4(Aq0(x0)))
Ca(moveleft(Bq4(x0))) → moveleft(Bq4(Aa(x0)))
Cx(moveleft(Bq4(x0))) → moveleft(Bq4(Ax(x0)))
Cq1(moveleft(Bq4(x0))) → moveleft(Bq4(Aq1(x0)))
Cy(moveleft(Bq4(x0))) → moveleft(Bq4(Ay(x0)))
Cb(moveleft(Bq4(x0))) → moveleft(Bq4(Ab(x0)))
Cq2(moveleft(Bq4(x0))) → moveleft(Bq4(Aq2(x0)))
Cq3(moveleft(Bq4(x0))) → moveleft(Bq4(Aq3(x0)))
Cbl(moveleft(Bq4(x0))) → moveleft(Bq4(Abl(x0)))
Cq4(moveleft(Bq4(x0))) → moveleft(Bq4(Aq4(x0)))
cut(moveleft(Bq0(x0))) → Dq0(cut(goright(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Bx(x0))) → Dx(cut(goright(x0)))
cut(moveleft(Bq1(x0))) → Dq1(cut(goright(x0)))
cut(moveleft(By(x0))) → Dy(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(Bq2(x0))) → Dq2(cut(goright(x0)))
cut(moveleft(Bq3(x0))) → Dq3(cut(goright(x0)))
cut(moveleft(Bbl(x0))) → Dbl(cut(goright(x0)))
cut(moveleft(Bq4(x0))) → Dq4(cut(goright(x0)))
goright(Aq0(x0)) → Cq0(goright(x0))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ax(x0)) → Cx(goright(x0))
goright(Aq1(x0)) → Cq1(goright(x0))
goright(Ay(x0)) → Cy(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(Aq2(x0)) → Cq2(goright(x0))
goright(Aq3(x0)) → Cq3(goright(x0))
goright(Abl(x0)) → Cbl(goright(x0))
goright(Aq4(x0)) → Cq4(goright(x0))
goright(wait(q0(x0))) → moveleft(Bq0(wait(x0)))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(x(x0))) → moveleft(Bx(wait(x0)))
goright(wait(q1(x0))) → moveleft(Bq1(wait(x0)))
goright(wait(y(x0))) → moveleft(By(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(q2(x0))) → moveleft(Bq2(wait(x0)))
goright(wait(q3(x0))) → moveleft(Bq3(wait(x0)))
goright(wait(bl(x0))) → moveleft(Bbl(wait(x0)))
goright(wait(q4(x0))) → moveleft(Bq4(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Cq0(finish(x0)) → finish(q0(x0))
Ca(finish(x0)) → finish(a(x0))
Cx(finish(x0)) → finish(x(x0))
Cq1(finish(x0)) → finish(q1(x0))
Cy(finish(x0)) → finish(y(x0))
Cb(finish(x0)) → finish(b(x0))
Cq2(finish(x0)) → finish(q2(x0))
Cq3(finish(x0)) → finish(q3(x0))
Cbl(finish(x0)) → finish(bl(x0))
Cq4(finish(x0)) → finish(q4(x0))
cut(finish(x0)) → finish2(x0)
Dq0(finish2(x0)) → finish2(q0(x0))
Da(finish2(x0)) → finish2(a(x0))
Dx(finish2(x0)) → finish2(x(x0))
Dq1(finish2(x0)) → finish2(q1(x0))
Dy(finish2(x0)) → finish2(y(x0))
Db(finish2(x0)) → finish2(b(x0))
Dq2(finish2(x0)) → finish2(q2(x0))
Dq3(finish2(x0)) → finish2(q3(x0))
Dbl(finish2(x0)) → finish2(bl(x0))
Dq4(finish2(x0)) → finish2(q4(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(q0(a(x0))) → begin(x(q1(x0)))
rewrite(q1(a(x0))) → begin(a(q1(x0)))
rewrite(q1(y(x0))) → begin(y(q1(x0)))
rewrite(a(q1(b(x0)))) → begin(q2(a(y(x0))))
rewrite(a(q2(a(x0)))) → begin(q2(a(a(x0))))
rewrite(a(q2(y(x0)))) → begin(q2(a(y(x0))))
rewrite(y(q1(b(x0)))) → begin(q2(y(y(x0))))
rewrite(y(q2(a(x0)))) → begin(q2(y(a(x0))))
rewrite(y(q2(y(x0)))) → begin(q2(y(y(x0))))
rewrite(q2(x(x0))) → begin(x(q0(x0)))
rewrite(q0(y(x0))) → begin(y(q3(x0)))
rewrite(q3(y(x0))) → begin(y(q3(x0)))
rewrite(q3(bl(x0))) → begin(bl(q4(x0)))