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))))
begin(c(x0))	→	rotate(cut(Cc(guess(x0))))
begin(d(x0))	→	rotate(cut(Cd(guess(x0))))
guess(a(x0))	→	Ca(guess(x0))
guess(b(x0))	→	Cb(guess(x0))
guess(c(x0))	→	Cc(guess(x0))
guess(d(x0))	→	Cd(guess(x0))
guess(a(x0))	→	moveleft(Ba(wait(x0)))
guess(b(x0))	→	moveleft(Bb(wait(x0)))
guess(c(x0))	→	moveleft(Bc(wait(x0)))
guess(d(x0))	→	moveleft(Bd(wait(x0)))
guess(end(x0))	→	finish(end(x0))
Ca(moveleft(Ba(x0)))	→	moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0)))	→	moveleft(Ba(Ab(x0)))
Cc(moveleft(Ba(x0)))	→	moveleft(Ba(Ac(x0)))
Cd(moveleft(Ba(x0)))	→	moveleft(Ba(Ad(x0)))
Ca(moveleft(Bb(x0)))	→	moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0)))	→	moveleft(Bb(Ab(x0)))
Cc(moveleft(Bb(x0)))	→	moveleft(Bb(Ac(x0)))
Cd(moveleft(Bb(x0)))	→	moveleft(Bb(Ad(x0)))
Ca(moveleft(Bc(x0)))	→	moveleft(Bc(Aa(x0)))
Cb(moveleft(Bc(x0)))	→	moveleft(Bc(Ab(x0)))
Cc(moveleft(Bc(x0)))	→	moveleft(Bc(Ac(x0)))
Cd(moveleft(Bc(x0)))	→	moveleft(Bc(Ad(x0)))
Ca(moveleft(Bd(x0)))	→	moveleft(Bd(Aa(x0)))
Cb(moveleft(Bd(x0)))	→	moveleft(Bd(Ab(x0)))
Cc(moveleft(Bd(x0)))	→	moveleft(Bd(Ac(x0)))
Cd(moveleft(Bd(x0)))	→	moveleft(Bd(Ad(x0)))
cut(moveleft(Ba(x0)))	→	Da(cut(goright(x0)))
cut(moveleft(Bb(x0)))	→	Db(cut(goright(x0)))
cut(moveleft(Bc(x0)))	→	Dc(cut(goright(x0)))
cut(moveleft(Bd(x0)))	→	Dd(cut(goright(x0)))
goright(Aa(x0))	→	Ca(goright(x0))
goright(Ab(x0))	→	Cb(goright(x0))
goright(Ac(x0))	→	Cc(goright(x0))
goright(Ad(x0))	→	Cd(goright(x0))
goright(wait(a(x0)))	→	moveleft(Ba(wait(x0)))
goright(wait(b(x0)))	→	moveleft(Bb(wait(x0)))
goright(wait(c(x0)))	→	moveleft(Bc(wait(x0)))
goright(wait(d(x0)))	→	moveleft(Bd(wait(x0)))
goright(wait(end(x0)))	→	finish(end(x0))
Ca(finish(x0))	→	finish(a(x0))
Cb(finish(x0))	→	finish(b(x0))
Cc(finish(x0))	→	finish(c(x0))
Cd(finish(x0))	→	finish(d(x0))
cut(finish(x0))	→	finish2(x0)
Da(finish2(x0))	→	finish2(a(x0))
Db(finish2(x0))	→	finish2(b(x0))
Dc(finish2(x0))	→	finish2(c(x0))
Dd(finish2(x0))	→	finish2(d(x0))
rotate(finish2(x0))	→	rewrite(x0)
rewrite(a(a(a(x0))))	→	begin(b(b(x0)))
rewrite(b(b(b(x0))))	→	begin(c(d(x0)))
rewrite(c(x0))	→	begin(a(a(x0)))
rewrite(d(x0))	→	begin(c(x0))

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[Bc(x₁)]	=	8 · x₁ + -∞
[guess(x₁)]	=	0 · x₁ + -∞
[Ba(x₁)]	=	4 · x₁ + -∞
[b(x₁)]	=	6 · x₁ + -∞
[begin(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	4 · x₁ + -∞
[moveleft(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	4 · x₁ + -∞
[Da(x₁)]	=	4 · x₁ + -∞
[Bd(x₁)]	=	10 · x₁ + -∞
[Bb(x₁)]	=	6 · x₁ + -∞
[Db(x₁)]	=	6 · x₁ + -∞
[Ab(x₁)]	=	6 · x₁ + -∞
[Dc(x₁)]	=	8 · x₁ + -∞
[Ca(x₁)]	=	4 · x₁ + -∞
[c(x₁)]	=	8 · x₁ + -∞
[end(x₁)]	=	0 · x₁ + -∞
[rotate(x₁)]	=	0 · x₁ + -∞
[finish(x₁)]	=	0 · x₁ + -∞
[goright(x₁)]	=	0 · x₁ + -∞
[finish2(x₁)]	=	0 · x₁ + -∞
[wait(x₁)]	=	0 · x₁ + -∞
[d(x₁)]	=	10 · x₁ + -∞
[Ac(x₁)]	=	8 · x₁ + -∞
[Ad(x₁)]	=	10 · x₁ + -∞
[Cc(x₁)]	=	8 · x₁ + -∞
[Cb(x₁)]	=	6 · x₁ + -∞
[Cd(x₁)]	=	10 · x₁ + -∞
[cut(x₁)]	=	0 · x₁ + -∞
[Dd(x₁)]	=	10 · x₁ + -∞
[rewrite(x₁)]	=	0 · x₁ + -∞

the rules

begin(end(x0))	→	rewrite(end(x0))
begin(a(x0))	→	rotate(cut(Ca(guess(x0))))
begin(b(x0))	→	rotate(cut(Cb(guess(x0))))
begin(c(x0))	→	rotate(cut(Cc(guess(x0))))
begin(d(x0))	→	rotate(cut(Cd(guess(x0))))
guess(a(x0))	→	Ca(guess(x0))
guess(b(x0))	→	Cb(guess(x0))
guess(c(x0))	→	Cc(guess(x0))
guess(d(x0))	→	Cd(guess(x0))
guess(a(x0))	→	moveleft(Ba(wait(x0)))
guess(b(x0))	→	moveleft(Bb(wait(x0)))
guess(c(x0))	→	moveleft(Bc(wait(x0)))
guess(d(x0))	→	moveleft(Bd(wait(x0)))
guess(end(x0))	→	finish(end(x0))
Ca(moveleft(Ba(x0)))	→	moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0)))	→	moveleft(Ba(Ab(x0)))
Cc(moveleft(Ba(x0)))	→	moveleft(Ba(Ac(x0)))
Cd(moveleft(Ba(x0)))	→	moveleft(Ba(Ad(x0)))
Ca(moveleft(Bb(x0)))	→	moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0)))	→	moveleft(Bb(Ab(x0)))
Cc(moveleft(Bb(x0)))	→	moveleft(Bb(Ac(x0)))
Cd(moveleft(Bb(x0)))	→	moveleft(Bb(Ad(x0)))
Ca(moveleft(Bc(x0)))	→	moveleft(Bc(Aa(x0)))
Cb(moveleft(Bc(x0)))	→	moveleft(Bc(Ab(x0)))
Cc(moveleft(Bc(x0)))	→	moveleft(Bc(Ac(x0)))
Cd(moveleft(Bc(x0)))	→	moveleft(Bc(Ad(x0)))
Ca(moveleft(Bd(x0)))	→	moveleft(Bd(Aa(x0)))
Cb(moveleft(Bd(x0)))	→	moveleft(Bd(Ab(x0)))
Cc(moveleft(Bd(x0)))	→	moveleft(Bd(Ac(x0)))
Cd(moveleft(Bd(x0)))	→	moveleft(Bd(Ad(x0)))
cut(moveleft(Ba(x0)))	→	Da(cut(goright(x0)))
cut(moveleft(Bb(x0)))	→	Db(cut(goright(x0)))
cut(moveleft(Bc(x0)))	→	Dc(cut(goright(x0)))
cut(moveleft(Bd(x0)))	→	Dd(cut(goright(x0)))
goright(Aa(x0))	→	Ca(goright(x0))
goright(Ab(x0))	→	Cb(goright(x0))
goright(Ac(x0))	→	Cc(goright(x0))
goright(Ad(x0))	→	Cd(goright(x0))
goright(wait(a(x0)))	→	moveleft(Ba(wait(x0)))
goright(wait(b(x0)))	→	moveleft(Bb(wait(x0)))
goright(wait(c(x0)))	→	moveleft(Bc(wait(x0)))
goright(wait(d(x0)))	→	moveleft(Bd(wait(x0)))
goright(wait(end(x0)))	→	finish(end(x0))
Ca(finish(x0))	→	finish(a(x0))
Cb(finish(x0))	→	finish(b(x0))
Cc(finish(x0))	→	finish(c(x0))
Cd(finish(x0))	→	finish(d(x0))
cut(finish(x0))	→	finish2(x0)
Da(finish2(x0))	→	finish2(a(x0))
Db(finish2(x0))	→	finish2(b(x0))
Dc(finish2(x0))	→	finish2(c(x0))
Dd(finish2(x0))	→	finish2(d(x0))
rotate(finish2(x0))	→	rewrite(x0)
rewrite(a(a(a(x0))))	→	begin(b(b(x0)))
rewrite(b(b(b(x0))))	→	begin(c(d(x0)))
rewrite(c(x0))	→	begin(a(a(x0)))

remain.

1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[Bc(x₁)]	=	4 · x₁ + -∞
[guess(x₁)]	=	0 · x₁ + -∞
[Ba(x₁)]	=	2 · x₁ + -∞
[b(x₁)]	=	2 · x₁ + -∞
[begin(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	2 · x₁ + -∞
[moveleft(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	2 · x₁ + -∞
[Da(x₁)]	=	2 · x₁ + -∞
[Bd(x₁)]	=	0 · x₁ + -∞
[Bb(x₁)]	=	2 · x₁ + -∞
[Db(x₁)]	=	2 · x₁ + -∞
[Ab(x₁)]	=	2 · x₁ + -∞
[Dc(x₁)]	=	4 · x₁ + -∞
[Ca(x₁)]	=	2 · x₁ + -∞
[c(x₁)]	=	4 · x₁ + -∞
[end(x₁)]	=	0 · x₁ + -∞
[rotate(x₁)]	=	0 · x₁ + -∞
[finish(x₁)]	=	0 · x₁ + -∞
[goright(x₁)]	=	0 · x₁ + -∞
[finish2(x₁)]	=	0 · x₁ + -∞
[wait(x₁)]	=	0 · x₁ + -∞
[d(x₁)]	=	0 · x₁ + -∞
[Ac(x₁)]	=	4 · x₁ + -∞
[Ad(x₁)]	=	0 · x₁ + -∞
[Cc(x₁)]	=	4 · x₁ + -∞
[Cb(x₁)]	=	2 · x₁ + -∞
[Cd(x₁)]	=	0 · x₁ + -∞
[cut(x₁)]	=	0 · x₁ + -∞
[Dd(x₁)]	=	0 · x₁ + -∞
[rewrite(x₁)]	=	0 · x₁ + -∞

the rules

begin(end(x0))	→	rewrite(end(x0))
begin(a(x0))	→	rotate(cut(Ca(guess(x0))))
begin(b(x0))	→	rotate(cut(Cb(guess(x0))))
begin(c(x0))	→	rotate(cut(Cc(guess(x0))))
begin(d(x0))	→	rotate(cut(Cd(guess(x0))))
guess(a(x0))	→	Ca(guess(x0))
guess(b(x0))	→	Cb(guess(x0))
guess(c(x0))	→	Cc(guess(x0))
guess(d(x0))	→	Cd(guess(x0))
guess(a(x0))	→	moveleft(Ba(wait(x0)))
guess(b(x0))	→	moveleft(Bb(wait(x0)))
guess(c(x0))	→	moveleft(Bc(wait(x0)))
guess(d(x0))	→	moveleft(Bd(wait(x0)))
guess(end(x0))	→	finish(end(x0))
Ca(moveleft(Ba(x0)))	→	moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0)))	→	moveleft(Ba(Ab(x0)))
Cc(moveleft(Ba(x0)))	→	moveleft(Ba(Ac(x0)))
Cd(moveleft(Ba(x0)))	→	moveleft(Ba(Ad(x0)))
Ca(moveleft(Bb(x0)))	→	moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0)))	→	moveleft(Bb(Ab(x0)))
Cc(moveleft(Bb(x0)))	→	moveleft(Bb(Ac(x0)))
Cd(moveleft(Bb(x0)))	→	moveleft(Bb(Ad(x0)))
Ca(moveleft(Bc(x0)))	→	moveleft(Bc(Aa(x0)))
Cb(moveleft(Bc(x0)))	→	moveleft(Bc(Ab(x0)))
Cc(moveleft(Bc(x0)))	→	moveleft(Bc(Ac(x0)))
Cd(moveleft(Bc(x0)))	→	moveleft(Bc(Ad(x0)))
Ca(moveleft(Bd(x0)))	→	moveleft(Bd(Aa(x0)))
Cb(moveleft(Bd(x0)))	→	moveleft(Bd(Ab(x0)))
Cc(moveleft(Bd(x0)))	→	moveleft(Bd(Ac(x0)))
Cd(moveleft(Bd(x0)))	→	moveleft(Bd(Ad(x0)))
cut(moveleft(Ba(x0)))	→	Da(cut(goright(x0)))
cut(moveleft(Bb(x0)))	→	Db(cut(goright(x0)))
cut(moveleft(Bc(x0)))	→	Dc(cut(goright(x0)))
cut(moveleft(Bd(x0)))	→	Dd(cut(goright(x0)))
goright(Aa(x0))	→	Ca(goright(x0))
goright(Ab(x0))	→	Cb(goright(x0))
goright(Ac(x0))	→	Cc(goright(x0))
goright(Ad(x0))	→	Cd(goright(x0))
goright(wait(a(x0)))	→	moveleft(Ba(wait(x0)))
goright(wait(b(x0)))	→	moveleft(Bb(wait(x0)))
goright(wait(c(x0)))	→	moveleft(Bc(wait(x0)))
goright(wait(d(x0)))	→	moveleft(Bd(wait(x0)))
goright(wait(end(x0)))	→	finish(end(x0))
Ca(finish(x0))	→	finish(a(x0))
Cb(finish(x0))	→	finish(b(x0))
Cc(finish(x0))	→	finish(c(x0))
Cd(finish(x0))	→	finish(d(x0))
cut(finish(x0))	→	finish2(x0)
Da(finish2(x0))	→	finish2(a(x0))
Db(finish2(x0))	→	finish2(b(x0))
Dc(finish2(x0))	→	finish2(c(x0))
Dd(finish2(x0))	→	finish2(d(x0))
rotate(finish2(x0))	→	rewrite(x0)
rewrite(c(x0))	→	begin(a(a(x0)))

remain.

1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[Bc(x₁)]	=	10 · x₁ + -∞
[guess(x₁)]	=	9 · x₁ + -∞
[Ba(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	1 · x₁ + -∞
[begin(x₁)]	=	10 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[moveleft(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Da(x₁)]	=	0 · x₁ + -∞
[Bd(x₁)]	=	4 · x₁ + -∞
[Bb(x₁)]	=	1 · x₁ + -∞
[Db(x₁)]	=	1 · x₁ + -∞
[Ab(x₁)]	=	1 · x₁ + -∞
[Dc(x₁)]	=	10 · x₁ + -∞
[Ca(x₁)]	=	0 · x₁ + -∞
[c(x₁)]	=	10 · x₁ + -∞
[end(x₁)]	=	10 · x₁ + -∞
[rotate(x₁)]	=	0 · x₁ + -∞
[finish(x₁)]	=	0 · x₁ + -∞
[goright(x₁)]	=	0 · x₁ + -∞
[finish2(x₁)]	=	1 · x₁ + -∞
[wait(x₁)]	=	4 · x₁ + -∞
[d(x₁)]	=	4 · x₁ + -∞
[Ac(x₁)]	=	10 · x₁ + -∞
[Ad(x₁)]	=	4 · x₁ + -∞
[Cc(x₁)]	=	10 · x₁ + -∞
[Cb(x₁)]	=	1 · x₁ + -∞
[Cd(x₁)]	=	4 · x₁ + -∞
[cut(x₁)]	=	1 · x₁ + -∞
[Dd(x₁)]	=	4 · x₁ + -∞
[rewrite(x₁)]	=	0 · x₁ + -∞

the rules

begin(a(x0))	→	rotate(cut(Ca(guess(x0))))
begin(b(x0))	→	rotate(cut(Cb(guess(x0))))
begin(c(x0))	→	rotate(cut(Cc(guess(x0))))
begin(d(x0))	→	rotate(cut(Cd(guess(x0))))
guess(a(x0))	→	Ca(guess(x0))
guess(b(x0))	→	Cb(guess(x0))
guess(c(x0))	→	Cc(guess(x0))
guess(d(x0))	→	Cd(guess(x0))
Ca(moveleft(Ba(x0)))	→	moveleft(Ba(Aa(x0)))
Cb(moveleft(Ba(x0)))	→	moveleft(Ba(Ab(x0)))
Cc(moveleft(Ba(x0)))	→	moveleft(Ba(Ac(x0)))
Cd(moveleft(Ba(x0)))	→	moveleft(Ba(Ad(x0)))
Ca(moveleft(Bb(x0)))	→	moveleft(Bb(Aa(x0)))
Cb(moveleft(Bb(x0)))	→	moveleft(Bb(Ab(x0)))
Cc(moveleft(Bb(x0)))	→	moveleft(Bb(Ac(x0)))
Cd(moveleft(Bb(x0)))	→	moveleft(Bb(Ad(x0)))
Ca(moveleft(Bc(x0)))	→	moveleft(Bc(Aa(x0)))
Cb(moveleft(Bc(x0)))	→	moveleft(Bc(Ab(x0)))
Cc(moveleft(Bc(x0)))	→	moveleft(Bc(Ac(x0)))
Cd(moveleft(Bc(x0)))	→	moveleft(Bc(Ad(x0)))
Ca(moveleft(Bd(x0)))	→	moveleft(Bd(Aa(x0)))
Cb(moveleft(Bd(x0)))	→	moveleft(Bd(Ab(x0)))
Cc(moveleft(Bd(x0)))	→	moveleft(Bd(Ac(x0)))
Cd(moveleft(Bd(x0)))	→	moveleft(Bd(Ad(x0)))
cut(moveleft(Ba(x0)))	→	Da(cut(goright(x0)))
cut(moveleft(Bb(x0)))	→	Db(cut(goright(x0)))
cut(moveleft(Bc(x0)))	→	Dc(cut(goright(x0)))
cut(moveleft(Bd(x0)))	→	Dd(cut(goright(x0)))
goright(Aa(x0))	→	Ca(goright(x0))
goright(Ab(x0))	→	Cb(goright(x0))
goright(Ac(x0))	→	Cc(goright(x0))
goright(Ad(x0))	→	Cd(goright(x0))
goright(wait(a(x0)))	→	moveleft(Ba(wait(x0)))
goright(wait(b(x0)))	→	moveleft(Bb(wait(x0)))
goright(wait(c(x0)))	→	moveleft(Bc(wait(x0)))
goright(wait(d(x0)))	→	moveleft(Bd(wait(x0)))
Ca(finish(x0))	→	finish(a(x0))
Cb(finish(x0))	→	finish(b(x0))
Cc(finish(x0))	→	finish(c(x0))
Cd(finish(x0))	→	finish(d(x0))
cut(finish(x0))	→	finish2(x0)
Da(finish2(x0))	→	finish2(a(x0))
Db(finish2(x0))	→	finish2(b(x0))
Dc(finish2(x0))	→	finish2(c(x0))
Dd(finish2(x0))	→	finish2(d(x0))
rewrite(c(x0))	→	begin(a(a(x0)))

remain.

1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

a(begin(x0))	→	guess(Ca(cut(rotate(x0))))
b(begin(x0))	→	guess(Cb(cut(rotate(x0))))
c(begin(x0))	→	guess(Cc(cut(rotate(x0))))
d(begin(x0))	→	guess(Cd(cut(rotate(x0))))
a(guess(x0))	→	guess(Ca(x0))
b(guess(x0))	→	guess(Cb(x0))
c(guess(x0))	→	guess(Cc(x0))
d(guess(x0))	→	guess(Cd(x0))
Ba(moveleft(Ca(x0)))	→	Aa(Ba(moveleft(x0)))
Ba(moveleft(Cb(x0)))	→	Ab(Ba(moveleft(x0)))
Ba(moveleft(Cc(x0)))	→	Ac(Ba(moveleft(x0)))
Ba(moveleft(Cd(x0)))	→	Ad(Ba(moveleft(x0)))
Bb(moveleft(Ca(x0)))	→	Aa(Bb(moveleft(x0)))
Bb(moveleft(Cb(x0)))	→	Ab(Bb(moveleft(x0)))
Bb(moveleft(Cc(x0)))	→	Ac(Bb(moveleft(x0)))
Bb(moveleft(Cd(x0)))	→	Ad(Bb(moveleft(x0)))
Bc(moveleft(Ca(x0)))	→	Aa(Bc(moveleft(x0)))
Bc(moveleft(Cb(x0)))	→	Ab(Bc(moveleft(x0)))
Bc(moveleft(Cc(x0)))	→	Ac(Bc(moveleft(x0)))
Bc(moveleft(Cd(x0)))	→	Ad(Bc(moveleft(x0)))
Bd(moveleft(Ca(x0)))	→	Aa(Bd(moveleft(x0)))
Bd(moveleft(Cb(x0)))	→	Ab(Bd(moveleft(x0)))
Bd(moveleft(Cc(x0)))	→	Ac(Bd(moveleft(x0)))
Bd(moveleft(Cd(x0)))	→	Ad(Bd(moveleft(x0)))
Ba(moveleft(cut(x0)))	→	goright(cut(Da(x0)))
Bb(moveleft(cut(x0)))	→	goright(cut(Db(x0)))
Bc(moveleft(cut(x0)))	→	goright(cut(Dc(x0)))
Bd(moveleft(cut(x0)))	→	goright(cut(Dd(x0)))
Aa(goright(x0))	→	goright(Ca(x0))
Ab(goright(x0))	→	goright(Cb(x0))
Ac(goright(x0))	→	goright(Cc(x0))
Ad(goright(x0))	→	goright(Cd(x0))
a(wait(goright(x0)))	→	wait(Ba(moveleft(x0)))
b(wait(goright(x0)))	→	wait(Bb(moveleft(x0)))
c(wait(goright(x0)))	→	wait(Bc(moveleft(x0)))
d(wait(goright(x0)))	→	wait(Bd(moveleft(x0)))
finish(Ca(x0))	→	a(finish(x0))
finish(Cb(x0))	→	b(finish(x0))
finish(Cc(x0))	→	c(finish(x0))
finish(Cd(x0))	→	d(finish(x0))
finish(cut(x0))	→	finish2(x0)
finish2(Da(x0))	→	a(finish2(x0))
finish2(Db(x0))	→	b(finish2(x0))
finish2(Dc(x0))	→	c(finish2(x0))
finish2(Dd(x0))	→	d(finish2(x0))
c(rewrite(x0))	→	a(a(begin(x0)))

1.1.1.1.1 Bounds

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

final states:

{71, 70, 69, 68, 67, 66, 65, 64, 63, 61, 60, 59, 58, 57, 56, 55, 54, 53, 50, 47, 44, 41, 40, 39, 38, 36, 35, 34, 33, 31, 30, 29, 28, 26, 25, 24, 23, 20, 18, 16, 14, 12, 10, 8, 6, 1}

transitions:

78 → 73

33 → 32

157 → 125

23 → 22

111 → 94

25 → 22

61 → 62

61 → 66

29 → 27

89 → 71

103 → 94

181 → 162

167 → 162

149 → 125

211 → 193

119 → 94

41 → 22

39 → 37

50 → 37

225 → 193

187 → 162

219 → 193

95 → 22

95 → 20

95 → 23

95 → 24

95 → 25

34 → 32

65 → 62

65 → 66

199 → 193

175 → 162

20 → 22

193 → 210

193 → 216

193 → 218

193 → 224

99 → 94

107 → 94

31 → 32

49 → 161

49 → 166

49 → 170

49 → 174

40 → 37

139 → 125

44 → 27

135 → 125

179 → 162

26 → 27

125 → 142

125 → 148

125 → 150

125 → 156

38 → 37

36 → 37

207 → 193

121 → 94

171 → 162

52 → 192

52 → 198

52 → 202

52 → 206

143 → 125

2 → 74

28 → 27

66 → 62

63 → 62

63 → 66

77 → 87

217 → 193

113 → 94

126 → 27

126 → 26

126 → 28

126 → 29

126 → 30

30 → 27

64 → 62

64 → 66

46 → 124

46 → 130

46 → 134

46 → 138

189 → 162

162 → 178

162 → 180

162 → 186

162 → 188

35 → 32

47 → 32

203 → 193

131 → 125

24 → 22

43 → 93

43 → 98

43 → 102

43 → 106

194 → 37

194 → 36

194 → 38

194 → 39

194 → 40

163 → 32

163 → 31

163 → 33

163 → 34

163 → 35

151 → 125

94 → 110

94 → 112

94 → 118

94 → 120

f31₀ → 2

Da₀(2) → 42

Aa₀(32) → 31

Aa₀(22) → 20

Aa₀(37) → 36

Aa₀(27) → 26

goright₀(19) → 56

goright₀(43) → 41

goright₀(15) → 54

goright₀(17) → 55

goright₀(13) → 53

goright₀(46) → 44

goright₀(49) → 47

goright₀(52) → 50

Dc₀(2) → 48

Cd₁(156) → 157

Cd₁(224) → 225

Cd₁(106) → 107

Cd₁(206) → 207

Cd₁(174) → 175

Cd₁(138) → 139

Cd₁(188) → 189

Cd₁(120) → 121

a₀(62) → 61

a₀(73) → 71

a₀(66) → 67

a₀(72) → 73

guess₁(88) → 89

guess₁(77) → 78

finish2₀(2) → 66

d₀(66) → 70

d₀(62) → 65

begin₀(2) → 72

finish₀(2) → 62

Cc₀(4) → 9

Cc₀(2) → 17

c₀(62) → 64

c₀(66) → 69

Ca₀(4) → 5

Ca₀(2) → 13

Cb₁(148) → 149

Cb₁(166) → 167

Cb₁(130) → 131

Cb₁(180) → 181

Cb₁(198) → 199

Cb₁(112) → 113

Cb₁(98) → 99

Cb₁(216) → 217

Bd₀(21) → 37

Ad₀(32) → 35

Ad₀(37) → 40

Ad₀(27) → 30

Ad₀(22) → 25

wait₀(32) → 59

wait₀(22) → 57

wait₀(27) → 58

wait₀(37) → 60

Dd₀(2) → 51

rotate₁(74) → 75

Bc₀(21) → 32

Ac₀(37) → 39

Ac₀(27) → 29

Ac₀(32) → 34

Ac₀(22) → 24

guess₀(5) → 1

guess₀(19) → 18

guess₀(15) → 14

guess₀(11) → 10

guess₀(9) → 8

guess₀(13) → 12

guess₀(17) → 16

guess₀(7) → 6

Cb₀(2) → 15

Cb₀(4) → 7

cut₁(75) → 76

rotate₀(2) → 3

Ba₀(21) → 22

b₀(62) → 63

b₀(66) → 68

Cc₁(186) → 187

Cc₁(134) → 135

Cc₁(118) → 119

Cc₁(170) → 171

Cc₁(150) → 151

Cc₁(202) → 203

Cc₁(218) → 219

Cc₁(102) → 103

moveleft₀(2) → 21

Bb₀(21) → 27

Cd₀(4) → 11

Cd₀(2) → 19

Ca₁(142) → 143

Ca₁(192) → 193

Ca₁(210) → 211

Ca₁(178) → 179

Ca₁(124) → 125

Ca₁(76) → 77

Ca₁(161) → 162

Ca₁(87) → 88

Ca₁(110) → 111

Ca₁(93) → 94

goright₁(193) → 194

goright₁(94) → 95

goright₁(162) → 163

goright₁(125) → 126

Db₀(2) → 45

cut₀(3) → 4

cut₀(48) → 49

cut₀(45) → 46

cut₀(51) → 52

cut₀(42) → 43

Ab₀(27) → 28

Ab₀(32) → 33

Ab₀(37) → 38

Ab₀(22) → 23

78	→	73
33	→	32
157	→	125
23	→	22
111	→	94
25	→	22
61	→	62
61	→	66
29	→	27
89	→	71
103	→	94
181	→	162
167	→	162
149	→	125
211	→	193
119	→	94
41	→	22
39	→	37
50	→	37
225	→	193
187	→	162
219	→	193
95	→	22
95	→	20
95	→	23
95	→	24
95	→	25
34	→	32
65	→	62
65	→	66
199	→	193
175	→	162
20	→	22
193	→	210
193	→	216
193	→	218
193	→	224
99	→	94
107	→	94
31	→	32
49	→	161
49	→	166
49	→	170
49	→	174
40	→	37
139	→	125
44	→	27
135	→	125
179	→	162
26	→	27
125	→	142
125	→	148
125	→	150
125	→	156
38	→	37
36	→	37
207	→	193
121	→	94
171	→	162
52	→	192
52	→	198
52	→	202
52	→	206
143	→	125
2	→	74
28	→	27
66	→	62
63	→	62
63	→	66
77	→	87
217	→	193
113	→	94
126	→	27
126	→	26
126	→	28
126	→	29
126	→	30
30	→	27
64	→	62
64	→	66
46	→	124
46	→	130
46	→	134
46	→	138
189	→	162
162	→	178
162	→	180
162	→	186
162	→	188
35	→	32
47	→	32
203	→	193
131	→	125
24	→	22
43	→	93
43	→	98
43	→	102
43	→	106
194	→	37
194	→	36
194	→	38
194	→	39
194	→	40
163	→	32
163	→	31
163	→	33
163	→	34
163	→	35
151	→	125
94	→	110
94	→	112
94	→	118
94	→	120
f31₀	→	2
Da₀(2)	→	42
Aa₀(32)	→	31
Aa₀(22)	→	20
Aa₀(37)	→	36
Aa₀(27)	→	26
goright₀(19)	→	56
goright₀(43)	→	41
goright₀(15)	→	54
goright₀(17)	→	55
goright₀(13)	→	53
goright₀(46)	→	44
goright₀(49)	→	47
goright₀(52)	→	50
Dc₀(2)	→	48
Cd₁(156)	→	157
Cd₁(224)	→	225
Cd₁(106)	→	107
Cd₁(206)	→	207
Cd₁(174)	→	175
Cd₁(138)	→	139
Cd₁(188)	→	189
Cd₁(120)	→	121
a₀(62)	→	61
a₀(73)	→	71
a₀(66)	→	67
a₀(72)	→	73
guess₁(88)	→	89
guess₁(77)	→	78
finish2₀(2)	→	66
d₀(66)	→	70
d₀(62)	→	65
begin₀(2)	→	72
finish₀(2)	→	62
Cc₀(4)	→	9
Cc₀(2)	→	17
c₀(62)	→	64
c₀(66)	→	69
Ca₀(4)	→	5
Ca₀(2)	→	13
Cb₁(148)	→	149
Cb₁(166)	→	167
Cb₁(130)	→	131
Cb₁(180)	→	181
Cb₁(198)	→	199
Cb₁(112)	→	113
Cb₁(98)	→	99
Cb₁(216)	→	217
Bd₀(21)	→	37
Ad₀(32)	→	35
Ad₀(37)	→	40
Ad₀(27)	→	30
Ad₀(22)	→	25
wait₀(32)	→	59
wait₀(22)	→	57
wait₀(27)	→	58
wait₀(37)	→	60
Dd₀(2)	→	51
rotate₁(74)	→	75
Bc₀(21)	→	32
Ac₀(37)	→	39
Ac₀(27)	→	29
Ac₀(32)	→	34
Ac₀(22)	→	24
guess₀(5)	→	1
guess₀(19)	→	18
guess₀(15)	→	14
guess₀(11)	→	10
guess₀(9)	→	8
guess₀(13)	→	12
guess₀(17)	→	16
guess₀(7)	→	6
Cb₀(2)	→	15
Cb₀(4)	→	7
cut₁(75)	→	76
rotate₀(2)	→	3
Ba₀(21)	→	22
b₀(62)	→	63
b₀(66)	→	68
Cc₁(186)	→	187
Cc₁(134)	→	135
Cc₁(118)	→	119
Cc₁(170)	→	171
Cc₁(150)	→	151
Cc₁(202)	→	203
Cc₁(218)	→	219
Cc₁(102)	→	103
moveleft₀(2)	→	21
Bb₀(21)	→	27
Cd₀(4)	→	11
Cd₀(2)	→	19
Ca₁(142)	→	143
Ca₁(192)	→	193
Ca₁(210)	→	211
Ca₁(178)	→	179
Ca₁(124)	→	125
Ca₁(76)	→	77
Ca₁(161)	→	162
Ca₁(87)	→	88
Ca₁(110)	→	111
Ca₁(93)	→	94
goright₁(193)	→	194
goright₁(94)	→	95
goright₁(162)	→	163
goright₁(125)	→	126
Db₀(2)	→	45
cut₀(3)	→	4
cut₀(48)	→	49
cut₀(45)	→	46
cut₀(51)	→	52
cut₀(42)	→	43
Ab₀(27)	→	28
Ab₀(32)	→	33
Ab₀(37)	→	38
Ab₀(22)	→	23