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(r0(x0)) → rotate(cut(Cr0(guess(x0))))
begin(0(x0)) → rotate(cut(C0(guess(x0))))
begin(1(x0)) → rotate(cut(C1(guess(x0))))
begin(m(x0)) → rotate(cut(Cm(guess(x0))))
begin(r1(x0)) → rotate(cut(Cr1(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(qr(x0)) → rotate(cut(Cqr(guess(x0))))
begin(ql(x0)) → rotate(cut(Cql(guess(x0))))
guess(r0(x0)) → Cr0(guess(x0))
guess(0(x0)) → C0(guess(x0))
guess(1(x0)) → C1(guess(x0))
guess(m(x0)) → Cm(guess(x0))
guess(r1(x0)) → Cr1(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(qr(x0)) → Cqr(guess(x0))
guess(ql(x0)) → Cql(guess(x0))
guess(r0(x0)) → moveleft(Br0(wait(x0)))
guess(0(x0)) → moveleft(B0(wait(x0)))
guess(1(x0)) → moveleft(B1(wait(x0)))
guess(m(x0)) → moveleft(Bm(wait(x0)))
guess(r1(x0)) → moveleft(Br1(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(qr(x0)) → moveleft(Bqr(wait(x0)))
guess(ql(x0)) → moveleft(Bql(wait(x0)))
guess(end(x0)) → finish(end(x0))
Cr0(moveleft(Br0(x0))) → moveleft(Br0(Ar0(x0)))
C0(moveleft(Br0(x0))) → moveleft(Br0(A0(x0)))
C1(moveleft(Br0(x0))) → moveleft(Br0(A1(x0)))
Cm(moveleft(Br0(x0))) → moveleft(Br0(Am(x0)))
Cr1(moveleft(Br0(x0))) → moveleft(Br0(Ar1(x0)))
Cb(moveleft(Br0(x0))) → moveleft(Br0(Ab(x0)))
Cqr(moveleft(Br0(x0))) → moveleft(Br0(Aqr(x0)))
Cql(moveleft(Br0(x0))) → moveleft(Br0(Aql(x0)))
Cr0(moveleft(B0(x0))) → moveleft(B0(Ar0(x0)))
C0(moveleft(B0(x0))) → moveleft(B0(A0(x0)))
C1(moveleft(B0(x0))) → moveleft(B0(A1(x0)))
Cm(moveleft(B0(x0))) → moveleft(B0(Am(x0)))
Cr1(moveleft(B0(x0))) → moveleft(B0(Ar1(x0)))
Cb(moveleft(B0(x0))) → moveleft(B0(Ab(x0)))
Cqr(moveleft(B0(x0))) → moveleft(B0(Aqr(x0)))
Cql(moveleft(B0(x0))) → moveleft(B0(Aql(x0)))
Cr0(moveleft(B1(x0))) → moveleft(B1(Ar0(x0)))
C0(moveleft(B1(x0))) → moveleft(B1(A0(x0)))
C1(moveleft(B1(x0))) → moveleft(B1(A1(x0)))
Cm(moveleft(B1(x0))) → moveleft(B1(Am(x0)))
Cr1(moveleft(B1(x0))) → moveleft(B1(Ar1(x0)))
Cb(moveleft(B1(x0))) → moveleft(B1(Ab(x0)))
Cqr(moveleft(B1(x0))) → moveleft(B1(Aqr(x0)))
Cql(moveleft(B1(x0))) → moveleft(B1(Aql(x0)))
Cr0(moveleft(Bm(x0))) → moveleft(Bm(Ar0(x0)))
C0(moveleft(Bm(x0))) → moveleft(Bm(A0(x0)))
C1(moveleft(Bm(x0))) → moveleft(Bm(A1(x0)))
Cm(moveleft(Bm(x0))) → moveleft(Bm(Am(x0)))
Cr1(moveleft(Bm(x0))) → moveleft(Bm(Ar1(x0)))
Cb(moveleft(Bm(x0))) → moveleft(Bm(Ab(x0)))
Cqr(moveleft(Bm(x0))) → moveleft(Bm(Aqr(x0)))
Cql(moveleft(Bm(x0))) → moveleft(Bm(Aql(x0)))
Cr0(moveleft(Br1(x0))) → moveleft(Br1(Ar0(x0)))
C0(moveleft(Br1(x0))) → moveleft(Br1(A0(x0)))
C1(moveleft(Br1(x0))) → moveleft(Br1(A1(x0)))
Cm(moveleft(Br1(x0))) → moveleft(Br1(Am(x0)))
Cr1(moveleft(Br1(x0))) → moveleft(Br1(Ar1(x0)))
Cb(moveleft(Br1(x0))) → moveleft(Br1(Ab(x0)))
Cqr(moveleft(Br1(x0))) → moveleft(Br1(Aqr(x0)))
Cql(moveleft(Br1(x0))) → moveleft(Br1(Aql(x0)))
Cr0(moveleft(Bb(x0))) → moveleft(Bb(Ar0(x0)))
C0(moveleft(Bb(x0))) → moveleft(Bb(A0(x0)))
C1(moveleft(Bb(x0))) → moveleft(Bb(A1(x0)))
Cm(moveleft(Bb(x0))) → moveleft(Bb(Am(x0)))
Cr1(moveleft(Bb(x0))) → moveleft(Bb(Ar1(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
Cqr(moveleft(Bb(x0))) → moveleft(Bb(Aqr(x0)))
Cql(moveleft(Bb(x0))) → moveleft(Bb(Aql(x0)))
Cr0(moveleft(Bqr(x0))) → moveleft(Bqr(Ar0(x0)))
C0(moveleft(Bqr(x0))) → moveleft(Bqr(A0(x0)))
C1(moveleft(Bqr(x0))) → moveleft(Bqr(A1(x0)))
Cm(moveleft(Bqr(x0))) → moveleft(Bqr(Am(x0)))
Cr1(moveleft(Bqr(x0))) → moveleft(Bqr(Ar1(x0)))
Cb(moveleft(Bqr(x0))) → moveleft(Bqr(Ab(x0)))
Cqr(moveleft(Bqr(x0))) → moveleft(Bqr(Aqr(x0)))
Cql(moveleft(Bqr(x0))) → moveleft(Bqr(Aql(x0)))
Cr0(moveleft(Bql(x0))) → moveleft(Bql(Ar0(x0)))
C0(moveleft(Bql(x0))) → moveleft(Bql(A0(x0)))
C1(moveleft(Bql(x0))) → moveleft(Bql(A1(x0)))
Cm(moveleft(Bql(x0))) → moveleft(Bql(Am(x0)))
Cr1(moveleft(Bql(x0))) → moveleft(Bql(Ar1(x0)))
Cb(moveleft(Bql(x0))) → moveleft(Bql(Ab(x0)))
Cqr(moveleft(Bql(x0))) → moveleft(Bql(Aqr(x0)))
Cql(moveleft(Bql(x0))) → moveleft(Bql(Aql(x0)))
cut(moveleft(Br0(x0))) → Dr0(cut(goright(x0)))
cut(moveleft(B0(x0))) → D0(cut(goright(x0)))
cut(moveleft(B1(x0))) → D1(cut(goright(x0)))
cut(moveleft(Bm(x0))) → Dm(cut(goright(x0)))
cut(moveleft(Br1(x0))) → Dr1(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(Bqr(x0))) → Dqr(cut(goright(x0)))
cut(moveleft(Bql(x0))) → Dql(cut(goright(x0)))
goright(Ar0(x0)) → Cr0(goright(x0))
goright(A0(x0)) → C0(goright(x0))
goright(A1(x0)) → C1(goright(x0))
goright(Am(x0)) → Cm(goright(x0))
goright(Ar1(x0)) → Cr1(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(Aqr(x0)) → Cqr(goright(x0))
goright(Aql(x0)) → Cql(goright(x0))
goright(wait(r0(x0))) → moveleft(Br0(wait(x0)))
goright(wait(0(x0))) → moveleft(B0(wait(x0)))
goright(wait(1(x0))) → moveleft(B1(wait(x0)))
goright(wait(m(x0))) → moveleft(Bm(wait(x0)))
goright(wait(r1(x0))) → moveleft(Br1(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(qr(x0))) → moveleft(Bqr(wait(x0)))
goright(wait(ql(x0))) → moveleft(Bql(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Cr0(finish(x0)) → finish(r0(x0))
C0(finish(x0)) → finish(0(x0))
C1(finish(x0)) → finish(1(x0))
Cm(finish(x0)) → finish(m(x0))
Cr1(finish(x0)) → finish(r1(x0))
Cb(finish(x0)) → finish(b(x0))
Cqr(finish(x0)) → finish(qr(x0))
Cql(finish(x0)) → finish(ql(x0))
cut(finish(x0)) → finish2(x0)
Dr0(finish2(x0)) → finish2(r0(x0))
D0(finish2(x0)) → finish2(0(x0))
D1(finish2(x0)) → finish2(1(x0))
Dm(finish2(x0)) → finish2(m(x0))
Dr1(finish2(x0)) → finish2(r1(x0))
Db(finish2(x0)) → finish2(b(x0))
Dqr(finish2(x0)) → finish2(qr(x0))
Dql(finish2(x0)) → finish2(ql(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(r0(0(x0))) → begin(0(r0(x0)))
rewrite(r0(1(x0))) → begin(1(r0(x0)))
rewrite(r0(m(x0))) → begin(m(r0(x0)))
rewrite(r1(0(x0))) → begin(0(r1(x0)))
rewrite(r1(1(x0))) → begin(1(r1(x0)))
rewrite(r1(m(x0))) → begin(m(r1(x0)))
rewrite(r0(b(x0))) → begin(qr(0(b(x0))))
rewrite(r1(b(x0))) → begin(qr(1(b(x0))))
rewrite(0(qr(x0))) → begin(qr(0(x0)))
rewrite(1(qr(x0))) → begin(qr(1(x0)))
rewrite(m(qr(x0))) → begin(ql(m(x0)))
rewrite(0(ql(x0))) → begin(ql(0(x0)))
rewrite(1(ql(x0))) → begin(ql(1(x0)))
rewrite(b(ql(0(x0)))) → begin(0(b(r0(x0))))
rewrite(b(ql(1(x0)))) → begin(1(b(r1(x0))))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) → rewrite(end(x0))
begin(r0(x0)) → rotate(cut(Cr0(guess(x0))))
begin(0(x0)) → rotate(cut(C0(guess(x0))))
begin(1(x0)) → rotate(cut(C1(guess(x0))))
begin(m(x0)) → rotate(cut(Cm(guess(x0))))
begin(r1(x0)) → rotate(cut(Cr1(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(qr(x0)) → rotate(cut(Cqr(guess(x0))))
begin(ql(x0)) → rotate(cut(Cql(guess(x0))))
guess(r0(x0)) → Cr0(guess(x0))
guess(0(x0)) → C0(guess(x0))
guess(1(x0)) → C1(guess(x0))
guess(m(x0)) → Cm(guess(x0))
guess(r1(x0)) → Cr1(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(qr(x0)) → Cqr(guess(x0))
guess(ql(x0)) → Cql(guess(x0))
guess(r0(x0)) → moveleft(Br0(wait(x0)))
guess(0(x0)) → moveleft(B0(wait(x0)))
guess(1(x0)) → moveleft(B1(wait(x0)))
guess(m(x0)) → moveleft(Bm(wait(x0)))
guess(r1(x0)) → moveleft(Br1(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(qr(x0)) → moveleft(Bqr(wait(x0)))
guess(ql(x0)) → moveleft(Bql(wait(x0)))
guess(end(x0)) → finish(end(x0))
Cr0(moveleft(Br0(x0))) → moveleft(Br0(Ar0(x0)))
C0(moveleft(Br0(x0))) → moveleft(Br0(A0(x0)))
C1(moveleft(Br0(x0))) → moveleft(Br0(A1(x0)))
Cm(moveleft(Br0(x0))) → moveleft(Br0(Am(x0)))
Cr1(moveleft(Br0(x0))) → moveleft(Br0(Ar1(x0)))
Cb(moveleft(Br0(x0))) → moveleft(Br0(Ab(x0)))
Cqr(moveleft(Br0(x0))) → moveleft(Br0(Aqr(x0)))
Cql(moveleft(Br0(x0))) → moveleft(Br0(Aql(x0)))
Cr0(moveleft(B0(x0))) → moveleft(B0(Ar0(x0)))
C0(moveleft(B0(x0))) → moveleft(B0(A0(x0)))
C1(moveleft(B0(x0))) → moveleft(B0(A1(x0)))
Cm(moveleft(B0(x0))) → moveleft(B0(Am(x0)))
Cr1(moveleft(B0(x0))) → moveleft(B0(Ar1(x0)))
Cb(moveleft(B0(x0))) → moveleft(B0(Ab(x0)))
Cqr(moveleft(B0(x0))) → moveleft(B0(Aqr(x0)))
Cql(moveleft(B0(x0))) → moveleft(B0(Aql(x0)))
Cr0(moveleft(B1(x0))) → moveleft(B1(Ar0(x0)))
C0(moveleft(B1(x0))) → moveleft(B1(A0(x0)))
C1(moveleft(B1(x0))) → moveleft(B1(A1(x0)))
Cm(moveleft(B1(x0))) → moveleft(B1(Am(x0)))
Cr1(moveleft(B1(x0))) → moveleft(B1(Ar1(x0)))
Cb(moveleft(B1(x0))) → moveleft(B1(Ab(x0)))
Cqr(moveleft(B1(x0))) → moveleft(B1(Aqr(x0)))
Cql(moveleft(B1(x0))) → moveleft(B1(Aql(x0)))
Cr0(moveleft(Bm(x0))) → moveleft(Bm(Ar0(x0)))
C0(moveleft(Bm(x0))) → moveleft(Bm(A0(x0)))
C1(moveleft(Bm(x0))) → moveleft(Bm(A1(x0)))
Cm(moveleft(Bm(x0))) → moveleft(Bm(Am(x0)))
Cr1(moveleft(Bm(x0))) → moveleft(Bm(Ar1(x0)))
Cb(moveleft(Bm(x0))) → moveleft(Bm(Ab(x0)))
Cqr(moveleft(Bm(x0))) → moveleft(Bm(Aqr(x0)))
Cql(moveleft(Bm(x0))) → moveleft(Bm(Aql(x0)))
Cr0(moveleft(Br1(x0))) → moveleft(Br1(Ar0(x0)))
C0(moveleft(Br1(x0))) → moveleft(Br1(A0(x0)))
C1(moveleft(Br1(x0))) → moveleft(Br1(A1(x0)))
Cm(moveleft(Br1(x0))) → moveleft(Br1(Am(x0)))
Cr1(moveleft(Br1(x0))) → moveleft(Br1(Ar1(x0)))
Cb(moveleft(Br1(x0))) → moveleft(Br1(Ab(x0)))
Cqr(moveleft(Br1(x0))) → moveleft(Br1(Aqr(x0)))
Cql(moveleft(Br1(x0))) → moveleft(Br1(Aql(x0)))
Cr0(moveleft(Bb(x0))) → moveleft(Bb(Ar0(x0)))
C0(moveleft(Bb(x0))) → moveleft(Bb(A0(x0)))
C1(moveleft(Bb(x0))) → moveleft(Bb(A1(x0)))
Cm(moveleft(Bb(x0))) → moveleft(Bb(Am(x0)))
Cr1(moveleft(Bb(x0))) → moveleft(Bb(Ar1(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
Cqr(moveleft(Bb(x0))) → moveleft(Bb(Aqr(x0)))
Cql(moveleft(Bb(x0))) → moveleft(Bb(Aql(x0)))
Cr0(moveleft(Bqr(x0))) → moveleft(Bqr(Ar0(x0)))
C0(moveleft(Bqr(x0))) → moveleft(Bqr(A0(x0)))
C1(moveleft(Bqr(x0))) → moveleft(Bqr(A1(x0)))
Cm(moveleft(Bqr(x0))) → moveleft(Bqr(Am(x0)))
Cr1(moveleft(Bqr(x0))) → moveleft(Bqr(Ar1(x0)))
Cb(moveleft(Bqr(x0))) → moveleft(Bqr(Ab(x0)))
Cqr(moveleft(Bqr(x0))) → moveleft(Bqr(Aqr(x0)))
Cql(moveleft(Bqr(x0))) → moveleft(Bqr(Aql(x0)))
Cr0(moveleft(Bql(x0))) → moveleft(Bql(Ar0(x0)))
C0(moveleft(Bql(x0))) → moveleft(Bql(A0(x0)))
C1(moveleft(Bql(x0))) → moveleft(Bql(A1(x0)))
Cm(moveleft(Bql(x0))) → moveleft(Bql(Am(x0)))
Cr1(moveleft(Bql(x0))) → moveleft(Bql(Ar1(x0)))
Cb(moveleft(Bql(x0))) → moveleft(Bql(Ab(x0)))
Cqr(moveleft(Bql(x0))) → moveleft(Bql(Aqr(x0)))
Cql(moveleft(Bql(x0))) → moveleft(Bql(Aql(x0)))
cut(moveleft(Br0(x0))) → Dr0(cut(goright(x0)))
cut(moveleft(B0(x0))) → D0(cut(goright(x0)))
cut(moveleft(B1(x0))) → D1(cut(goright(x0)))
cut(moveleft(Bm(x0))) → Dm(cut(goright(x0)))
cut(moveleft(Br1(x0))) → Dr1(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(Bqr(x0))) → Dqr(cut(goright(x0)))
cut(moveleft(Bql(x0))) → Dql(cut(goright(x0)))
goright(Ar0(x0)) → Cr0(goright(x0))
goright(A0(x0)) → C0(goright(x0))
goright(A1(x0)) → C1(goright(x0))
goright(Am(x0)) → Cm(goright(x0))
goright(Ar1(x0)) → Cr1(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(Aqr(x0)) → Cqr(goright(x0))
goright(Aql(x0)) → Cql(goright(x0))
goright(wait(r0(x0))) → moveleft(Br0(wait(x0)))
goright(wait(0(x0))) → moveleft(B0(wait(x0)))
goright(wait(1(x0))) → moveleft(B1(wait(x0)))
goright(wait(m(x0))) → moveleft(Bm(wait(x0)))
goright(wait(r1(x0))) → moveleft(Br1(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(qr(x0))) → moveleft(Bqr(wait(x0)))
goright(wait(ql(x0))) → moveleft(Bql(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Cr0(finish(x0)) → finish(r0(x0))
C0(finish(x0)) → finish(0(x0))
C1(finish(x0)) → finish(1(x0))
Cm(finish(x0)) → finish(m(x0))
Cr1(finish(x0)) → finish(r1(x0))
Cb(finish(x0)) → finish(b(x0))
Cqr(finish(x0)) → finish(qr(x0))
Cql(finish(x0)) → finish(ql(x0))
cut(finish(x0)) → finish2(x0)
Dr0(finish2(x0)) → finish2(r0(x0))
D0(finish2(x0)) → finish2(0(x0))
D1(finish2(x0)) → finish2(1(x0))
Dm(finish2(x0)) → finish2(m(x0))
Dr1(finish2(x0)) → finish2(r1(x0))
Db(finish2(x0)) → finish2(b(x0))
Dqr(finish2(x0)) → finish2(qr(x0))
Dql(finish2(x0)) → finish2(ql(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(r0(0(x0))) → begin(0(r0(x0)))
rewrite(r0(1(x0))) → begin(1(r0(x0)))
rewrite(r0(m(x0))) → begin(m(r0(x0)))
rewrite(r1(0(x0))) → begin(0(r1(x0)))
rewrite(r1(1(x0))) → begin(1(r1(x0)))
rewrite(r1(m(x0))) → begin(m(r1(x0)))
rewrite(r0(b(x0))) → begin(qr(0(b(x0))))
rewrite(r1(b(x0))) → begin(qr(1(b(x0))))
rewrite(0(qr(x0))) → begin(qr(0(x0)))
rewrite(1(qr(x0))) → begin(qr(1(x0)))
rewrite(m(qr(x0))) → begin(ql(m(x0)))
rewrite(0(ql(x0))) → begin(ql(0(x0)))
rewrite(1(ql(x0))) → begin(ql(1(x0)))
rewrite(b(ql(0(x0)))) → begin(0(b(r0(x0))))
rewrite(b(ql(1(x0)))) → begin(1(b(r1(x0))))