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(0(x0)) → rotate(cut(C0(guess(x0))))
begin(*(x0)) → rotate(cut(C*(guess(x0))))
begin(1(x0)) → rotate(cut(C1(guess(x0))))
begin(#(x0)) → rotate(cut(C#(guess(x0))))
begin($(x0)) → rotate(cut(C$(guess(x0))))
guess(0(x0)) → C0(guess(x0))
guess(*(x0)) → C*(guess(x0))
guess(1(x0)) → C1(guess(x0))
guess(#(x0)) → C#(guess(x0))
guess($(x0)) → C$(guess(x0))
guess(0(x0)) → moveleft(B0(wait(x0)))
guess(*(x0)) → moveleft(B*(wait(x0)))
guess(1(x0)) → moveleft(B1(wait(x0)))
guess(#(x0)) → moveleft(B#(wait(x0)))
guess($(x0)) → moveleft(B$(wait(x0)))
guess(end(x0)) → finish(end(x0))
C0(moveleft(B0(x0))) → moveleft(B0(A0(x0)))
C*(moveleft(B0(x0))) → moveleft(B0(A*(x0)))
C1(moveleft(B0(x0))) → moveleft(B0(A1(x0)))
C#(moveleft(B0(x0))) → moveleft(B0(A#(x0)))
C$(moveleft(B0(x0))) → moveleft(B0(A$(x0)))
C0(moveleft(B*(x0))) → moveleft(B*(A0(x0)))
C*(moveleft(B*(x0))) → moveleft(B*(A*(x0)))
C1(moveleft(B*(x0))) → moveleft(B*(A1(x0)))
C#(moveleft(B*(x0))) → moveleft(B*(A#(x0)))
C$(moveleft(B*(x0))) → moveleft(B*(A$(x0)))
C0(moveleft(B1(x0))) → moveleft(B1(A0(x0)))
C*(moveleft(B1(x0))) → moveleft(B1(A*(x0)))
C1(moveleft(B1(x0))) → moveleft(B1(A1(x0)))
C#(moveleft(B1(x0))) → moveleft(B1(A#(x0)))
C$(moveleft(B1(x0))) → moveleft(B1(A$(x0)))
C0(moveleft(B#(x0))) → moveleft(B#(A0(x0)))
C*(moveleft(B#(x0))) → moveleft(B#(A*(x0)))
C1(moveleft(B#(x0))) → moveleft(B#(A1(x0)))
C#(moveleft(B#(x0))) → moveleft(B#(A#(x0)))
C$(moveleft(B#(x0))) → moveleft(B#(A$(x0)))
C0(moveleft(B$(x0))) → moveleft(B$(A0(x0)))
C*(moveleft(B$(x0))) → moveleft(B$(A*(x0)))
C1(moveleft(B$(x0))) → moveleft(B$(A1(x0)))
C#(moveleft(B$(x0))) → moveleft(B$(A#(x0)))
C$(moveleft(B$(x0))) → moveleft(B$(A$(x0)))
cut(moveleft(B0(x0))) → D0(cut(goright(x0)))
cut(moveleft(B*(x0))) → D*(cut(goright(x0)))
cut(moveleft(B1(x0))) → D1(cut(goright(x0)))
cut(moveleft(B#(x0))) → D#(cut(goright(x0)))
cut(moveleft(B$(x0))) → D$(cut(goright(x0)))
goright(A0(x0)) → C0(goright(x0))
goright(A*(x0)) → C*(goright(x0))
goright(A1(x0)) → C1(goright(x0))
goright(A#(x0)) → C#(goright(x0))
goright(A$(x0)) → C$(goright(x0))
goright(wait(0(x0))) → moveleft(B0(wait(x0)))
goright(wait(*(x0))) → moveleft(B*(wait(x0)))
goright(wait(1(x0))) → moveleft(B1(wait(x0)))
goright(wait(#(x0))) → moveleft(B#(wait(x0)))
goright(wait($(x0))) → moveleft(B$(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
C0(finish(x0)) → finish(0(x0))
C*(finish(x0)) → finish(*(x0))
C1(finish(x0)) → finish(1(x0))
C#(finish(x0)) → finish(#(x0))
C$(finish(x0)) → finish($(x0))
cut(finish(x0)) → finish2(x0)
D0(finish2(x0)) → finish2(0(x0))
D*(finish2(x0)) → finish2(*(x0))
D1(finish2(x0)) → finish2(1(x0))
D#(finish2(x0)) → finish2(#(x0))
D$(finish2(x0)) → finish2($(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(0(0(*(*(x0))))) → begin(*(*(1(1(x0)))))
rewrite(1(1(*(*(x0))))) → begin(0(0(#(#(x0)))))
rewrite(#(#(0(0(x0))))) → begin(0(0(#(#(x0)))))
rewrite(#(#(1(1(x0))))) → begin(1(1(#(#(x0)))))
rewrite(#(#($($(x0))))) → begin(*(*($($(x0)))))
rewrite(#(#(#(#(x0))))) → begin(#(#(x0)))
rewrite(#(#(*(*(x0))))) → begin(*(*(x0)))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) → rewrite(end(x0))
begin(0(x0)) → rotate(cut(C0(guess(x0))))
begin(*(x0)) → rotate(cut(C*(guess(x0))))
begin(1(x0)) → rotate(cut(C1(guess(x0))))
begin(#(x0)) → rotate(cut(C#(guess(x0))))
begin($(x0)) → rotate(cut(C$(guess(x0))))
guess(0(x0)) → C0(guess(x0))
guess(*(x0)) → C*(guess(x0))
guess(1(x0)) → C1(guess(x0))
guess(#(x0)) → C#(guess(x0))
guess($(x0)) → C$(guess(x0))
guess(0(x0)) → moveleft(B0(wait(x0)))
guess(*(x0)) → moveleft(B*(wait(x0)))
guess(1(x0)) → moveleft(B1(wait(x0)))
guess(#(x0)) → moveleft(B#(wait(x0)))
guess($(x0)) → moveleft(B$(wait(x0)))
guess(end(x0)) → finish(end(x0))
C0(moveleft(B0(x0))) → moveleft(B0(A0(x0)))
C*(moveleft(B0(x0))) → moveleft(B0(A*(x0)))
C1(moveleft(B0(x0))) → moveleft(B0(A1(x0)))
C#(moveleft(B0(x0))) → moveleft(B0(A#(x0)))
C$(moveleft(B0(x0))) → moveleft(B0(A$(x0)))
C0(moveleft(B*(x0))) → moveleft(B*(A0(x0)))
C*(moveleft(B*(x0))) → moveleft(B*(A*(x0)))
C1(moveleft(B*(x0))) → moveleft(B*(A1(x0)))
C#(moveleft(B*(x0))) → moveleft(B*(A#(x0)))
C$(moveleft(B*(x0))) → moveleft(B*(A$(x0)))
C0(moveleft(B1(x0))) → moveleft(B1(A0(x0)))
C*(moveleft(B1(x0))) → moveleft(B1(A*(x0)))
C1(moveleft(B1(x0))) → moveleft(B1(A1(x0)))
C#(moveleft(B1(x0))) → moveleft(B1(A#(x0)))
C$(moveleft(B1(x0))) → moveleft(B1(A$(x0)))
C0(moveleft(B#(x0))) → moveleft(B#(A0(x0)))
C*(moveleft(B#(x0))) → moveleft(B#(A*(x0)))
C1(moveleft(B#(x0))) → moveleft(B#(A1(x0)))
C#(moveleft(B#(x0))) → moveleft(B#(A#(x0)))
C$(moveleft(B#(x0))) → moveleft(B#(A$(x0)))
C0(moveleft(B$(x0))) → moveleft(B$(A0(x0)))
C*(moveleft(B$(x0))) → moveleft(B$(A*(x0)))
C1(moveleft(B$(x0))) → moveleft(B$(A1(x0)))
C#(moveleft(B$(x0))) → moveleft(B$(A#(x0)))
C$(moveleft(B$(x0))) → moveleft(B$(A$(x0)))
cut(moveleft(B0(x0))) → D0(cut(goright(x0)))
cut(moveleft(B*(x0))) → D*(cut(goright(x0)))
cut(moveleft(B1(x0))) → D1(cut(goright(x0)))
cut(moveleft(B#(x0))) → D#(cut(goright(x0)))
cut(moveleft(B$(x0))) → D$(cut(goright(x0)))
goright(A0(x0)) → C0(goright(x0))
goright(A*(x0)) → C*(goright(x0))
goright(A1(x0)) → C1(goright(x0))
goright(A#(x0)) → C#(goright(x0))
goright(A$(x0)) → C$(goright(x0))
goright(wait(0(x0))) → moveleft(B0(wait(x0)))
goright(wait(*(x0))) → moveleft(B*(wait(x0)))
goright(wait(1(x0))) → moveleft(B1(wait(x0)))
goright(wait(#(x0))) → moveleft(B#(wait(x0)))
goright(wait($(x0))) → moveleft(B$(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
C0(finish(x0)) → finish(0(x0))
C*(finish(x0)) → finish(*(x0))
C1(finish(x0)) → finish(1(x0))
C#(finish(x0)) → finish(#(x0))
C$(finish(x0)) → finish($(x0))
cut(finish(x0)) → finish2(x0)
D0(finish2(x0)) → finish2(0(x0))
D*(finish2(x0)) → finish2(*(x0))
D1(finish2(x0)) → finish2(1(x0))
D#(finish2(x0)) → finish2(#(x0))
D$(finish2(x0)) → finish2($(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(0(0(*(*(x0))))) → begin(*(*(1(1(x0)))))
rewrite(1(1(*(*(x0))))) → begin(0(0(#(#(x0)))))
rewrite(#(#(0(0(x0))))) → begin(0(0(#(#(x0)))))
rewrite(#(#(1(1(x0))))) → begin(1(1(#(#(x0)))))
rewrite(#(#($($(x0))))) → begin(*(*($($(x0)))))
rewrite(#(#(#(#(x0))))) → begin(#(#(x0)))
rewrite(#(#(*(*(x0))))) → begin(*(*(x0)))