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(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(P(x0)) → rotate(cut(CP(guess(x0))))
begin(x(x0)) → rotate(cut(Cx(guess(x0))))
begin(Q(x0)) → rotate(cut(CQ(guess(x0))))
guess(a(x0)) → Ca(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(P(x0)) → CP(guess(x0))
guess(x(x0)) → Cx(guess(x0))
guess(Q(x0)) → CQ(guess(x0))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(P(x0)) → moveleft(BP(wait(x0)))
guess(x(x0)) → moveleft(Bx(wait(x0)))
guess(Q(x0)) → moveleft(BQ(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0))) → moveleft(Ba(Ab(x0)))
CP(moveleft(Ba(x0))) → moveleft(Ba(AP(x0)))
Cx(moveleft(Ba(x0))) → moveleft(Ba(Ax(x0)))
CQ(moveleft(Ba(x0))) → moveleft(Ba(AQ(x0)))
Ca(moveleft(Bb(x0))) → moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
CP(moveleft(Bb(x0))) → moveleft(Bb(AP(x0)))
Cx(moveleft(Bb(x0))) → moveleft(Bb(Ax(x0)))
CQ(moveleft(Bb(x0))) → moveleft(Bb(AQ(x0)))
Ca(moveleft(BP(x0))) → moveleft(BP(Aa(x0)))
Cb(moveleft(BP(x0))) → moveleft(BP(Ab(x0)))
CP(moveleft(BP(x0))) → moveleft(BP(AP(x0)))
Cx(moveleft(BP(x0))) → moveleft(BP(Ax(x0)))
CQ(moveleft(BP(x0))) → moveleft(BP(AQ(x0)))
Ca(moveleft(Bx(x0))) → moveleft(Bx(Aa(x0)))
Cb(moveleft(Bx(x0))) → moveleft(Bx(Ab(x0)))
CP(moveleft(Bx(x0))) → moveleft(Bx(AP(x0)))
Cx(moveleft(Bx(x0))) → moveleft(Bx(Ax(x0)))
CQ(moveleft(Bx(x0))) → moveleft(Bx(AQ(x0)))
Ca(moveleft(BQ(x0))) → moveleft(BQ(Aa(x0)))
Cb(moveleft(BQ(x0))) → moveleft(BQ(Ab(x0)))
CP(moveleft(BQ(x0))) → moveleft(BQ(AP(x0)))
Cx(moveleft(BQ(x0))) → moveleft(BQ(Ax(x0)))
CQ(moveleft(BQ(x0))) → moveleft(BQ(AQ(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(BP(x0))) → DP(cut(goright(x0)))
cut(moveleft(Bx(x0))) → Dx(cut(goright(x0)))
cut(moveleft(BQ(x0))) → DQ(cut(goright(x0)))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(AP(x0)) → CP(goright(x0))
goright(Ax(x0)) → Cx(goright(x0))
goright(AQ(x0)) → CQ(goright(x0))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(P(x0))) → moveleft(BP(wait(x0)))
goright(wait(x(x0))) → moveleft(Bx(wait(x0)))
goright(wait(Q(x0))) → moveleft(BQ(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ca(finish(x0)) → finish(a(x0))
Cb(finish(x0)) → finish(b(x0))
CP(finish(x0)) → finish(P(x0))
Cx(finish(x0)) → finish(x(x0))
CQ(finish(x0)) → finish(Q(x0))
cut(finish(x0)) → finish2(x0)
Da(finish2(x0)) → finish2(a(x0))
Db(finish2(x0)) → finish2(b(x0))
DP(finish2(x0)) → finish2(P(x0))
Dx(finish2(x0)) → finish2(x(x0))
DQ(finish2(x0)) → finish2(Q(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(a(b(b(x0)))) → begin(P(a(b(x0))))
rewrite(a(P(x0))) → begin(P(a(x(x0))))
rewrite(a(x(x0))) → begin(x(a(x0)))
rewrite(b(P(x0))) → begin(b(Q(x0)))
rewrite(Q(x(x0))) → begin(a(Q(x0)))
rewrite(Q(a(x0))) → begin(b(b(a(x0))))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) → rewrite(end(x0))
begin(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(P(x0)) → rotate(cut(CP(guess(x0))))
begin(x(x0)) → rotate(cut(Cx(guess(x0))))
begin(Q(x0)) → rotate(cut(CQ(guess(x0))))
guess(a(x0)) → Ca(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(P(x0)) → CP(guess(x0))
guess(x(x0)) → Cx(guess(x0))
guess(Q(x0)) → CQ(guess(x0))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(P(x0)) → moveleft(BP(wait(x0)))
guess(x(x0)) → moveleft(Bx(wait(x0)))
guess(Q(x0)) → moveleft(BQ(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0))) → moveleft(Ba(Ab(x0)))
CP(moveleft(Ba(x0))) → moveleft(Ba(AP(x0)))
Cx(moveleft(Ba(x0))) → moveleft(Ba(Ax(x0)))
CQ(moveleft(Ba(x0))) → moveleft(Ba(AQ(x0)))
Ca(moveleft(Bb(x0))) → moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
CP(moveleft(Bb(x0))) → moveleft(Bb(AP(x0)))
Cx(moveleft(Bb(x0))) → moveleft(Bb(Ax(x0)))
CQ(moveleft(Bb(x0))) → moveleft(Bb(AQ(x0)))
Ca(moveleft(BP(x0))) → moveleft(BP(Aa(x0)))
Cb(moveleft(BP(x0))) → moveleft(BP(Ab(x0)))
CP(moveleft(BP(x0))) → moveleft(BP(AP(x0)))
Cx(moveleft(BP(x0))) → moveleft(BP(Ax(x0)))
CQ(moveleft(BP(x0))) → moveleft(BP(AQ(x0)))
Ca(moveleft(Bx(x0))) → moveleft(Bx(Aa(x0)))
Cb(moveleft(Bx(x0))) → moveleft(Bx(Ab(x0)))
CP(moveleft(Bx(x0))) → moveleft(Bx(AP(x0)))
Cx(moveleft(Bx(x0))) → moveleft(Bx(Ax(x0)))
CQ(moveleft(Bx(x0))) → moveleft(Bx(AQ(x0)))
Ca(moveleft(BQ(x0))) → moveleft(BQ(Aa(x0)))
Cb(moveleft(BQ(x0))) → moveleft(BQ(Ab(x0)))
CP(moveleft(BQ(x0))) → moveleft(BQ(AP(x0)))
Cx(moveleft(BQ(x0))) → moveleft(BQ(Ax(x0)))
CQ(moveleft(BQ(x0))) → moveleft(BQ(AQ(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(BP(x0))) → DP(cut(goright(x0)))
cut(moveleft(Bx(x0))) → Dx(cut(goright(x0)))
cut(moveleft(BQ(x0))) → DQ(cut(goright(x0)))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(AP(x0)) → CP(goright(x0))
goright(Ax(x0)) → Cx(goright(x0))
goright(AQ(x0)) → CQ(goright(x0))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(P(x0))) → moveleft(BP(wait(x0)))
goright(wait(x(x0))) → moveleft(Bx(wait(x0)))
goright(wait(Q(x0))) → moveleft(BQ(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ca(finish(x0)) → finish(a(x0))
Cb(finish(x0)) → finish(b(x0))
CP(finish(x0)) → finish(P(x0))
Cx(finish(x0)) → finish(x(x0))
CQ(finish(x0)) → finish(Q(x0))
cut(finish(x0)) → finish2(x0)
Da(finish2(x0)) → finish2(a(x0))
Db(finish2(x0)) → finish2(b(x0))
DP(finish2(x0)) → finish2(P(x0))
Dx(finish2(x0)) → finish2(x(x0))
DQ(finish2(x0)) → finish2(Q(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(a(b(b(x0)))) → begin(P(a(b(x0))))
rewrite(a(P(x0))) → begin(P(a(x(x0))))
rewrite(a(x(x0))) → begin(x(a(x0)))
rewrite(b(P(x0))) → begin(b(Q(x0)))
rewrite(Q(x(x0))) → begin(a(Q(x0)))
rewrite(Q(a(x0))) → begin(b(b(a(x0))))