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(a(x0))) → begin(b(b(b(x0))))
rewrite(b(b(b(b(b(x0)))))) → begin(a(a(a(x0))))

Proof

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)
a(a(rewrite(x0))) → b(b(b(begin(x0))))
b(b(b(b(b(rewrite(x0)))))) → a(a(a(begin(x0))))

1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[Da(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[guess(x1)] =
1 2
0 0
· x1 +
1 0
0 0
[Aa(x1)] =
1 0
0 1
· x1 +
0 0
0 0
[b(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[begin(x1)] =
1 0
0 0
· x1 +
3 0
1 0
[a(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[Ab(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[Db(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[goright(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[Ca(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[wait(x1)] =
1 0
0 0
· x1 +
1 0
0 0
[end(x1)] =
2 1
0 0
· x1 +
0 0
0 0
[rotate(x1)] =
1 0
0 0
· x1 +
2 0
0 0
[finish2(x1)] =
1 0
0 0
· x1 +
1 0
0 0
[finish(x1)] =
1 0
0 0
· x1 +
1 0
0 0
[moveleft(x1)] =
1 0
0 0
· x1 +
0 0
1 0
[Ba(x1)] =
1 0
0 0
· x1 +
0 0
2 0
[Cb(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[Bb(x1)] =
1 0
0 1
· x1 +
0 0
0 0
[cut(x1)] =
1 0
2 0
· x1 +
0 0
1 0
[rewrite(x1)] =
1 0
0 0
· x1 +
3 0
0 0
the rules
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)
a(a(rewrite(x0))) → b(b(b(begin(x0))))
b(b(b(b(b(rewrite(x0)))))) → a(a(a(begin(x0))))
remain.

1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Da(x1)] = 6 · x1 + -∞
[guess(x1)] = 10 · x1 + -∞
[Aa(x1)] = 6 · x1 + -∞
[b(x1)] = 4 · x1 + -∞
[begin(x1)] = 10 · x1 + -∞
[a(x1)] = 6 · x1 + -∞
[Ab(x1)] = 4 · x1 + -∞
[Db(x1)] = 4 · x1 + -∞
[goright(x1)] = 0 · x1 + -∞
[Ca(x1)] = 6 · x1 + -∞
[wait(x1)] = 10 · x1 + -∞
[end(x1)] = 0 · x1 + -∞
[rotate(x1)] = 0 · x1 + -∞
[finish2(x1)] = 10 · x1 + -∞
[finish(x1)] = 10 · x1 + -∞
[moveleft(x1)] = 1 · x1 + -∞
[Ba(x1)] = 5 · x1 + -∞
[Cb(x1)] = 4 · x1 + -∞
[Bb(x1)] = 3 · x1 + -∞
[cut(x1)] = 0 · x1 + -∞
[rewrite(x1)] = 10 · x1 + -∞
the rules
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)
a(a(rewrite(x0))) → b(b(b(begin(x0))))
remain.

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Da(x1)] = 14 · x1 + -∞
[guess(x1)] = 1 · x1 + -∞
[Aa(x1)] = 14 · x1 + -∞
[b(x1)] = 8 · x1 + -∞
[begin(x1)] = 3 · x1 + -∞
[a(x1)] = 14 · x1 + -∞
[Ab(x1)] = 8 · x1 + -∞
[Db(x1)] = 8 · x1 + -∞
[goright(x1)] = 0 · x1 + -∞
[Ca(x1)] = 14 · x1 + -∞
[wait(x1)] = 1 · x1 + -∞
[end(x1)] = 0 · x1 + -∞
[rotate(x1)] = 0 · x1 + -∞
[finish2(x1)] = 0 · x1 + -∞
[finish(x1)] = 0 · x1 + -∞
[moveleft(x1)] = 5 · x1 + -∞
[Ba(x1)] = 9 · x1 + -∞
[Cb(x1)] = 8 · x1 + -∞
[Bb(x1)] = 3 · x1 + -∞
[cut(x1)] = 2 · x1 + -∞
[rewrite(x1)] = 0 · x1 + -∞
the rules
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)))
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)))
finish(Ca(x0)) → a(finish(x0))
finish(Cb(x0)) → b(finish(x0))
finish2(Da(x0)) → a(finish2(x0))
finish2(Db(x0)) → b(finish2(x0))
finish2(rotate(x0)) → rewrite(x0)
remain.

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Da(x1)] = 14 · x1 + -∞
[guess(x1)] = 0 · x1 + -∞
[Aa(x1)] = 14 · x1 + -∞
[b(x1)] = 2 · x1 + -∞
[begin(x1)] = 1 · x1 + -∞
[a(x1)] = 14 · x1 + -∞
[Ab(x1)] = 2 · x1 + -∞
[Db(x1)] = 2 · x1 + -∞
[goright(x1)] = 0 · x1 + -∞
[Ca(x1)] = 14 · x1 + -∞
[wait(x1)] = 0 · x1 + -∞
[rotate(x1)] = 0 · x1 + -∞
[finish2(x1)] = 7 · x1 + -∞
[finish(x1)] = 8 · x1 + -∞
[moveleft(x1)] = 0 · x1 + -∞
[Ba(x1)] = 14 · x1 + -∞
[Cb(x1)] = 2 · x1 + -∞
[Bb(x1)] = 2 · x1 + -∞
[cut(x1)] = 1 · x1 + -∞
[rewrite(x1)] = 0 · x1 + -∞
the rules
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)))
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)))
finish(Ca(x0)) → a(finish(x0))
finish(Cb(x0)) → b(finish(x0))
finish2(Da(x0)) → a(finish2(x0))
finish2(Db(x0)) → b(finish2(x0))
remain.

1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Da(x1)] = 0 · x1 + -∞
[guess(x1)] = 2 · x1 + -∞
[Aa(x1)] = 0 · x1 + -∞
[b(x1)] = 1 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[Ab(x1)] = 1 · x1 + -∞
[Db(x1)] = 1 · x1 + -∞
[goright(x1)] = 0 · x1 + -∞
[Ca(x1)] = 0 · x1 + -∞
[wait(x1)] = 0 · x1 + -∞
[finish2(x1)] = 0 · x1 + -∞
[finish(x1)] = 0 · x1 + -∞
[moveleft(x1)] = 0 · x1 + -∞
[Ba(x1)] = 0 · x1 + -∞
[Cb(x1)] = 1 · x1 + -∞
[Bb(x1)] = 1 · x1 + -∞
[cut(x1)] = 0 · x1 + -∞
the rules
a(guess(x0)) → guess(Ca(x0))
b(guess(x0)) → guess(Cb(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)))
finish(Ca(x0)) → a(finish(x0))
finish(Cb(x0)) → b(finish(x0))
finish2(Da(x0)) → a(finish2(x0))
finish2(Db(x0)) → b(finish2(x0))
remain.

1.1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight function
prec(finish2) = 2 weight(finish2) = 1
prec(Db) = 0 weight(Db) = 1
prec(Da) = 0 weight(Da) = 1
prec(goright) = 0 weight(goright) = 1
prec(Ab) = 1 weight(Ab) = 1
prec(Aa) = 1 weight(Aa) = 1
prec(finish) = 2 weight(finish) = 1
prec(Bb) = 3 weight(Bb) = 1
prec(moveleft) = 0 weight(moveleft) = 1
prec(Ba) = 2 weight(Ba) = 1
prec(wait) = 0 weight(wait) = 1
prec(Cb) = 7 weight(Cb) = 1
prec(b) = 1 weight(b) = 1
prec(cut) = 0 weight(cut) = 1
prec(Ca) = 0 weight(Ca) = 1
prec(guess) = 0 weight(guess) = 1
prec(a) = 1 weight(a) = 1
all rules could be removed.

1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.