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(b(x0))) |
|
rewrite(b(b(b(x0)))) |
→ |
begin(a(x0)) |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Da(x1)] |
= |
4 ·
x1 +
-∞
|
| [guess(x1)] |
= |
0 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
4 ·
x1 +
-∞
|
| [b(x1)] |
= |
2 ·
x1 +
-∞
|
| [begin(x1)] |
= |
0 ·
x1 +
-∞
|
| [a(x1)] |
= |
4 ·
x1 +
-∞
|
| [Ab(x1)] |
= |
2 ·
x1 +
-∞
|
| [Db(x1)] |
= |
2 ·
x1 +
-∞
|
| [goright(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ca(x1)] |
= |
4 ·
x1 +
-∞
|
| [wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [end(x1)] |
= |
0 ·
x1 +
-∞
|
| [rotate(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish2(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish(x1)] |
= |
0 ·
x1 +
-∞
|
| [moveleft(x1)] |
= |
1 ·
x1 +
-∞
|
| [Ba(x1)] |
= |
3 ·
x1 +
-∞
|
| [Cb(x1)] |
= |
2 ·
x1 +
-∞
|
| [Bb(x1)] |
= |
1 ·
x1 +
-∞
|
| [cut(x1)] |
= |
0 ·
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)))) |
|
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(b(x0))) |
remain.
1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Da(x1)] |
= |
12 ·
x1 +
-∞
|
| [guess(x1)] |
= |
1 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
12 ·
x1 +
-∞
|
| [b(x1)] |
= |
1 ·
x1 +
-∞
|
| [begin(x1)] |
= |
12 ·
x1 +
-∞
|
| [a(x1)] |
= |
12 ·
x1 +
-∞
|
| [Ab(x1)] |
= |
1 ·
x1 +
-∞
|
| [Db(x1)] |
= |
1 ·
x1 +
-∞
|
| [goright(x1)] |
= |
1 ·
x1 +
-∞
|
| [Ca(x1)] |
= |
12 ·
x1 +
-∞
|
| [wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [end(x1)] |
= |
0 ·
x1 +
-∞
|
| [rotate(x1)] |
= |
4 ·
x1 +
-∞
|
| [finish2(x1)] |
= |
0 ·
x1 +
-∞
|
| [finish(x1)] |
= |
0 ·
x1 +
-∞
|
| [moveleft(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ba(x1)] |
= |
13 ·
x1 +
-∞
|
| [Cb(x1)] |
= |
1 ·
x1 +
-∞
|
| [Bb(x1)] |
= |
2 ·
x1 +
-∞
|
| [cut(x1)] |
= |
0 ·
x1 +
-∞
|
| [rewrite(x1)] |
= |
4 ·
x1 +
-∞
|
the
rules
|
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))) |
|
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))) |
|
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.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(Db) |
= |
1 |
|
weight(Db) |
= |
1 |
|
|
|
| prec(Da) |
= |
1 |
|
weight(Da) |
= |
1 |
|
|
|
| prec(goright) |
= |
2 |
|
weight(goright) |
= |
1 |
|
|
|
| prec(Ab) |
= |
0 |
|
weight(Ab) |
= |
1 |
|
|
|
| prec(Aa) |
= |
0 |
|
weight(Aa) |
= |
1 |
|
|
|
| prec(finish) |
= |
0 |
|
weight(finish) |
= |
1 |
|
|
|
| prec(Bb) |
= |
0 |
|
weight(Bb) |
= |
1 |
|
|
|
| prec(moveleft) |
= |
0 |
|
weight(moveleft) |
= |
1 |
|
|
|
| prec(Ba) |
= |
0 |
|
weight(Ba) |
= |
1 |
|
|
|
| prec(wait) |
= |
27 |
|
weight(wait) |
= |
0 |
|
|
|
| prec(Cb) |
= |
1 |
|
weight(Cb) |
= |
1 |
|
|
|
| prec(b) |
= |
0 |
|
weight(b) |
= |
1 |
|
|
|
| prec(rotate) |
= |
0 |
|
weight(rotate) |
= |
1 |
|
|
|
| prec(cut) |
= |
2 |
|
weight(cut) |
= |
1 |
|
|
|
| prec(Ca) |
= |
1 |
|
weight(Ca) |
= |
1 |
|
|
|
| prec(guess) |
= |
16 |
|
weight(guess) |
= |
1 |
|
|
|
| prec(a) |
= |
0 |
|
weight(a) |
= |
1 |
|
|
|
| prec(rewrite) |
= |
0 |
|
weight(rewrite) |
= |
1 |
|
|
|
all rules could be removed.
1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.