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(t(x0)) → rotate(cut(Ct(guess(x0))))
begin(o(x0)) → rotate(cut(Co(guess(x0))))
begin(m(x0)) → rotate(cut(Cm(guess(x0))))
begin(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(e(x0)) → rotate(cut(Ce(guess(x0))))
begin(n(x0)) → rotate(cut(Cn(guess(x0))))
begin(s(x0)) → rotate(cut(Cs(guess(x0))))
begin(l(x0)) → rotate(cut(Cl(guess(x0))))
guess(t(x0)) → Ct(guess(x0))
guess(o(x0)) → Co(guess(x0))
guess(m(x0)) → Cm(guess(x0))
guess(a(x0)) → Ca(guess(x0))
guess(e(x0)) → Ce(guess(x0))
guess(n(x0)) → Cn(guess(x0))
guess(s(x0)) → Cs(guess(x0))
guess(l(x0)) → Cl(guess(x0))
guess(t(x0)) → moveleft(Bt(wait(x0)))
guess(o(x0)) → moveleft(Bo(wait(x0)))
guess(m(x0)) → moveleft(Bm(wait(x0)))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(e(x0)) → moveleft(Be(wait(x0)))
guess(n(x0)) → moveleft(Bn(wait(x0)))
guess(s(x0)) → moveleft(Bs(wait(x0)))
guess(l(x0)) → moveleft(Bl(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ct(moveleft(Bt(x0))) → moveleft(Bt(At(x0)))
Co(moveleft(Bt(x0))) → moveleft(Bt(Ao(x0)))
Cm(moveleft(Bt(x0))) → moveleft(Bt(Am(x0)))
Ca(moveleft(Bt(x0))) → moveleft(Bt(Aa(x0)))
Ce(moveleft(Bt(x0))) → moveleft(Bt(Ae(x0)))
Cn(moveleft(Bt(x0))) → moveleft(Bt(An(x0)))
Cs(moveleft(Bt(x0))) → moveleft(Bt(As(x0)))
Cl(moveleft(Bt(x0))) → moveleft(Bt(Al(x0)))
Ct(moveleft(Bo(x0))) → moveleft(Bo(At(x0)))
Co(moveleft(Bo(x0))) → moveleft(Bo(Ao(x0)))
Cm(moveleft(Bo(x0))) → moveleft(Bo(Am(x0)))
Ca(moveleft(Bo(x0))) → moveleft(Bo(Aa(x0)))
Ce(moveleft(Bo(x0))) → moveleft(Bo(Ae(x0)))
Cn(moveleft(Bo(x0))) → moveleft(Bo(An(x0)))
Cs(moveleft(Bo(x0))) → moveleft(Bo(As(x0)))
Cl(moveleft(Bo(x0))) → moveleft(Bo(Al(x0)))
Ct(moveleft(Bm(x0))) → moveleft(Bm(At(x0)))
Co(moveleft(Bm(x0))) → moveleft(Bm(Ao(x0)))
Cm(moveleft(Bm(x0))) → moveleft(Bm(Am(x0)))
Ca(moveleft(Bm(x0))) → moveleft(Bm(Aa(x0)))
Ce(moveleft(Bm(x0))) → moveleft(Bm(Ae(x0)))
Cn(moveleft(Bm(x0))) → moveleft(Bm(An(x0)))
Cs(moveleft(Bm(x0))) → moveleft(Bm(As(x0)))
Cl(moveleft(Bm(x0))) → moveleft(Bm(Al(x0)))
Ct(moveleft(Ba(x0))) → moveleft(Ba(At(x0)))
Co(moveleft(Ba(x0))) → moveleft(Ba(Ao(x0)))
Cm(moveleft(Ba(x0))) → moveleft(Ba(Am(x0)))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Ce(moveleft(Ba(x0))) → moveleft(Ba(Ae(x0)))
Cn(moveleft(Ba(x0))) → moveleft(Ba(An(x0)))
Cs(moveleft(Ba(x0))) → moveleft(Ba(As(x0)))
Cl(moveleft(Ba(x0))) → moveleft(Ba(Al(x0)))
Ct(moveleft(Be(x0))) → moveleft(Be(At(x0)))
Co(moveleft(Be(x0))) → moveleft(Be(Ao(x0)))
Cm(moveleft(Be(x0))) → moveleft(Be(Am(x0)))
Ca(moveleft(Be(x0))) → moveleft(Be(Aa(x0)))
Ce(moveleft(Be(x0))) → moveleft(Be(Ae(x0)))
Cn(moveleft(Be(x0))) → moveleft(Be(An(x0)))
Cs(moveleft(Be(x0))) → moveleft(Be(As(x0)))
Cl(moveleft(Be(x0))) → moveleft(Be(Al(x0)))
Ct(moveleft(Bn(x0))) → moveleft(Bn(At(x0)))
Co(moveleft(Bn(x0))) → moveleft(Bn(Ao(x0)))
Cm(moveleft(Bn(x0))) → moveleft(Bn(Am(x0)))
Ca(moveleft(Bn(x0))) → moveleft(Bn(Aa(x0)))
Ce(moveleft(Bn(x0))) → moveleft(Bn(Ae(x0)))
Cn(moveleft(Bn(x0))) → moveleft(Bn(An(x0)))
Cs(moveleft(Bn(x0))) → moveleft(Bn(As(x0)))
Cl(moveleft(Bn(x0))) → moveleft(Bn(Al(x0)))
Ct(moveleft(Bs(x0))) → moveleft(Bs(At(x0)))
Co(moveleft(Bs(x0))) → moveleft(Bs(Ao(x0)))
Cm(moveleft(Bs(x0))) → moveleft(Bs(Am(x0)))
Ca(moveleft(Bs(x0))) → moveleft(Bs(Aa(x0)))
Ce(moveleft(Bs(x0))) → moveleft(Bs(Ae(x0)))
Cn(moveleft(Bs(x0))) → moveleft(Bs(An(x0)))
Cs(moveleft(Bs(x0))) → moveleft(Bs(As(x0)))
Cl(moveleft(Bs(x0))) → moveleft(Bs(Al(x0)))
Ct(moveleft(Bl(x0))) → moveleft(Bl(At(x0)))
Co(moveleft(Bl(x0))) → moveleft(Bl(Ao(x0)))
Cm(moveleft(Bl(x0))) → moveleft(Bl(Am(x0)))
Ca(moveleft(Bl(x0))) → moveleft(Bl(Aa(x0)))
Ce(moveleft(Bl(x0))) → moveleft(Bl(Ae(x0)))
Cn(moveleft(Bl(x0))) → moveleft(Bl(An(x0)))
Cs(moveleft(Bl(x0))) → moveleft(Bl(As(x0)))
Cl(moveleft(Bl(x0))) → moveleft(Bl(Al(x0)))
cut(moveleft(Bt(x0))) → Dt(cut(goright(x0)))
cut(moveleft(Bo(x0))) → Do(cut(goright(x0)))
cut(moveleft(Bm(x0))) → Dm(cut(goright(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Be(x0))) → De(cut(goright(x0)))
cut(moveleft(Bn(x0))) → Dn(cut(goright(x0)))
cut(moveleft(Bs(x0))) → Ds(cut(goright(x0)))
cut(moveleft(Bl(x0))) → Dl(cut(goright(x0)))
goright(At(x0)) → Ct(goright(x0))
goright(Ao(x0)) → Co(goright(x0))
goright(Am(x0)) → Cm(goright(x0))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ae(x0)) → Ce(goright(x0))
goright(An(x0)) → Cn(goright(x0))
goright(As(x0)) → Cs(goright(x0))
goright(Al(x0)) → Cl(goright(x0))
goright(wait(t(x0))) → moveleft(Bt(wait(x0)))
goright(wait(o(x0))) → moveleft(Bo(wait(x0)))
goright(wait(m(x0))) → moveleft(Bm(wait(x0)))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(e(x0))) → moveleft(Be(wait(x0)))
goright(wait(n(x0))) → moveleft(Bn(wait(x0)))
goright(wait(s(x0))) → moveleft(Bs(wait(x0)))
goright(wait(l(x0))) → moveleft(Bl(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ct(finish(x0)) → finish(t(x0))
Co(finish(x0)) → finish(o(x0))
Cm(finish(x0)) → finish(m(x0))
Ca(finish(x0)) → finish(a(x0))
Ce(finish(x0)) → finish(e(x0))
Cn(finish(x0)) → finish(n(x0))
Cs(finish(x0)) → finish(s(x0))
Cl(finish(x0)) → finish(l(x0))
cut(finish(x0)) → finish2(x0)
Dt(finish2(x0)) → finish2(t(x0))
Do(finish2(x0)) → finish2(o(x0))
Dm(finish2(x0)) → finish2(m(x0))
Da(finish2(x0)) → finish2(a(x0))
De(finish2(x0)) → finish2(e(x0))
Dn(finish2(x0)) → finish2(n(x0))
Ds(finish2(x0)) → finish2(s(x0))
Dl(finish2(x0)) → finish2(l(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(t(o(x0))) → begin(m(a(x0)))
rewrite(t(e(x0))) → begin(n(s(x0)))
rewrite(a(l(x0))) → begin(a(t(x0)))
rewrite(o(m(a(x0)))) → begin(t(e(n(x0))))
rewrite(s(a(x0))) → begin(l(a(t(o(m(a(t(e(x0)))))))))
rewrite(n(s(x0))) → begin(a(l(a(t(x0)))))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) → rewrite(end(x0))
begin(t(x0)) → rotate(cut(Ct(guess(x0))))
begin(o(x0)) → rotate(cut(Co(guess(x0))))
begin(m(x0)) → rotate(cut(Cm(guess(x0))))
begin(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(e(x0)) → rotate(cut(Ce(guess(x0))))
begin(n(x0)) → rotate(cut(Cn(guess(x0))))
begin(s(x0)) → rotate(cut(Cs(guess(x0))))
begin(l(x0)) → rotate(cut(Cl(guess(x0))))
guess(t(x0)) → Ct(guess(x0))
guess(o(x0)) → Co(guess(x0))
guess(m(x0)) → Cm(guess(x0))
guess(a(x0)) → Ca(guess(x0))
guess(e(x0)) → Ce(guess(x0))
guess(n(x0)) → Cn(guess(x0))
guess(s(x0)) → Cs(guess(x0))
guess(l(x0)) → Cl(guess(x0))
guess(t(x0)) → moveleft(Bt(wait(x0)))
guess(o(x0)) → moveleft(Bo(wait(x0)))
guess(m(x0)) → moveleft(Bm(wait(x0)))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(e(x0)) → moveleft(Be(wait(x0)))
guess(n(x0)) → moveleft(Bn(wait(x0)))
guess(s(x0)) → moveleft(Bs(wait(x0)))
guess(l(x0)) → moveleft(Bl(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ct(moveleft(Bt(x0))) → moveleft(Bt(At(x0)))
Co(moveleft(Bt(x0))) → moveleft(Bt(Ao(x0)))
Cm(moveleft(Bt(x0))) → moveleft(Bt(Am(x0)))
Ca(moveleft(Bt(x0))) → moveleft(Bt(Aa(x0)))
Ce(moveleft(Bt(x0))) → moveleft(Bt(Ae(x0)))
Cn(moveleft(Bt(x0))) → moveleft(Bt(An(x0)))
Cs(moveleft(Bt(x0))) → moveleft(Bt(As(x0)))
Cl(moveleft(Bt(x0))) → moveleft(Bt(Al(x0)))
Ct(moveleft(Bo(x0))) → moveleft(Bo(At(x0)))
Co(moveleft(Bo(x0))) → moveleft(Bo(Ao(x0)))
Cm(moveleft(Bo(x0))) → moveleft(Bo(Am(x0)))
Ca(moveleft(Bo(x0))) → moveleft(Bo(Aa(x0)))
Ce(moveleft(Bo(x0))) → moveleft(Bo(Ae(x0)))
Cn(moveleft(Bo(x0))) → moveleft(Bo(An(x0)))
Cs(moveleft(Bo(x0))) → moveleft(Bo(As(x0)))
Cl(moveleft(Bo(x0))) → moveleft(Bo(Al(x0)))
Ct(moveleft(Bm(x0))) → moveleft(Bm(At(x0)))
Co(moveleft(Bm(x0))) → moveleft(Bm(Ao(x0)))
Cm(moveleft(Bm(x0))) → moveleft(Bm(Am(x0)))
Ca(moveleft(Bm(x0))) → moveleft(Bm(Aa(x0)))
Ce(moveleft(Bm(x0))) → moveleft(Bm(Ae(x0)))
Cn(moveleft(Bm(x0))) → moveleft(Bm(An(x0)))
Cs(moveleft(Bm(x0))) → moveleft(Bm(As(x0)))
Cl(moveleft(Bm(x0))) → moveleft(Bm(Al(x0)))
Ct(moveleft(Ba(x0))) → moveleft(Ba(At(x0)))
Co(moveleft(Ba(x0))) → moveleft(Ba(Ao(x0)))
Cm(moveleft(Ba(x0))) → moveleft(Ba(Am(x0)))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Ce(moveleft(Ba(x0))) → moveleft(Ba(Ae(x0)))
Cn(moveleft(Ba(x0))) → moveleft(Ba(An(x0)))
Cs(moveleft(Ba(x0))) → moveleft(Ba(As(x0)))
Cl(moveleft(Ba(x0))) → moveleft(Ba(Al(x0)))
Ct(moveleft(Be(x0))) → moveleft(Be(At(x0)))
Co(moveleft(Be(x0))) → moveleft(Be(Ao(x0)))
Cm(moveleft(Be(x0))) → moveleft(Be(Am(x0)))
Ca(moveleft(Be(x0))) → moveleft(Be(Aa(x0)))
Ce(moveleft(Be(x0))) → moveleft(Be(Ae(x0)))
Cn(moveleft(Be(x0))) → moveleft(Be(An(x0)))
Cs(moveleft(Be(x0))) → moveleft(Be(As(x0)))
Cl(moveleft(Be(x0))) → moveleft(Be(Al(x0)))
Ct(moveleft(Bn(x0))) → moveleft(Bn(At(x0)))
Co(moveleft(Bn(x0))) → moveleft(Bn(Ao(x0)))
Cm(moveleft(Bn(x0))) → moveleft(Bn(Am(x0)))
Ca(moveleft(Bn(x0))) → moveleft(Bn(Aa(x0)))
Ce(moveleft(Bn(x0))) → moveleft(Bn(Ae(x0)))
Cn(moveleft(Bn(x0))) → moveleft(Bn(An(x0)))
Cs(moveleft(Bn(x0))) → moveleft(Bn(As(x0)))
Cl(moveleft(Bn(x0))) → moveleft(Bn(Al(x0)))
Ct(moveleft(Bs(x0))) → moveleft(Bs(At(x0)))
Co(moveleft(Bs(x0))) → moveleft(Bs(Ao(x0)))
Cm(moveleft(Bs(x0))) → moveleft(Bs(Am(x0)))
Ca(moveleft(Bs(x0))) → moveleft(Bs(Aa(x0)))
Ce(moveleft(Bs(x0))) → moveleft(Bs(Ae(x0)))
Cn(moveleft(Bs(x0))) → moveleft(Bs(An(x0)))
Cs(moveleft(Bs(x0))) → moveleft(Bs(As(x0)))
Cl(moveleft(Bs(x0))) → moveleft(Bs(Al(x0)))
Ct(moveleft(Bl(x0))) → moveleft(Bl(At(x0)))
Co(moveleft(Bl(x0))) → moveleft(Bl(Ao(x0)))
Cm(moveleft(Bl(x0))) → moveleft(Bl(Am(x0)))
Ca(moveleft(Bl(x0))) → moveleft(Bl(Aa(x0)))
Ce(moveleft(Bl(x0))) → moveleft(Bl(Ae(x0)))
Cn(moveleft(Bl(x0))) → moveleft(Bl(An(x0)))
Cs(moveleft(Bl(x0))) → moveleft(Bl(As(x0)))
Cl(moveleft(Bl(x0))) → moveleft(Bl(Al(x0)))
cut(moveleft(Bt(x0))) → Dt(cut(goright(x0)))
cut(moveleft(Bo(x0))) → Do(cut(goright(x0)))
cut(moveleft(Bm(x0))) → Dm(cut(goright(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Be(x0))) → De(cut(goright(x0)))
cut(moveleft(Bn(x0))) → Dn(cut(goright(x0)))
cut(moveleft(Bs(x0))) → Ds(cut(goright(x0)))
cut(moveleft(Bl(x0))) → Dl(cut(goright(x0)))
goright(At(x0)) → Ct(goright(x0))
goright(Ao(x0)) → Co(goright(x0))
goright(Am(x0)) → Cm(goright(x0))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ae(x0)) → Ce(goright(x0))
goright(An(x0)) → Cn(goright(x0))
goright(As(x0)) → Cs(goright(x0))
goright(Al(x0)) → Cl(goright(x0))
goright(wait(t(x0))) → moveleft(Bt(wait(x0)))
goright(wait(o(x0))) → moveleft(Bo(wait(x0)))
goright(wait(m(x0))) → moveleft(Bm(wait(x0)))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(e(x0))) → moveleft(Be(wait(x0)))
goright(wait(n(x0))) → moveleft(Bn(wait(x0)))
goright(wait(s(x0))) → moveleft(Bs(wait(x0)))
goright(wait(l(x0))) → moveleft(Bl(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ct(finish(x0)) → finish(t(x0))
Co(finish(x0)) → finish(o(x0))
Cm(finish(x0)) → finish(m(x0))
Ca(finish(x0)) → finish(a(x0))
Ce(finish(x0)) → finish(e(x0))
Cn(finish(x0)) → finish(n(x0))
Cs(finish(x0)) → finish(s(x0))
Cl(finish(x0)) → finish(l(x0))
cut(finish(x0)) → finish2(x0)
Dt(finish2(x0)) → finish2(t(x0))
Do(finish2(x0)) → finish2(o(x0))
Dm(finish2(x0)) → finish2(m(x0))
Da(finish2(x0)) → finish2(a(x0))
De(finish2(x0)) → finish2(e(x0))
Dn(finish2(x0)) → finish2(n(x0))
Ds(finish2(x0)) → finish2(s(x0))
Dl(finish2(x0)) → finish2(l(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(t(o(x0))) → begin(m(a(x0)))
rewrite(t(e(x0))) → begin(n(s(x0)))
rewrite(a(l(x0))) → begin(a(t(x0)))
rewrite(o(m(a(x0)))) → begin(t(e(n(x0))))
rewrite(s(a(x0))) → begin(l(a(t(o(m(a(t(e(x0)))))))))
rewrite(n(s(x0))) → begin(a(l(a(t(x0)))))