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(x0))) |
→ |
begin(b(b(b(x0)))) |
|
rewrite(b(b(x0))) |
→ |
begin(c(c(c(x0)))) |
|
rewrite(c(c(x0))) |
→ |
begin(d(d(d(x0)))) |
|
rewrite(b(x0)) |
→ |
begin(d(d(x0))) |
|
rewrite(c(d(d(x0)))) |
→ |
begin(a(x0)) |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Bc(x1)] |
= |
3 ·
x1 +
-∞
|
| [guess(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ba(x1)] |
= |
11 ·
x1 +
-∞
|
| [b(x1)] |
= |
9 ·
x1 +
-∞
|
| [begin(x1)] |
= |
0 ·
x1 +
-∞
|
| [a(x1)] |
= |
14 ·
x1 +
-∞
|
| [moveleft(x1)] |
= |
3 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
14 ·
x1 +
-∞
|
| [Da(x1)] |
= |
14 ·
x1 +
-∞
|
| [Bd(x1)] |
= |
1 ·
x1 +
-∞
|
| [Bb(x1)] |
= |
6 ·
x1 +
-∞
|
| [Db(x1)] |
= |
9 ·
x1 +
-∞
|
| [Ab(x1)] |
= |
9 ·
x1 +
-∞
|
| [Dc(x1)] |
= |
6 ·
x1 +
-∞
|
| [Ca(x1)] |
= |
14 ·
x1 +
-∞
|
| [c(x1)] |
= |
6 ·
x1 +
-∞
|
| [end(x1)] |
= |
8 ·
x1 +
-∞
|
| [rotate(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish(x1)] |
= |
0 ·
x1 +
-∞
|
| [goright(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish2(x1)] |
= |
0 ·
x1 +
-∞
|
| [wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [d(x1)] |
= |
4 ·
x1 +
-∞
|
| [Ac(x1)] |
= |
6 ·
x1 +
-∞
|
| [Ad(x1)] |
= |
4 ·
x1 +
-∞
|
| [Cc(x1)] |
= |
6 ·
x1 +
-∞
|
| [Cb(x1)] |
= |
9 ·
x1 +
-∞
|
| [Cd(x1)] |
= |
4 ·
x1 +
-∞
|
| [cut(x1)] |
= |
0 ·
x1 +
-∞
|
| [Dd(x1)] |
= |
4 ·
x1 +
-∞
|
| [rewrite(x1)] |
= |
0 ·
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)))) |
|
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(b(b(x0))) |
→ |
begin(c(c(c(x0)))) |
|
rewrite(c(c(x0))) |
→ |
begin(d(d(d(x0)))) |
|
rewrite(c(d(d(x0)))) |
→ |
begin(a(x0)) |
remain.
1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Bc(x1)] |
= |
8 ·
x1 +
-∞
|
| [guess(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ba(x1)] |
= |
0 ·
x1 +
-∞
|
| [b(x1)] |
= |
13 ·
x1 +
-∞
|
| [begin(x1)] |
= |
2 ·
x1 +
-∞
|
| [a(x1)] |
= |
0 ·
x1 +
-∞
|
| [moveleft(x1)] |
= |
0 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
0 ·
x1 +
-∞
|
| [Da(x1)] |
= |
0 ·
x1 +
-∞
|
| [Bd(x1)] |
= |
1 ·
x1 +
-∞
|
| [Bb(x1)] |
= |
13 ·
x1 +
-∞
|
| [Db(x1)] |
= |
13 ·
x1 +
-∞
|
| [Ab(x1)] |
= |
13 ·
x1 +
-∞
|
| [Dc(x1)] |
= |
8 ·
x1 +
-∞
|
| [Ca(x1)] |
= |
0 ·
x1 +
-∞
|
| [c(x1)] |
= |
8 ·
x1 +
-∞
|
| [end(x1)] |
= |
0 ·
x1 +
-∞
|
| [rotate(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish(x1)] |
= |
0 ·
x1 +
-∞
|
| [goright(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish2(x1)] |
= |
0 ·
x1 +
-∞
|
| [wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [d(x1)] |
= |
1 ·
x1 +
-∞
|
| [Ac(x1)] |
= |
8 ·
x1 +
-∞
|
| [Ad(x1)] |
= |
1 ·
x1 +
-∞
|
| [Cc(x1)] |
= |
8 ·
x1 +
-∞
|
| [Cb(x1)] |
= |
13 ·
x1 +
-∞
|
| [Cd(x1)] |
= |
1 ·
x1 +
-∞
|
| [cut(x1)] |
= |
2 ·
x1 +
-∞
|
| [Dd(x1)] |
= |
1 ·
x1 +
-∞
|
| [rewrite(x1)] |
= |
0 ·
x1 +
-∞
|
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)) |
|
rotate(finish2(x0)) |
→ |
rewrite(x0) |
|
rewrite(b(b(x0))) |
→ |
begin(c(c(c(x0)))) |
remain.
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Bc(x1)] |
= |
0 ·
x1 +
-∞
|
| [guess(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ba(x1)] |
= |
0 ·
x1 +
-∞
|
| [b(x1)] |
= |
0 ·
x1 +
-∞
|
| [begin(x1)] |
= |
4 ·
x1 +
-∞
|
| [a(x1)] |
= |
0 ·
x1 +
-∞
|
| [moveleft(x1)] |
= |
0 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
0 ·
x1 +
-∞
|
| [Da(x1)] |
= |
0 ·
x1 +
-∞
|
| [Bd(x1)] |
= |
14 ·
x1 +
-∞
|
| [Bb(x1)] |
= |
0 ·
x1 +
-∞
|
| [Db(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ab(x1)] |
= |
0 ·
x1 +
-∞
|
| [Dc(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ca(x1)] |
= |
0 ·
x1 +
-∞
|
| [c(x1)] |
= |
0 ·
x1 +
-∞
|
| [end(x1)] |
= |
0 ·
x1 +
-∞
|
| [rotate(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish(x1)] |
= |
0 ·
x1 +
-∞
|
| [goright(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish2(x1)] |
= |
8 ·
x1 +
-∞
|
| [wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [d(x1)] |
= |
14 ·
x1 +
-∞
|
| [Ac(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ad(x1)] |
= |
14 ·
x1 +
-∞
|
| [Cc(x1)] |
= |
0 ·
x1 +
-∞
|
| [Cb(x1)] |
= |
0 ·
x1 +
-∞
|
| [Cd(x1)] |
= |
14 ·
x1 +
-∞
|
| [cut(x1)] |
= |
3 ·
x1 +
-∞
|
| [Dd(x1)] |
= |
14 ·
x1 +
-∞
|
| [rewrite(x1)] |
= |
5 ·
x1 +
-∞
|
the
rules
|
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 Rule Removal
Using the
Knuth Bendix order with w0 = 1 and the following precedence and weight function
| prec(finish2) |
= |
0 |
|
weight(finish2) |
= |
1 |
|
|
|
| prec(Dd) |
= |
2 |
|
weight(Dd) |
= |
1 |
|
|
|
| prec(Dc) |
= |
1 |
|
weight(Dc) |
= |
1 |
|
|
|
| prec(Db) |
= |
2 |
|
weight(Db) |
= |
1 |
|
|
|
| prec(Da) |
= |
2 |
|
weight(Da) |
= |
1 |
|
|
|
| prec(goright) |
= |
2 |
|
weight(goright) |
= |
1 |
|
|
|
| prec(Ad) |
= |
0 |
|
weight(Ad) |
= |
1 |
|
|
|
| prec(Ac) |
= |
0 |
|
weight(Ac) |
= |
1 |
|
|
|
| prec(Ab) |
= |
0 |
|
weight(Ab) |
= |
1 |
|
|
|
| prec(Aa) |
= |
0 |
|
weight(Aa) |
= |
1 |
|
|
|
| prec(finish) |
= |
0 |
|
weight(finish) |
= |
1 |
|
|
|
| prec(Bd) |
= |
0 |
|
weight(Bd) |
= |
1 |
|
|
|
| prec(Bc) |
= |
0 |
|
weight(Bc) |
= |
1 |
|
|
|
| prec(Bb) |
= |
0 |
|
weight(Bb) |
= |
1 |
|
|
|
| prec(moveleft) |
= |
0 |
|
weight(moveleft) |
= |
1 |
|
|
|
| prec(Ba) |
= |
0 |
|
weight(Ba) |
= |
1 |
|
|
|
| prec(wait) |
= |
11 |
|
weight(wait) |
= |
0 |
|
|
|
| prec(Cd) |
= |
1 |
|
weight(Cd) |
= |
1 |
|
|
|
| prec(d) |
= |
0 |
|
weight(d) |
= |
1 |
|
|
|
| prec(Cc) |
= |
1 |
|
weight(Cc) |
= |
1 |
|
|
|
| prec(c) |
= |
0 |
|
weight(c) |
= |
1 |
|
|
|
| prec(Cb) |
= |
1 |
|
weight(Cb) |
= |
1 |
|
|
|
| prec(b) |
= |
0 |
|
weight(b) |
= |
1 |
|
|
|
| prec(cut) |
= |
3 |
|
weight(cut) |
= |
1 |
|
|
|
| prec(Ca) |
= |
1 |
|
weight(Ca) |
= |
1 |
|
|
|
| prec(guess) |
= |
4 |
|
weight(guess) |
= |
1 |
|
|
|
| prec(a) |
= |
0 |
|
weight(a) |
= |
1 |
|
|
|
| prec(end) |
= |
0 |
|
weight(end) |
= |
1 |
|
|
|
all rules could be removed.
1.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.