YES 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(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
guess(a(x0)) → Ca(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0))) → moveleft(Ba(Ab(x0)))
Ca(moveleft(Bb(x0))) → moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ca(finish(x0)) → finish(a(x0))
Cb(finish(x0)) → finish(b(x0))
cut(finish(x0)) → finish2(x0)
Da(finish2(x0)) → finish2(a(x0))
Db(finish2(x0)) → finish2(b(x0))
rotate(finish2(x0)) → rewrite(x0)
rewrite(a(x0)) → begin(b(x0))

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Da(x1)] = 12 · x1 + -∞
[guess(x1)] = 8 · x1 + -∞
[Aa(x1)] = 12 · x1 + -∞
[b(x1)] = 11 · x1 + -∞
[begin(x1)] = 9 · x1 + -∞
[a(x1)] = 12 · x1 + -∞
[Ab(x1)] = 11 · x1 + -∞
[Db(x1)] = 11 · x1 + -∞
[goright(x1)] = 1 · x1 + -∞
[Ca(x1)] = 12 · x1 + -∞
[wait(x1)] = 7 · x1 + -∞
[end(x1)] = 8 · x1 + -∞
[rotate(x1)] = 0 · x1 + -∞
[finish2(x1)] = 9 · x1 + -∞
[finish(x1)] = 8 · x1 + -∞
[moveleft(x1)] = 4 · x1 + -∞
[Ba(x1)] = 9 · x1 + -∞
[Cb(x1)] = 11 · x1 + -∞
[Bb(x1)] = 8 · x1 + -∞
[cut(x1)] = 1 · x1 + -∞
[rewrite(x1)] = 9 · x1 + -∞
the rules
begin(end(x0)) → rewrite(end(x0))
begin(a(x0)) → rotate(cut(Ca(guess(x0))))
begin(b(x0)) → rotate(cut(Cb(guess(x0))))
guess(a(x0)) → Ca(guess(x0))
guess(b(x0)) → Cb(guess(x0))
guess(a(x0)) → moveleft(Ba(wait(x0)))
guess(b(x0)) → moveleft(Bb(wait(x0)))
guess(end(x0)) → finish(end(x0))
Ca(moveleft(Ba(x0))) → moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0))) → moveleft(Ba(Ab(x0)))
Ca(moveleft(Bb(x0))) → moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0))) → moveleft(Bb(Ab(x0)))
cut(moveleft(Ba(x0))) → Da(cut(goright(x0)))
cut(moveleft(Bb(x0))) → Db(cut(goright(x0)))
goright(Aa(x0)) → Ca(goright(x0))
goright(Ab(x0)) → Cb(goright(x0))
goright(wait(a(x0))) → moveleft(Ba(wait(x0)))
goright(wait(b(x0))) → moveleft(Bb(wait(x0)))
goright(wait(end(x0))) → finish(end(x0))
Ca(finish(x0)) → finish(a(x0))
Cb(finish(x0)) → finish(b(x0))
cut(finish(x0)) → finish2(x0)
Da(finish2(x0)) → finish2(a(x0))
Db(finish2(x0)) → finish2(b(x0))
rotate(finish2(x0)) → rewrite(x0)
remain.

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
end(begin(x0)) → end(rewrite(x0))
a(begin(x0)) → guess(Ca(cut(rotate(x0))))
b(begin(x0)) → guess(Cb(cut(rotate(x0))))
a(guess(x0)) → guess(Ca(x0))
b(guess(x0)) → guess(Cb(x0))
a(guess(x0)) → wait(Ba(moveleft(x0)))
b(guess(x0)) → wait(Bb(moveleft(x0)))
end(guess(x0)) → end(finish(x0))
Ba(moveleft(Ca(x0))) → Aa(Ba(moveleft(x0)))
Ba(moveleft(Cb(x0))) → Ab(Ba(moveleft(x0)))
Bb(moveleft(Ca(x0))) → Aa(Bb(moveleft(x0)))
Bb(moveleft(Cb(x0))) → Ab(Bb(moveleft(x0)))
Ba(moveleft(cut(x0))) → goright(cut(Da(x0)))
Bb(moveleft(cut(x0))) → goright(cut(Db(x0)))
Aa(goright(x0)) → goright(Ca(x0))
Ab(goright(x0)) → goright(Cb(x0))
a(wait(goright(x0))) → wait(Ba(moveleft(x0)))
b(wait(goright(x0))) → wait(Bb(moveleft(x0)))
end(wait(goright(x0))) → end(finish(x0))
finish(Ca(x0)) → a(finish(x0))
finish(Cb(x0)) → b(finish(x0))
finish(cut(x0)) → finish2(x0)
finish2(Da(x0)) → a(finish2(x0))
finish2(Db(x0)) → b(finish2(x0))
finish2(rotate(x0)) → rewrite(x0)

1.1.1 Bounds

The given TRS is match-bounded by 1. This is shown by the following automaton.