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(x0))
rewrite(c(x0))	→	begin(d(d(x0)))
rewrite(d(x0))	→	begin(a(a(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₁)]	=	2 · x₁ + -∞
[b(x₁)]	=	3 · x₁ + -∞
[begin(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	2 · x₁ + -∞
[moveleft(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	2 · x₁ + -∞
[Da(x₁)]	=	2 · x₁ + -∞
[Bd(x₁)]	=	4 · x₁ + -∞
[Bb(x₁)]	=	3 · x₁ + -∞
[Db(x₁)]	=	3 · x₁ + -∞
[Ab(x₁)]	=	3 · x₁ + -∞
[Dc(x₁)]	=	8 · x₁ + -∞
[Ca(x₁)]	=	2 · 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₁)]	=	4 · x₁ + -∞
[Ac(x₁)]	=	8 · x₁ + -∞
[Ad(x₁)]	=	4 · x₁ + -∞
[Cc(x₁)]	=	8 · x₁ + -∞
[Cb(x₁)]	=	3 · x₁ + -∞
[Cd(x₁)]	=	4 · x₁ + -∞
[cut(x₁)]	=	0 · x₁ + -∞
[Dd(x₁)]	=	4 · 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(c(x0))	→	begin(d(d(x0)))
rewrite(d(x0))	→	begin(a(a(x0)))

remain.

1.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₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[begin(x₁)]	=	1 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[moveleft(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Da(x₁)]	=	0 · x₁ + -∞
[Bd(x₁)]	=	4 · x₁ + -∞
[Bb(x₁)]	=	0 · x₁ + -∞
[Db(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[Dc(x₁)]	=	8 · x₁ + -∞
[Ca(x₁)]	=	0 · x₁ + -∞
[c(x₁)]	=	8 · x₁ + -∞
[end(x₁)]	=	0 · x₁ + -∞
[rotate(x₁)]	=	1 · x₁ + -∞
[finish(x₁)]	=	0 · x₁ + -∞
[goright(x₁)]	=	0 · x₁ + -∞
[finish2(x₁)]	=	0 · x₁ + -∞
[wait(x₁)]	=	0 · x₁ + -∞
[d(x₁)]	=	4 · x₁ + -∞
[Ac(x₁)]	=	8 · x₁ + -∞
[Ad(x₁)]	=	4 · x₁ + -∞
[Cc(x₁)]	=	8 · x₁ + -∞
[Cb(x₁)]	=	0 · x₁ + -∞
[Cd(x₁)]	=	4 · x₁ + -∞
[cut(x₁)]	=	0 · x₁ + -∞
[Dd(x₁)]	=	4 · x₁ + -∞
[rewrite(x₁)]	=	1 · 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(c(x0))	→	begin(d(d(x0)))

remain.

1.1.1 Rule Removal

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

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

remain.

1.1.1.1 Rule Removal

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

[Bc(x₁)]	=	0 · x₁ + -∞
[guess(x₁)]	=	0 · x₁ + -∞
[Ba(x₁)]	=	3 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[begin(x₁)]	=	8 · x₁ + -∞
[a(x₁)]	=	3 · x₁ + -∞
[moveleft(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	3 · x₁ + -∞
[Da(x₁)]	=	3 · x₁ + -∞
[Bd(x₁)]	=	0 · x₁ + -∞
[Bb(x₁)]	=	0 · x₁ + -∞
[Db(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[Dc(x₁)]	=	0 · x₁ + -∞
[Ca(x₁)]	=	3 · x₁ + -∞
[c(x₁)]	=	0 · x₁ + -∞
[end(x₁)]	=	0 · x₁ + -∞
[rotate(x₁)]	=	0 · x₁ + -∞
[finish(x₁)]	=	0 · x₁ + -∞
[goright(x₁)]	=	0 · x₁ + -∞
[finish2(x₁)]	=	2 · x₁ + -∞
[wait(x₁)]	=	0 · x₁ + -∞
[d(x₁)]	=	0 · x₁ + -∞
[Ac(x₁)]	=	0 · x₁ + -∞
[Ad(x₁)]	=	0 · x₁ + -∞
[Cc(x₁)]	=	0 · x₁ + -∞
[Cb(x₁)]	=	0 · x₁ + -∞
[Cd(x₁)]	=	0 · x₁ + -∞
[cut(x₁)]	=	8 · x₁ + -∞
[Dd(x₁)]	=	0 · 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))
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))
Da(finish2(x0))	→	finish2(a(x0))
Db(finish2(x0))	→	finish2(b(x0))
Dc(finish2(x0))	→	finish2(c(x0))
Dd(finish2(x0))	→	finish2(d(x0))

remain.

1.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))
a(guess(x0))	→	wait(Ba(moveleft(x0)))
b(guess(x0))	→	wait(Bb(moveleft(x0)))
c(guess(x0))	→	wait(Bc(moveleft(x0)))
d(guess(x0))	→	wait(Bd(moveleft(x0)))
end(guess(x0))	→	end(finish(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)))
end(wait(goright(x0)))	→	end(finish(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))
finish2(Da(x0))	→	a(finish2(x0))
finish2(Db(x0))	→	b(finish2(x0))
finish2(Dc(x0))	→	c(finish2(x0))
finish2(Dd(x0))	→	d(finish2(x0))

1.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, 67, 66, 65, 64, 63, 62, 61, 60, 59, 56, 53, 50, 47, 46, 45, 44, 43, 42, 41, 40, 39, 38, 37, 36, 35, 34, 33, 32, 31, 29, 27, 25, 23, 20, 18, 16, 14, 12, 10, 8, 6, 1}

transitions:

33 → 22

111 → 24

111 → 35

111 → 36

111 → 37

111 → 38

32 → 22

205 → 178

87 → 73

97 → 73

129 → 110

167 → 141

119 → 110

41 → 26

39 → 26

50 → 24

187 → 178

147 → 141

37 → 24

110 → 126

110 → 128

110 → 134

110 → 136

34 → 22

65 → 30

55 → 140

55 → 146

55 → 150

55 → 154

99 → 73

31 → 22

49 → 72

49 → 78

49 → 82

49 → 86

40 → 26

123 → 110

71 → 68

165 → 141

127 → 110

183 → 178

197 → 178

44 → 28

135 → 110

73 → 90

73 → 96

73 → 98

73 → 104

179 → 28

179 → 43

179 → 44

179 → 45

179 → 46

38 → 24

79 → 73

91 → 73

58 → 177

58 → 182

58 → 186

58 → 190

36 → 24

141 → 158

141 → 164

141 → 166

141 → 172

178 → 194

178 → 196

178 → 202

178 → 204

173 → 141

52 → 109

52 → 114

52 → 118

52 → 122

105 → 73

67 → 68

53 → 26

45 → 28

66 → 30

63 → 30

69 → 68

42 → 26

137 → 110

64 → 30

46 → 28

35 → 24

115 → 110

83 → 73

47 → 22

159 → 141

203 → 178

142 → 26

142 → 39

142 → 40

142 → 41

142 → 42

74 → 22

74 → 31

74 → 32

74 → 33

74 → 34

195 → 178

43 → 28

70 → 68

56 → 28

151 → 141

155 → 141

191 → 178

Cc₀(4) → 9

Cc₀(2) → 17

Ac₀(26) → 41

Ac₀(28) → 45

Ac₀(24) → 37

Ac₀(22) → 33

Ca₀(4) → 5

Ca₀(2) → 13

goright₁(110) → 111

goright₁(73) → 74

goright₁(141) → 142

goright₁(178) → 179

c₀(30) → 65

c₀(68) → 70

b₀(68) → 69

b₀(30) → 64

Aa₀(28) → 43

Aa₀(22) → 31

Aa₀(26) → 39

Aa₀(24) → 35

cut₀(3) → 4

cut₀(48) → 49

cut₀(57) → 58

cut₀(54) → 55

cut₀(51) → 52

Db₀(2) → 51

Cc₁(150) → 151

Cc₁(166) → 167

Cc₁(186) → 187

Cc₁(98) → 99

Cc₁(118) → 119

Cc₁(82) → 83

Cc₁(202) → 203

Cc₁(134) → 135

goright₀(52) → 50

goright₀(19) → 62

goright₀(17) → 61

goright₀(13) → 59

goright₀(55) → 53

goright₀(15) → 60

goright₀(58) → 56

goright₀(49) → 47

a₀(68) → 67

a₀(30) → 63

wait₀(26) → 25

wait₀(28) → 27

wait₀(22) → 20

wait₀(24) → 23

Ca₁(158) → 159

Ca₁(194) → 195

Ca₁(109) → 110

Ca₁(126) → 127

Ca₁(177) → 178

Ca₁(90) → 91

Ca₁(72) → 73

Ca₁(140) → 141

Ad₀(22) → 34

Ad₀(28) → 46

Ad₀(26) → 42

Ad₀(24) → 38

Cb₀(2) → 15

Cb₀(4) → 7

Cd₀(4) → 11

Cd₀(2) → 19

Da₀(2) → 48

d₀(30) → 66

d₀(68) → 71

Dd₀(2) → 57

Bb₀(21) → 24

Cb₁(164) → 165

Cb₁(146) → 147

Cb₁(96) → 97

Cb₁(196) → 197

Cb₁(78) → 79

Cb₁(114) → 115

Cb₁(182) → 183

Cb₁(128) → 129

rotate₀(2) → 3

finish2₀(2) → 68

Ba₀(21) → 22

moveleft₀(2) → 21

f31₀ → 2

end₀(30) → 29

Cd₁(104) → 105

Cd₁(204) → 205

Cd₁(86) → 87

Cd₁(154) → 155

Cd₁(136) → 137

Cd₁(190) → 191

Cd₁(172) → 173

Cd₁(122) → 123

Bc₀(21) → 26

finish₀(2) → 30

guess₀(5) → 1

guess₀(19) → 18

guess₀(15) → 14

guess₀(11) → 10

guess₀(9) → 8

guess₀(13) → 12

guess₀(17) → 16

guess₀(7) → 6

Ab₀(22) → 32

Ab₀(24) → 36

Ab₀(28) → 44

Ab₀(26) → 40

Bd₀(21) → 28

Dc₀(2) → 54

33	→	22
111	→	24
111	→	35
111	→	36
111	→	37
111	→	38
32	→	22
205	→	178
87	→	73
97	→	73
129	→	110
167	→	141
119	→	110
41	→	26
39	→	26
50	→	24
187	→	178
147	→	141
37	→	24
110	→	126
110	→	128
110	→	134
110	→	136
34	→	22
65	→	30
55	→	140
55	→	146
55	→	150
55	→	154
99	→	73
31	→	22
49	→	72
49	→	78
49	→	82
49	→	86
40	→	26
123	→	110
71	→	68
165	→	141
127	→	110
183	→	178
197	→	178
44	→	28
135	→	110
73	→	90
73	→	96
73	→	98
73	→	104
179	→	28
179	→	43
179	→	44
179	→	45
179	→	46
38	→	24
79	→	73
91	→	73
58	→	177
58	→	182
58	→	186
58	→	190
36	→	24
141	→	158
141	→	164
141	→	166
141	→	172
178	→	194
178	→	196
178	→	202
178	→	204
173	→	141
52	→	109
52	→	114
52	→	118
52	→	122
105	→	73
67	→	68
53	→	26
45	→	28
66	→	30
63	→	30
69	→	68
42	→	26
137	→	110
64	→	30
46	→	28
35	→	24
115	→	110
83	→	73
47	→	22
159	→	141
203	→	178
142	→	26
142	→	39
142	→	40
142	→	41
142	→	42
74	→	22
74	→	31
74	→	32
74	→	33
74	→	34
195	→	178
43	→	28
70	→	68
56	→	28
151	→	141
155	→	141
191	→	178
Cc₀(4)	→	9
Cc₀(2)	→	17
Ac₀(26)	→	41
Ac₀(28)	→	45
Ac₀(24)	→	37
Ac₀(22)	→	33
Ca₀(4)	→	5
Ca₀(2)	→	13
goright₁(110)	→	111
goright₁(73)	→	74
goright₁(141)	→	142
goright₁(178)	→	179
c₀(30)	→	65
c₀(68)	→	70
b₀(68)	→	69
b₀(30)	→	64
Aa₀(28)	→	43
Aa₀(22)	→	31
Aa₀(26)	→	39
Aa₀(24)	→	35
cut₀(3)	→	4
cut₀(48)	→	49
cut₀(57)	→	58
cut₀(54)	→	55
cut₀(51)	→	52
Db₀(2)	→	51
Cc₁(150)	→	151
Cc₁(166)	→	167
Cc₁(186)	→	187
Cc₁(98)	→	99
Cc₁(118)	→	119
Cc₁(82)	→	83
Cc₁(202)	→	203
Cc₁(134)	→	135
goright₀(52)	→	50
goright₀(19)	→	62
goright₀(17)	→	61
goright₀(13)	→	59
goright₀(55)	→	53
goright₀(15)	→	60
goright₀(58)	→	56
goright₀(49)	→	47
a₀(68)	→	67
a₀(30)	→	63
wait₀(26)	→	25
wait₀(28)	→	27
wait₀(22)	→	20
wait₀(24)	→	23
Ca₁(158)	→	159
Ca₁(194)	→	195
Ca₁(109)	→	110
Ca₁(126)	→	127
Ca₁(177)	→	178
Ca₁(90)	→	91
Ca₁(72)	→	73
Ca₁(140)	→	141
Ad₀(22)	→	34
Ad₀(28)	→	46
Ad₀(26)	→	42
Ad₀(24)	→	38
Cb₀(2)	→	15
Cb₀(4)	→	7
Cd₀(4)	→	11
Cd₀(2)	→	19
Da₀(2)	→	48
d₀(30)	→	66
d₀(68)	→	71
Dd₀(2)	→	57
Bb₀(21)	→	24
Cb₁(164)	→	165
Cb₁(146)	→	147
Cb₁(96)	→	97
Cb₁(196)	→	197
Cb₁(78)	→	79
Cb₁(114)	→	115
Cb₁(182)	→	183
Cb₁(128)	→	129
rotate₀(2)	→	3
finish2₀(2)	→	68
Ba₀(21)	→	22
moveleft₀(2)	→	21
f31₀	→	2
end₀(30)	→	29
Cd₁(104)	→	105
Cd₁(204)	→	205
Cd₁(86)	→	87
Cd₁(154)	→	155
Cd₁(136)	→	137
Cd₁(190)	→	191
Cd₁(172)	→	173
Cd₁(122)	→	123
Bc₀(21)	→	26
finish₀(2)	→	30
guess₀(5)	→	1
guess₀(19)	→	18
guess₀(15)	→	14
guess₀(11)	→	10
guess₀(9)	→	8
guess₀(13)	→	12
guess₀(17)	→	16
guess₀(7)	→	6
Ab₀(22)	→	32
Ab₀(24)	→	36
Ab₀(28)	→	44
Ab₀(26)	→	40
Bd₀(21)	→	28
Dc₀(2)	→	54