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(r(x0)) → rotate(cut(Cr(guess(x0))))
begin(e(x0)) → rotate(cut(Ce(guess(x0))))
begin(w(x0)) → rotate(cut(Cw(guess(x0))))
begin(i(x0)) → rotate(cut(Ci(guess(x0))))
begin(t(x0)) → rotate(cut(Ct(guess(x0))))
guess(r(x0)) → Cr(guess(x0))
guess(e(x0)) → Ce(guess(x0))
guess(w(x0)) → Cw(guess(x0))
guess(i(x0)) → Ci(guess(x0))
guess(t(x0)) → Ct(guess(x0))
guess(r(x0)) → moveleft(Br(wait(x0)))
guess(e(x0)) → moveleft(Be(wait(x0)))
guess(w(x0)) → moveleft(Bw(wait(x0)))
guess(i(x0)) → moveleft(Bi(wait(x0)))
guess(t(x0)) → moveleft(Bt(wait(x0)))
guess(end(x0)) → finish(end(x0))
Cr(moveleft(Br(x0))) → moveleft(Br(Ar(x0)))
Ce(moveleft(Br(x0))) → moveleft(Br(Ae(x0)))
Cw(moveleft(Br(x0))) → moveleft(Br(Aw(x0)))
Ci(moveleft(Br(x0))) → moveleft(Br(Ai(x0)))
Ct(moveleft(Br(x0))) → moveleft(Br(At(x0)))
Cr(moveleft(Be(x0))) → moveleft(Be(Ar(x0)))
Ce(moveleft(Be(x0))) → moveleft(Be(Ae(x0)))
Cw(moveleft(Be(x0))) → moveleft(Be(Aw(x0)))
Ci(moveleft(Be(x0))) → moveleft(Be(Ai(x0)))
Ct(moveleft(Be(x0))) → moveleft(Be(At(x0)))
Cr(moveleft(Bw(x0))) → moveleft(Bw(Ar(x0)))
Ce(moveleft(Bw(x0))) → moveleft(Bw(Ae(x0)))
Cw(moveleft(Bw(x0))) → moveleft(Bw(Aw(x0)))
Ci(moveleft(Bw(x0))) → moveleft(Bw(Ai(x0)))
Ct(moveleft(Bw(x0))) → moveleft(Bw(At(x0)))
Cr(moveleft(Bi(x0))) → moveleft(Bi(Ar(x0)))
Ce(moveleft(Bi(x0))) → moveleft(Bi(Ae(x0)))
Cw(moveleft(Bi(x0))) → moveleft(Bi(Aw(x0)))
Ci(moveleft(Bi(x0))) → moveleft(Bi(Ai(x0)))
Ct(moveleft(Bi(x0))) → moveleft(Bi(At(x0)))
Cr(moveleft(Bt(x0))) → moveleft(Bt(Ar(x0)))
Ce(moveleft(Bt(x0))) → moveleft(Bt(Ae(x0)))
Cw(moveleft(Bt(x0))) → moveleft(Bt(Aw(x0)))
Ci(moveleft(Bt(x0))) → moveleft(Bt(Ai(x0)))
Ct(moveleft(Bt(x0))) → moveleft(Bt(At(x0)))
cut(moveleft(Br(x0))) → Dr(cut(goright(x0)))
cut(moveleft(Be(x0))) → De(cut(goright(x0)))
cut(moveleft(Bw(x0))) → Dw(cut(goright(x0)))
cut(moveleft(Bi(x0))) → Di(cut(goright(x0)))
cut(moveleft(Bt(x0))) → Dt(cut(goright(x0)))
goright(Ar(x0)) → Cr(goright(x0))
goright(Ae(x0)) → Ce(goright(x0))
goright(Aw(x0)) → Cw(goright(x0))
goright(Ai(x0)) → Ci(goright(x0))
goright(At(x0)) → Ct(goright(x0))
goright(wait(r(x0))) → moveleft(Br(wait(x0)))
goright(wait(e(x0))) → moveleft(Be(wait(x0)))
goright(wait(w(x0))) → moveleft(Bw(wait(x0)))
goright(wait(i(x0))) → moveleft(Bi(wait(x0)))
goright(wait(t(x0))) → moveleft(Bt(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Cr(finish(x0)) → finish(r(x0))
Ce(finish(x0)) → finish(e(x0))
Cw(finish(x0)) → finish(w(x0))
Ci(finish(x0)) → finish(i(x0))
Ct(finish(x0)) → finish(t(x0))
cut(finish(x0)) → finish2(x0)
Dr(finish2(x0)) → finish2(r(x0))
De(finish2(x0)) → finish2(e(x0))
Dw(finish2(x0)) → finish2(w(x0))
Di(finish2(x0)) → finish2(i(x0))
Dt(finish2(x0)) → finish2(t(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(r(e(x0))) → begin(w(r(x0)))
rewrite(i(t(x0))) → begin(e(r(x0)))
rewrite(e(w(x0))) → begin(r(i(x0)))
rewrite(t(e(x0))) → begin(r(e(x0)))
rewrite(w(r(x0))) → begin(i(t(x0)))
rewrite(e(r(x0))) → begin(e(w(x0)))
rewrite(r(i(t(e(r(x0)))))) → begin(e(w(r(i(t(e(x0)))))))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) → rewrite(end(x0))
begin(r(x0)) → rotate(cut(Cr(guess(x0))))
begin(e(x0)) → rotate(cut(Ce(guess(x0))))
begin(w(x0)) → rotate(cut(Cw(guess(x0))))
begin(i(x0)) → rotate(cut(Ci(guess(x0))))
begin(t(x0)) → rotate(cut(Ct(guess(x0))))
guess(r(x0)) → Cr(guess(x0))
guess(e(x0)) → Ce(guess(x0))
guess(w(x0)) → Cw(guess(x0))
guess(i(x0)) → Ci(guess(x0))
guess(t(x0)) → Ct(guess(x0))
guess(r(x0)) → moveleft(Br(wait(x0)))
guess(e(x0)) → moveleft(Be(wait(x0)))
guess(w(x0)) → moveleft(Bw(wait(x0)))
guess(i(x0)) → moveleft(Bi(wait(x0)))
guess(t(x0)) → moveleft(Bt(wait(x0)))
guess(end(x0)) → finish(end(x0))
Cr(moveleft(Br(x0))) → moveleft(Br(Ar(x0)))
Ce(moveleft(Br(x0))) → moveleft(Br(Ae(x0)))
Cw(moveleft(Br(x0))) → moveleft(Br(Aw(x0)))
Ci(moveleft(Br(x0))) → moveleft(Br(Ai(x0)))
Ct(moveleft(Br(x0))) → moveleft(Br(At(x0)))
Cr(moveleft(Be(x0))) → moveleft(Be(Ar(x0)))
Ce(moveleft(Be(x0))) → moveleft(Be(Ae(x0)))
Cw(moveleft(Be(x0))) → moveleft(Be(Aw(x0)))
Ci(moveleft(Be(x0))) → moveleft(Be(Ai(x0)))
Ct(moveleft(Be(x0))) → moveleft(Be(At(x0)))
Cr(moveleft(Bw(x0))) → moveleft(Bw(Ar(x0)))
Ce(moveleft(Bw(x0))) → moveleft(Bw(Ae(x0)))
Cw(moveleft(Bw(x0))) → moveleft(Bw(Aw(x0)))
Ci(moveleft(Bw(x0))) → moveleft(Bw(Ai(x0)))
Ct(moveleft(Bw(x0))) → moveleft(Bw(At(x0)))
Cr(moveleft(Bi(x0))) → moveleft(Bi(Ar(x0)))
Ce(moveleft(Bi(x0))) → moveleft(Bi(Ae(x0)))
Cw(moveleft(Bi(x0))) → moveleft(Bi(Aw(x0)))
Ci(moveleft(Bi(x0))) → moveleft(Bi(Ai(x0)))
Ct(moveleft(Bi(x0))) → moveleft(Bi(At(x0)))
Cr(moveleft(Bt(x0))) → moveleft(Bt(Ar(x0)))
Ce(moveleft(Bt(x0))) → moveleft(Bt(Ae(x0)))
Cw(moveleft(Bt(x0))) → moveleft(Bt(Aw(x0)))
Ci(moveleft(Bt(x0))) → moveleft(Bt(Ai(x0)))
Ct(moveleft(Bt(x0))) → moveleft(Bt(At(x0)))
cut(moveleft(Br(x0))) → Dr(cut(goright(x0)))
cut(moveleft(Be(x0))) → De(cut(goright(x0)))
cut(moveleft(Bw(x0))) → Dw(cut(goright(x0)))
cut(moveleft(Bi(x0))) → Di(cut(goright(x0)))
cut(moveleft(Bt(x0))) → Dt(cut(goright(x0)))
goright(Ar(x0)) → Cr(goright(x0))
goright(Ae(x0)) → Ce(goright(x0))
goright(Aw(x0)) → Cw(goright(x0))
goright(Ai(x0)) → Ci(goright(x0))
goright(At(x0)) → Ct(goright(x0))
goright(wait(r(x0))) → moveleft(Br(wait(x0)))
goright(wait(e(x0))) → moveleft(Be(wait(x0)))
goright(wait(w(x0))) → moveleft(Bw(wait(x0)))
goright(wait(i(x0))) → moveleft(Bi(wait(x0)))
goright(wait(t(x0))) → moveleft(Bt(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Cr(finish(x0)) → finish(r(x0))
Ce(finish(x0)) → finish(e(x0))
Cw(finish(x0)) → finish(w(x0))
Ci(finish(x0)) → finish(i(x0))
Ct(finish(x0)) → finish(t(x0))
cut(finish(x0)) → finish2(x0)
Dr(finish2(x0)) → finish2(r(x0))
De(finish2(x0)) → finish2(e(x0))
Dw(finish2(x0)) → finish2(w(x0))
Di(finish2(x0)) → finish2(i(x0))
Dt(finish2(x0)) → finish2(t(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(r(e(x0))) → begin(w(r(x0)))
rewrite(i(t(x0))) → begin(e(r(x0)))
rewrite(e(w(x0))) → begin(r(i(x0)))
rewrite(t(e(x0))) → begin(r(e(x0)))
rewrite(w(r(x0))) → begin(i(t(x0)))
rewrite(e(r(x0))) → begin(e(w(x0)))
rewrite(r(i(t(e(r(x0)))))) → begin(e(w(r(i(t(e(x0)))))))