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(h(x0)) → rotate(cut(Ch(guess(x0))))
begin(1(x0)) → rotate(cut(C1(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(s(x0)) → rotate(cut(Cs(guess(x0))))
begin(t(x0)) → rotate(cut(Ct(guess(x0))))
guess(h(x0)) → Ch(guess(x0))
guess(1(x0)) → C1(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(s(x0)) → Cs(guess(x0))
guess(t(x0)) → Ct(guess(x0))
guess(h(x0)) → moveleft(Bh(wait(x0)))
guess(1(x0)) → moveleft(B1(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(s(x0)) → moveleft(Bs(wait(x0)))
guess(t(x0)) → moveleft(Bt(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ch(moveleft(Bh(x0))) → moveleft(Bh(Ah(x0)))
C1(moveleft(Bh(x0))) → moveleft(Bh(A1(x0)))
Cb(moveleft(Bh(x0))) → moveleft(Bh(Ab(x0)))
Cs(moveleft(Bh(x0))) → moveleft(Bh(As(x0)))
Ct(moveleft(Bh(x0))) → moveleft(Bh(At(x0)))
Ch(moveleft(B1(x0))) → moveleft(B1(Ah(x0)))
C1(moveleft(B1(x0))) → moveleft(B1(A1(x0)))
Cb(moveleft(B1(x0))) → moveleft(B1(Ab(x0)))
Cs(moveleft(B1(x0))) → moveleft(B1(As(x0)))
Ct(moveleft(B1(x0))) → moveleft(B1(At(x0)))
Ch(moveleft(Bb(x0))) → moveleft(Bb(Ah(x0)))
C1(moveleft(Bb(x0))) → moveleft(Bb(A1(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
Cs(moveleft(Bb(x0))) → moveleft(Bb(As(x0)))
Ct(moveleft(Bb(x0))) → moveleft(Bb(At(x0)))
Ch(moveleft(Bs(x0))) → moveleft(Bs(Ah(x0)))
C1(moveleft(Bs(x0))) → moveleft(Bs(A1(x0)))
Cb(moveleft(Bs(x0))) → moveleft(Bs(Ab(x0)))
Cs(moveleft(Bs(x0))) → moveleft(Bs(As(x0)))
Ct(moveleft(Bs(x0))) → moveleft(Bs(At(x0)))
Ch(moveleft(Bt(x0))) → moveleft(Bt(Ah(x0)))
C1(moveleft(Bt(x0))) → moveleft(Bt(A1(x0)))
Cb(moveleft(Bt(x0))) → moveleft(Bt(Ab(x0)))
Cs(moveleft(Bt(x0))) → moveleft(Bt(As(x0)))
Ct(moveleft(Bt(x0))) → moveleft(Bt(At(x0)))
cut(moveleft(Bh(x0))) → Dh(cut(goright(x0)))
cut(moveleft(B1(x0))) → D1(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(Bs(x0))) → Ds(cut(goright(x0)))
cut(moveleft(Bt(x0))) → Dt(cut(goright(x0)))
goright(Ah(x0)) → Ch(goright(x0))
goright(A1(x0)) → C1(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(As(x0)) → Cs(goright(x0))
goright(At(x0)) → Ct(goright(x0))
goright(wait(h(x0))) → moveleft(Bh(wait(x0)))
goright(wait(1(x0))) → moveleft(B1(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(s(x0))) → moveleft(Bs(wait(x0)))
goright(wait(t(x0))) → moveleft(Bt(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ch(finish(x0)) → finish(h(x0))
C1(finish(x0)) → finish(1(x0))
Cb(finish(x0)) → finish(b(x0))
Cs(finish(x0)) → finish(s(x0))
Ct(finish(x0)) → finish(t(x0))
cut(finish(x0)) → finish2(x0)
Dh(finish2(x0)) → finish2(h(x0))
D1(finish2(x0)) → finish2(1(x0))
Db(finish2(x0)) → finish2(b(x0))
Ds(finish2(x0)) → finish2(s(x0))
Dt(finish2(x0)) → finish2(t(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(h(1(1(x0)))) → begin(1(h(x0)))
rewrite(1(1(h(b(x0))))) → begin(1(1(s(b(x0)))))
rewrite(1(s(x0))) → begin(s(1(x0)))
rewrite(b(s(x0))) → begin(b(h(x0)))
rewrite(h(1(b(x0)))) → begin(t(1(1(b(x0)))))
rewrite(1(t(x0))) → begin(t(1(1(1(x0)))))
rewrite(b(t(x0))) → begin(b(h(x0)))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) → rewrite(end(x0))
begin(h(x0)) → rotate(cut(Ch(guess(x0))))
begin(1(x0)) → rotate(cut(C1(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
begin(s(x0)) → rotate(cut(Cs(guess(x0))))
begin(t(x0)) → rotate(cut(Ct(guess(x0))))
guess(h(x0)) → Ch(guess(x0))
guess(1(x0)) → C1(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(s(x0)) → Cs(guess(x0))
guess(t(x0)) → Ct(guess(x0))
guess(h(x0)) → moveleft(Bh(wait(x0)))
guess(1(x0)) → moveleft(B1(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(s(x0)) → moveleft(Bs(wait(x0)))
guess(t(x0)) → moveleft(Bt(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ch(moveleft(Bh(x0))) → moveleft(Bh(Ah(x0)))
C1(moveleft(Bh(x0))) → moveleft(Bh(A1(x0)))
Cb(moveleft(Bh(x0))) → moveleft(Bh(Ab(x0)))
Cs(moveleft(Bh(x0))) → moveleft(Bh(As(x0)))
Ct(moveleft(Bh(x0))) → moveleft(Bh(At(x0)))
Ch(moveleft(B1(x0))) → moveleft(B1(Ah(x0)))
C1(moveleft(B1(x0))) → moveleft(B1(A1(x0)))
Cb(moveleft(B1(x0))) → moveleft(B1(Ab(x0)))
Cs(moveleft(B1(x0))) → moveleft(B1(As(x0)))
Ct(moveleft(B1(x0))) → moveleft(B1(At(x0)))
Ch(moveleft(Bb(x0))) → moveleft(Bb(Ah(x0)))
C1(moveleft(Bb(x0))) → moveleft(Bb(A1(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
Cs(moveleft(Bb(x0))) → moveleft(Bb(As(x0)))
Ct(moveleft(Bb(x0))) → moveleft(Bb(At(x0)))
Ch(moveleft(Bs(x0))) → moveleft(Bs(Ah(x0)))
C1(moveleft(Bs(x0))) → moveleft(Bs(A1(x0)))
Cb(moveleft(Bs(x0))) → moveleft(Bs(Ab(x0)))
Cs(moveleft(Bs(x0))) → moveleft(Bs(As(x0)))
Ct(moveleft(Bs(x0))) → moveleft(Bs(At(x0)))
Ch(moveleft(Bt(x0))) → moveleft(Bt(Ah(x0)))
C1(moveleft(Bt(x0))) → moveleft(Bt(A1(x0)))
Cb(moveleft(Bt(x0))) → moveleft(Bt(Ab(x0)))
Cs(moveleft(Bt(x0))) → moveleft(Bt(As(x0)))
Ct(moveleft(Bt(x0))) → moveleft(Bt(At(x0)))
cut(moveleft(Bh(x0))) → Dh(cut(goright(x0)))
cut(moveleft(B1(x0))) → D1(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
cut(moveleft(Bs(x0))) → Ds(cut(goright(x0)))
cut(moveleft(Bt(x0))) → Dt(cut(goright(x0)))
goright(Ah(x0)) → Ch(goright(x0))
goright(A1(x0)) → C1(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(As(x0)) → Cs(goright(x0))
goright(At(x0)) → Ct(goright(x0))
goright(wait(h(x0))) → moveleft(Bh(wait(x0)))
goright(wait(1(x0))) → moveleft(B1(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(s(x0))) → moveleft(Bs(wait(x0)))
goright(wait(t(x0))) → moveleft(Bt(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ch(finish(x0)) → finish(h(x0))
C1(finish(x0)) → finish(1(x0))
Cb(finish(x0)) → finish(b(x0))
Cs(finish(x0)) → finish(s(x0))
Ct(finish(x0)) → finish(t(x0))
cut(finish(x0)) → finish2(x0)
Dh(finish2(x0)) → finish2(h(x0))
D1(finish2(x0)) → finish2(1(x0))
Db(finish2(x0)) → finish2(b(x0))
Ds(finish2(x0)) → finish2(s(x0))
Dt(finish2(x0)) → finish2(t(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(h(1(1(x0)))) → begin(1(h(x0)))
rewrite(1(1(h(b(x0))))) → begin(1(1(s(b(x0)))))
rewrite(1(s(x0))) → begin(s(1(x0)))
rewrite(b(s(x0))) → begin(b(h(x0)))
rewrite(h(1(b(x0)))) → begin(t(1(1(b(x0)))))
rewrite(1(t(x0))) → begin(t(1(1(1(x0)))))
rewrite(b(t(x0))) → begin(b(h(x0)))