YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
Begin(b(b(x0))) |
→ |
Wait(Right1(x0)) |
|
Begin(b(x0)) |
→ |
Wait(Right2(x0)) |
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(d(x0)) |
→ |
Wait(Right4(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right1(b(End(x0))) |
→ |
Left(c(d(c(End(x0))))) |
|
Right2(b(b(End(x0)))) |
→ |
Left(c(d(c(End(x0))))) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right4(c(End(x0))) |
→ |
Left(g(g(End(x0)))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right1(c(x0)) |
→ |
Ac(Right1(x0)) |
|
Right2(c(x0)) |
→ |
Ac(Right2(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right4(c(x0)) |
→ |
Ac(Right4(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(b(x0))) |
→ |
c(d(c(x0))) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
c(d(x0)) |
→ |
g(g(x0)) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Ab(x1)] |
= |
3 ·
x1 +
-∞
|
| [Right2(x1)] |
= |
4 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
2 ·
x1 +
-∞
|
| [g(x1)] |
= |
2 ·
x1 +
-∞
|
| [Begin(x1)] |
= |
2 ·
x1 +
-∞
|
| [Wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ag(x1)] |
= |
2 ·
x1 +
-∞
|
| [Ac(x1)] |
= |
4 ·
x1 +
-∞
|
| [Ad(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right3(x1)] |
= |
5 ·
x1 +
-∞
|
| [Right6(x1)] |
= |
4 ·
x1 +
-∞
|
| [b(x1)] |
= |
3 ·
x1 +
-∞
|
| [Right4(x1)] |
= |
2 ·
x1 +
-∞
|
| [a(x1)] |
= |
2 ·
x1 +
-∞
|
| [c(x1)] |
= |
4 ·
x1 +
-∞
|
| [End(x1)] |
= |
1 ·
x1 +
-∞
|
| [Right5(x1)] |
= |
6 ·
x1 +
-∞
|
| [Left(x1)] |
= |
2 ·
x1 +
-∞
|
| [d(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right1(x1)] |
= |
8 ·
x1 +
-∞
|
the
rules
|
Begin(b(b(x0))) |
→ |
Wait(Right1(x0)) |
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(d(x0)) |
→ |
Wait(Right4(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right2(b(b(End(x0)))) |
→ |
Left(c(d(c(End(x0))))) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right4(c(End(x0))) |
→ |
Left(g(g(End(x0)))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right1(c(x0)) |
→ |
Ac(Right1(x0)) |
|
Right2(c(x0)) |
→ |
Ac(Right2(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right4(c(x0)) |
→ |
Ac(Right4(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
c(d(x0)) |
→ |
g(g(x0)) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
remain.
1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Ab(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right2(x1)] |
= |
10 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
0 ·
x1 +
-∞
|
| [g(x1)] |
= |
0 ·
x1 +
-∞
|
| [Begin(x1)] |
= |
0 ·
x1 +
-∞
|
| [Wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ag(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ac(x1)] |
= |
5 ·
x1 +
-∞
|
| [Ad(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right3(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right6(x1)] |
= |
0 ·
x1 +
-∞
|
| [b(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right4(x1)] |
= |
0 ·
x1 +
-∞
|
| [a(x1)] |
= |
0 ·
x1 +
-∞
|
| [c(x1)] |
= |
5 ·
x1 +
-∞
|
| [End(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right5(x1)] |
= |
0 ·
x1 +
-∞
|
| [Left(x1)] |
= |
0 ·
x1 +
-∞
|
| [d(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right1(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
Begin(b(b(x0))) |
→ |
Wait(Right1(x0)) |
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(d(x0)) |
→ |
Wait(Right4(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right2(b(b(End(x0)))) |
→ |
Left(c(d(c(End(x0))))) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right1(c(x0)) |
→ |
Ac(Right1(x0)) |
|
Right2(c(x0)) |
→ |
Ac(Right2(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right4(c(x0)) |
→ |
Ac(Right4(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
remain.
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [Ab(x1)] |
= |
1 ·
x1 + 0 |
| [Right2(x1)] |
= |
11 ·
x1 + 0 |
| [Aa(x1)] |
= |
1 ·
x1 + 0 |
| [g(x1)] |
= |
1 ·
x1 + 0 |
| [Begin(x1)] |
= |
8 ·
x1 + 6 |
| [Wait(x1)] |
= |
1 ·
x1 + 0 |
| [Ag(x1)] |
= |
1 ·
x1 + 0 |
| [Ac(x1)] |
= |
1 ·
x1 + 0 |
| [Ad(x1)] |
= |
1 ·
x1 + 0 |
| [Right3(x1)] |
= |
8 ·
x1 + 6 |
| [Right6(x1)] |
= |
8 ·
x1 + 6 |
| [b(x1)] |
= |
1 ·
x1 + 0 |
| [Right4(x1)] |
= |
4 ·
x1 + 0 |
| [a(x1)] |
= |
1 ·
x1 + 0 |
| [c(x1)] |
= |
1 ·
x1 + 0 |
| [End(x1)] |
= |
1 ·
x1 + 2 |
| [Right5(x1)] |
= |
8 ·
x1 + 6 |
| [Left(x1)] |
= |
8 ·
x1 + 6 |
| [d(x1)] |
= |
1 ·
x1 + 0 |
| [Right1(x1)] |
= |
2 ·
x1 + 0 |
the
rules
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right2(b(b(End(x0)))) |
→ |
Left(c(d(c(End(x0))))) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right1(c(x0)) |
→ |
Ac(Right1(x0)) |
|
Right2(c(x0)) |
→ |
Ac(Right2(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right4(c(x0)) |
→ |
Ac(Right4(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
remain.
1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Ab(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right2(x1)] |
= |
3 ·
x1 +
-∞
|
| [Aa(x1)] |
= |
0 ·
x1 +
-∞
|
| [g(x1)] |
= |
0 ·
x1 +
-∞
|
| [Begin(x1)] |
= |
0 ·
x1 +
-∞
|
| [Wait(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ag(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ac(x1)] |
= |
1 ·
x1 +
-∞
|
| [Ad(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right3(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right6(x1)] |
= |
0 ·
x1 +
-∞
|
| [b(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right4(x1)] |
= |
0 ·
x1 +
-∞
|
| [a(x1)] |
= |
0 ·
x1 +
-∞
|
| [c(x1)] |
= |
1 ·
x1 +
-∞
|
| [End(x1)] |
= |
3 ·
x1 +
-∞
|
| [Right5(x1)] |
= |
0 ·
x1 +
-∞
|
| [Left(x1)] |
= |
0 ·
x1 +
-∞
|
| [d(x1)] |
= |
0 ·
x1 +
-∞
|
| [Right1(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right1(c(x0)) |
→ |
Ac(Right1(x0)) |
|
Right2(c(x0)) |
→ |
Ac(Right2(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right4(c(x0)) |
→ |
Ac(Right4(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
remain.
1.1.1.1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
|
b(Begin(x0)) |
→ |
Right3(Wait(x0)) |
|
g(g(Begin(x0))) |
→ |
Right5(Wait(x0)) |
|
g(Begin(x0)) |
→ |
Right6(Wait(x0)) |
|
End(b(Right3(x0))) |
→ |
End(g(g(a(Left(x0))))) |
|
End(g(Right5(x0))) |
→ |
End(b(b(Left(x0)))) |
|
End(g(g(Right6(x0)))) |
→ |
End(b(b(Left(x0)))) |
|
a(Right1(x0)) |
→ |
Right1(Aa(x0)) |
|
a(Right2(x0)) |
→ |
Right2(Aa(x0)) |
|
a(Right3(x0)) |
→ |
Right3(Aa(x0)) |
|
a(Right4(x0)) |
→ |
Right4(Aa(x0)) |
|
a(Right5(x0)) |
→ |
Right5(Aa(x0)) |
|
a(Right6(x0)) |
→ |
Right6(Aa(x0)) |
|
g(Right1(x0)) |
→ |
Right1(Ag(x0)) |
|
g(Right2(x0)) |
→ |
Right2(Ag(x0)) |
|
g(Right3(x0)) |
→ |
Right3(Ag(x0)) |
|
g(Right4(x0)) |
→ |
Right4(Ag(x0)) |
|
g(Right5(x0)) |
→ |
Right5(Ag(x0)) |
|
g(Right6(x0)) |
→ |
Right6(Ag(x0)) |
|
d(Right1(x0)) |
→ |
Right1(Ad(x0)) |
|
d(Right2(x0)) |
→ |
Right2(Ad(x0)) |
|
d(Right3(x0)) |
→ |
Right3(Ad(x0)) |
|
d(Right4(x0)) |
→ |
Right4(Ad(x0)) |
|
d(Right5(x0)) |
→ |
Right5(Ad(x0)) |
|
d(Right6(x0)) |
→ |
Right6(Ad(x0)) |
|
b(Right1(x0)) |
→ |
Right1(Ab(x0)) |
|
b(Right2(x0)) |
→ |
Right2(Ab(x0)) |
|
b(Right3(x0)) |
→ |
Right3(Ab(x0)) |
|
b(Right4(x0)) |
→ |
Right4(Ab(x0)) |
|
b(Right5(x0)) |
→ |
Right5(Ab(x0)) |
|
b(Right6(x0)) |
→ |
Right6(Ab(x0)) |
|
c(Right1(x0)) |
→ |
Right1(Ac(x0)) |
|
c(Right2(x0)) |
→ |
Right2(Ac(x0)) |
|
c(Right3(x0)) |
→ |
Right3(Ac(x0)) |
|
c(Right4(x0)) |
→ |
Right4(Ac(x0)) |
|
c(Right5(x0)) |
→ |
Right5(Ac(x0)) |
|
c(Right6(x0)) |
→ |
Right6(Ac(x0)) |
|
Left(Aa(x0)) |
→ |
a(Left(x0)) |
|
Left(Ag(x0)) |
→ |
g(Left(x0)) |
|
Left(Ad(x0)) |
→ |
d(Left(x0)) |
|
Left(Ab(x0)) |
→ |
b(Left(x0)) |
|
Left(Ac(x0)) |
→ |
c(Left(x0)) |
|
Left(Wait(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
d(g(x0)) |
|
b(b(x0)) |
→ |
g(g(a(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [Ab(x1)] |
= |
1 ·
x1 + 0 |
| [Right2(x1)] |
= |
4 ·
x1 + 0 |
| [Aa(x1)] |
= |
1 ·
x1 + 0 |
| [g(x1)] |
= |
1 ·
x1 + 0 |
| [Begin(x1)] |
= |
2 ·
x1 + 0 |
| [Wait(x1)] |
= |
1 ·
x1 + 0 |
| [Ag(x1)] |
= |
1 ·
x1 + 0 |
| [Ac(x1)] |
= |
2 ·
x1 + 0 |
| [Ad(x1)] |
= |
1 ·
x1 + 0 |
| [Right3(x1)] |
= |
2 ·
x1 + 0 |
| [Right6(x1)] |
= |
2 ·
x1 + 0 |
| [b(x1)] |
= |
1 ·
x1 + 0 |
| [Right4(x1)] |
= |
1 ·
x1 + 0 |
| [a(x1)] |
= |
1 ·
x1 + 0 |
| [c(x1)] |
= |
2 ·
x1 + 0 |
| [End(x1)] |
= |
1 ·
x1 + 0 |
| [Right5(x1)] |
= |
2 ·
x1 + 0 |
| [Left(x1)] |
= |
2 ·
x1 + 0 |
| [d(x1)] |
= |
1 ·
x1 + 0 |
| [Right1(x1)] |
= |
4 ·
x1 + 8 |
the
rules
|
b(Begin(x0)) |
→ |
Right3(Wait(x0)) |
|
g(g(Begin(x0))) |
→ |
Right5(Wait(x0)) |
|
g(Begin(x0)) |
→ |
Right6(Wait(x0)) |
|
End(b(Right3(x0))) |
→ |
End(g(g(a(Left(x0))))) |
|
End(g(Right5(x0))) |
→ |
End(b(b(Left(x0)))) |
|
End(g(g(Right6(x0)))) |
→ |
End(b(b(Left(x0)))) |
|
a(Right1(x0)) |
→ |
Right1(Aa(x0)) |
|
a(Right2(x0)) |
→ |
Right2(Aa(x0)) |
|
a(Right3(x0)) |
→ |
Right3(Aa(x0)) |
|
a(Right4(x0)) |
→ |
Right4(Aa(x0)) |
|
a(Right5(x0)) |
→ |
Right5(Aa(x0)) |
|
a(Right6(x0)) |
→ |
Right6(Aa(x0)) |
|
g(Right1(x0)) |
→ |
Right1(Ag(x0)) |
|
g(Right2(x0)) |
→ |
Right2(Ag(x0)) |
|
g(Right3(x0)) |
→ |
Right3(Ag(x0)) |
|
g(Right4(x0)) |
→ |
Right4(Ag(x0)) |
|
g(Right5(x0)) |
→ |
Right5(Ag(x0)) |
|
g(Right6(x0)) |
→ |
Right6(Ag(x0)) |
|
d(Right1(x0)) |
→ |
Right1(Ad(x0)) |
|
d(Right2(x0)) |
→ |
Right2(Ad(x0)) |
|
d(Right3(x0)) |
→ |
Right3(Ad(x0)) |
|
d(Right4(x0)) |
→ |
Right4(Ad(x0)) |
|
d(Right5(x0)) |
→ |
Right5(Ad(x0)) |
|
d(Right6(x0)) |
→ |
Right6(Ad(x0)) |
|
b(Right1(x0)) |
→ |
Right1(Ab(x0)) |
|
b(Right2(x0)) |
→ |
Right2(Ab(x0)) |
|
b(Right3(x0)) |
→ |
Right3(Ab(x0)) |
|
b(Right4(x0)) |
→ |
Right4(Ab(x0)) |
|
b(Right5(x0)) |
→ |
Right5(Ab(x0)) |
|
b(Right6(x0)) |
→ |
Right6(Ab(x0)) |
|
c(Right2(x0)) |
→ |
Right2(Ac(x0)) |
|
c(Right3(x0)) |
→ |
Right3(Ac(x0)) |
|
c(Right4(x0)) |
→ |
Right4(Ac(x0)) |
|
c(Right5(x0)) |
→ |
Right5(Ac(x0)) |
|
c(Right6(x0)) |
→ |
Right6(Ac(x0)) |
|
Left(Aa(x0)) |
→ |
a(Left(x0)) |
|
Left(Ag(x0)) |
→ |
g(Left(x0)) |
|
Left(Ad(x0)) |
→ |
d(Left(x0)) |
|
Left(Ab(x0)) |
→ |
b(Left(x0)) |
|
Left(Ac(x0)) |
→ |
c(Left(x0)) |
|
Left(Wait(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
d(g(x0)) |
|
b(b(x0)) |
→ |
g(g(a(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
remain.
1.1.1.1.1.1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right2(c(x0)) |
→ |
Ac(Right2(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right4(c(x0)) |
→ |
Ac(Right4(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
1.1.1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [Ab(x1)] |
= |
1 ·
x1 + 0 |
| [Right2(x1)] |
= |
2 ·
x1 + 2 |
| [Aa(x1)] |
= |
1 ·
x1 + 0 |
| [g(x1)] |
= |
1 ·
x1 + 0 |
| [Begin(x1)] |
= |
4 ·
x1 + 0 |
| [Wait(x1)] |
= |
2 ·
x1 + 0 |
| [Ag(x1)] |
= |
1 ·
x1 + 0 |
| [Ac(x1)] |
= |
1 ·
x1 + 2 |
| [Ad(x1)] |
= |
1 ·
x1 + 0 |
| [Right3(x1)] |
= |
2 ·
x1 + 0 |
| [Right6(x1)] |
= |
2 ·
x1 + 0 |
| [b(x1)] |
= |
1 ·
x1 + 0 |
| [Right4(x1)] |
= |
3 ·
x1 + 0 |
| [a(x1)] |
= |
1 ·
x1 + 0 |
| [c(x1)] |
= |
1 ·
x1 + 1 |
| [End(x1)] |
= |
1 ·
x1 + 0 |
| [Right5(x1)] |
= |
2 ·
x1 + 0 |
| [Left(x1)] |
= |
2 ·
x1 + 0 |
| [d(x1)] |
= |
1 ·
x1 + 0 |
| [Right1(x1)] |
= |
1 ·
x1 + 0 |
the
rules
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right2(c(x0)) |
→ |
Ac(Right2(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
remain.
1.1.1.1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [Ab(x1)] |
= |
1 ·
x1 + 0 |
| [Right2(x1)] |
= |
6 ·
x1 + 6 |
| [Aa(x1)] |
= |
1 ·
x1 + 0 |
| [g(x1)] |
= |
1 ·
x1 + 0 |
| [Begin(x1)] |
= |
4 ·
x1 + 0 |
| [Wait(x1)] |
= |
2 ·
x1 + 0 |
| [Ag(x1)] |
= |
1 ·
x1 + 0 |
| [Ac(x1)] |
= |
1 ·
x1 + 4 |
| [Ad(x1)] |
= |
1 ·
x1 + 0 |
| [Right3(x1)] |
= |
2 ·
x1 + 0 |
| [Right6(x1)] |
= |
2 ·
x1 + 0 |
| [b(x1)] |
= |
1 ·
x1 + 0 |
| [Right4(x1)] |
= |
2 ·
x1 + 0 |
| [a(x1)] |
= |
1 ·
x1 + 0 |
| [c(x1)] |
= |
1 ·
x1 + 2 |
| [End(x1)] |
= |
2 ·
x1 + 0 |
| [Right5(x1)] |
= |
2 ·
x1 + 0 |
| [Left(x1)] |
= |
2 ·
x1 + 0 |
| [d(x1)] |
= |
1 ·
x1 + 0 |
| [Right1(x1)] |
= |
2 ·
x1 + 0 |
the
rules
|
Begin(b(x0)) |
→ |
Wait(Right3(x0)) |
|
Begin(g(g(x0))) |
→ |
Wait(Right5(x0)) |
|
Begin(g(x0)) |
→ |
Wait(Right6(x0)) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right1(a(x0)) |
→ |
Aa(Right1(x0)) |
|
Right2(a(x0)) |
→ |
Aa(Right2(x0)) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right4(a(x0)) |
→ |
Aa(Right4(x0)) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right1(g(x0)) |
→ |
Ag(Right1(x0)) |
|
Right2(g(x0)) |
→ |
Ag(Right2(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right4(g(x0)) |
→ |
Ag(Right4(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right1(d(x0)) |
→ |
Ad(Right1(x0)) |
|
Right2(d(x0)) |
→ |
Ad(Right2(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right4(d(x0)) |
→ |
Ad(Right4(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right1(b(x0)) |
→ |
Ab(Right1(x0)) |
|
Right2(b(x0)) |
→ |
Ab(Right2(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right4(b(x0)) |
→ |
Ab(Right4(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Wait(Left(x0)) |
→ |
Begin(x0) |
|
a(x0) |
→ |
g(d(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
remain.
1.1.1.1.1.1.1.1.1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
Begin#(b(x0)) |
→ |
Right3#(x0) |
|
Begin#(b(x0)) |
→ |
Wait#(Right3(x0)) |
|
Begin#(g(g(x0))) |
→ |
Right5#(x0) |
|
Begin#(g(g(x0))) |
→ |
Wait#(Right5(x0)) |
|
Begin#(g(x0)) |
→ |
Right6#(x0) |
|
Begin#(g(x0)) |
→ |
Wait#(Right6(x0)) |
|
Right3#(b(End(x0))) |
→ |
g#(End(x0)) |
|
Right3#(b(End(x0))) |
→ |
g#(g(End(x0))) |
|
Right3#(b(End(x0))) |
→ |
a#(g(g(End(x0)))) |
|
Right5#(g(End(x0))) |
→ |
b#(End(x0)) |
|
Right5#(g(End(x0))) |
→ |
b#(b(End(x0))) |
|
Right6#(g(g(End(x0)))) |
→ |
b#(End(x0)) |
|
Right6#(g(g(End(x0)))) |
→ |
b#(b(End(x0))) |
|
Right1#(a(x0)) |
→ |
Right1#(x0) |
|
Right1#(a(x0)) |
→ |
Aa#(Right1(x0)) |
|
Right2#(a(x0)) |
→ |
Right2#(x0) |
|
Right2#(a(x0)) |
→ |
Aa#(Right2(x0)) |
|
Right3#(a(x0)) |
→ |
Right3#(x0) |
|
Right3#(a(x0)) |
→ |
Aa#(Right3(x0)) |
|
Right4#(a(x0)) |
→ |
Right4#(x0) |
|
Right4#(a(x0)) |
→ |
Aa#(Right4(x0)) |
|
Right5#(a(x0)) |
→ |
Right5#(x0) |
|
Right5#(a(x0)) |
→ |
Aa#(Right5(x0)) |
|
Right6#(a(x0)) |
→ |
Right6#(x0) |
|
Right6#(a(x0)) |
→ |
Aa#(Right6(x0)) |
|
Right1#(g(x0)) |
→ |
Right1#(x0) |
|
Right1#(g(x0)) |
→ |
Ag#(Right1(x0)) |
|
Right2#(g(x0)) |
→ |
Right2#(x0) |
|
Right2#(g(x0)) |
→ |
Ag#(Right2(x0)) |
|
Right3#(g(x0)) |
→ |
Right3#(x0) |
|
Right3#(g(x0)) |
→ |
Ag#(Right3(x0)) |
|
Right4#(g(x0)) |
→ |
Right4#(x0) |
|
Right4#(g(x0)) |
→ |
Ag#(Right4(x0)) |
|
Right5#(g(x0)) |
→ |
Right5#(x0) |
|
Right5#(g(x0)) |
→ |
Ag#(Right5(x0)) |
|
Right6#(g(x0)) |
→ |
Right6#(x0) |
|
Right6#(g(x0)) |
→ |
Ag#(Right6(x0)) |
|
Right1#(d(x0)) |
→ |
Right1#(x0) |
|
Right1#(d(x0)) |
→ |
Ad#(Right1(x0)) |
|
Right2#(d(x0)) |
→ |
Right2#(x0) |
|
Right2#(d(x0)) |
→ |
Ad#(Right2(x0)) |
|
Right3#(d(x0)) |
→ |
Right3#(x0) |
|
Right3#(d(x0)) |
→ |
Ad#(Right3(x0)) |
|
Right4#(d(x0)) |
→ |
Right4#(x0) |
|
Right4#(d(x0)) |
→ |
Ad#(Right4(x0)) |
|
Right5#(d(x0)) |
→ |
Right5#(x0) |
|
Right5#(d(x0)) |
→ |
Ad#(Right5(x0)) |
|
Right6#(d(x0)) |
→ |
Right6#(x0) |
|
Right6#(d(x0)) |
→ |
Ad#(Right6(x0)) |
|
Right1#(b(x0)) |
→ |
Right1#(x0) |
|
Right1#(b(x0)) |
→ |
Ab#(Right1(x0)) |
|
Right2#(b(x0)) |
→ |
Right2#(x0) |
|
Right2#(b(x0)) |
→ |
Ab#(Right2(x0)) |
|
Right3#(b(x0)) |
→ |
Right3#(x0) |
|
Right3#(b(x0)) |
→ |
Ab#(Right3(x0)) |
|
Right4#(b(x0)) |
→ |
Right4#(x0) |
|
Right4#(b(x0)) |
→ |
Ab#(Right4(x0)) |
|
Right5#(b(x0)) |
→ |
Right5#(x0) |
|
Right5#(b(x0)) |
→ |
Ab#(Right5(x0)) |
|
Right6#(b(x0)) |
→ |
Right6#(x0) |
|
Right6#(b(x0)) |
→ |
Ab#(Right6(x0)) |
|
Right3#(c(x0)) |
→ |
Right3#(x0) |
|
Right3#(c(x0)) |
→ |
Ac#(Right3(x0)) |
|
Right5#(c(x0)) |
→ |
Right5#(x0) |
|
Right5#(c(x0)) |
→ |
Ac#(Right5(x0)) |
|
Right6#(c(x0)) |
→ |
Right6#(x0) |
|
Right6#(c(x0)) |
→ |
Ac#(Right6(x0)) |
|
Aa#(Left(x0)) |
→ |
a#(x0) |
|
Ag#(Left(x0)) |
→ |
g#(x0) |
|
Ab#(Left(x0)) |
→ |
b#(x0) |
|
Wait#(Left(x0)) |
→ |
Begin#(x0) |
|
a#(x0) |
→ |
g#(d(x0)) |
|
b#(b(x0)) |
→ |
g#(x0) |
|
b#(b(x0)) |
→ |
g#(g(x0)) |
|
b#(b(x0)) |
→ |
a#(g(g(x0))) |
|
g#(g(g(x0))) |
→ |
b#(x0) |
|
g#(g(g(x0))) |
→ |
b#(b(x0)) |
1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 8
components.
-
The
1st
component contains the
pairs
|
Wait#(Left(x0)) |
→ |
Begin#(x0) |
|
Begin#(g(x0)) |
→ |
Wait#(Right6(x0)) |
|
Begin#(g(g(x0))) |
→ |
Wait#(Right5(x0)) |
|
Begin#(b(x0)) |
→ |
Wait#(Right3(x0)) |
1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [Ab(x1)] |
= |
4 ·
x1 + 0 |
| [Aa(x1)] |
= |
-∞
·
x1 + 8 |
| [g(x1)] |
= |
4 ·
x1 + 0 |
| [Ag(x1)] |
= |
4 ·
x1 + 0 |
| [Ac(x1)] |
= |
-∞
·
x1 + 12 |
| [Ad(x1)] |
= |
-∞
·
x1 + 4 |
| [Wait#(x1)] |
= |
0 ·
x1 + 0 |
| [Right3(x1)] |
= |
4 ·
x1 +
-∞
|
| [Right6(x1)] |
= |
4 ·
x1 +
-∞
|
| [b(x1)] |
= |
4 ·
x1 + 0 |
| [Begin#(x1)] |
= |
0 ·
x1 +
-∞
|
| [a(x1)] |
= |
-∞
·
x1 + 4 |
| [c(x1)] |
= |
-∞
·
x1 + 8 |
| [End(x1)] |
= |
-∞
·
x1 + 4 |
| [Right5(x1)] |
= |
8 ·
x1 + 4 |
| [Left(x1)] |
= |
4 ·
x1 + 0 |
| [d(x1)] |
= |
-∞
·
x1 + 0 |
together with the usable
rules
|
Right6(g(g(End(x0)))) |
→ |
Left(b(b(End(x0)))) |
|
Right6(a(x0)) |
→ |
Aa(Right6(x0)) |
|
Right6(g(x0)) |
→ |
Ag(Right6(x0)) |
|
Right6(d(x0)) |
→ |
Ad(Right6(x0)) |
|
Right6(b(x0)) |
→ |
Ab(Right6(x0)) |
|
Right6(c(x0)) |
→ |
Ac(Right6(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
a(x0) |
→ |
g(d(x0)) |
|
g(g(g(x0))) |
→ |
b(b(x0)) |
|
Aa(Left(x0)) |
→ |
Left(a(x0)) |
|
Ag(Left(x0)) |
→ |
Left(g(x0)) |
|
Ad(Left(x0)) |
→ |
Left(d(x0)) |
|
Ab(Left(x0)) |
→ |
Left(b(x0)) |
|
Ac(Left(x0)) |
→ |
Left(c(x0)) |
|
Right5(g(End(x0))) |
→ |
Left(b(b(End(x0)))) |
|
Right5(a(x0)) |
→ |
Aa(Right5(x0)) |
|
Right5(g(x0)) |
→ |
Ag(Right5(x0)) |
|
Right5(d(x0)) |
→ |
Ad(Right5(x0)) |
|
Right5(b(x0)) |
→ |
Ab(Right5(x0)) |
|
Right5(c(x0)) |
→ |
Ac(Right5(x0)) |
|
Right3(b(End(x0))) |
→ |
Left(a(g(g(End(x0))))) |
|
Right3(a(x0)) |
→ |
Aa(Right3(x0)) |
|
Right3(g(x0)) |
→ |
Ag(Right3(x0)) |
|
Right3(d(x0)) |
→ |
Ad(Right3(x0)) |
|
Right3(b(x0)) |
→ |
Ab(Right3(x0)) |
|
Right3(c(x0)) |
→ |
Ac(Right3(x0)) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
|
Begin#(g(x0)) |
→ |
Wait#(Right6(x0)) |
|
Begin#(g(g(x0))) |
→ |
Wait#(Right5(x0)) |
|
Begin#(b(x0)) |
→ |
Wait#(Right3(x0)) |
remain.
1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
2nd
component contains the
pairs
|
Right3#(c(x0)) |
→ |
Right3#(x0) |
|
Right3#(b(x0)) |
→ |
Right3#(x0) |
|
Right3#(d(x0)) |
→ |
Right3#(x0) |
|
Right3#(g(x0)) |
→ |
Right3#(x0) |
|
Right3#(a(x0)) |
→ |
Right3#(x0) |
1.1.1.1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1
over the arctic semiring over the integers
| [g(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [Right3#(x1)] |
= |
| 0 |
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
·
x1 +
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
| [b(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [a(x1)] |
= |
| 1 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [c(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [d(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
|
Right3#(c(x0)) |
→ |
Right3#(x0) |
|
Right3#(b(x0)) |
→ |
Right3#(x0) |
|
Right3#(d(x0)) |
→ |
Right3#(x0) |
|
Right3#(g(x0)) |
→ |
Right3#(x0) |
remain.
1.1.1.1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
3rd
component contains the
pairs
|
Right5#(a(x0)) |
→ |
Right5#(x0) |
|
Right5#(c(x0)) |
→ |
Right5#(x0) |
|
Right5#(b(x0)) |
→ |
Right5#(x0) |
|
Right5#(d(x0)) |
→ |
Right5#(x0) |
|
Right5#(g(x0)) |
→ |
Right5#(x0) |
1.1.1.1.1.1.1.1.1.1.1.3 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1
over the arctic semiring over the integers
| [g(x1)] |
= |
| 1 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [b(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [a(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [c(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [Right5#(x1)] |
= |
| 0 |
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
·
x1 +
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
| [d(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
|
Right5#(a(x0)) |
→ |
Right5#(x0) |
|
Right5#(c(x0)) |
→ |
Right5#(x0) |
|
Right5#(b(x0)) |
→ |
Right5#(x0) |
|
Right5#(d(x0)) |
→ |
Right5#(x0) |
remain.
1.1.1.1.1.1.1.1.1.1.1.3.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
4th
component contains the
pairs
|
Right6#(a(x0)) |
→ |
Right6#(x0) |
|
Right6#(c(x0)) |
→ |
Right6#(x0) |
|
Right6#(b(x0)) |
→ |
Right6#(x0) |
|
Right6#(d(x0)) |
→ |
Right6#(x0) |
|
Right6#(g(x0)) |
→ |
Right6#(x0) |
1.1.1.1.1.1.1.1.1.1.1.4 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the arctic semiring over the integers
| [g(x1)] |
= |
·
x1 +
|
| [b(x1)] |
= |
·
x1 +
|
| [a(x1)] |
= |
·
x1 +
|
| [c(x1)] |
= |
·
x1 +
|
| [Right6#(x1)] |
= |
| 1 |
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [d(x1)] |
= |
·
x1 +
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
|
Right6#(a(x0)) |
→ |
Right6#(x0) |
|
Right6#(c(x0)) |
→ |
Right6#(x0) |
|
Right6#(b(x0)) |
→ |
Right6#(x0) |
|
Right6#(d(x0)) |
→ |
Right6#(x0) |
remain.
1.1.1.1.1.1.1.1.1.1.1.4.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
5th
component contains the
pairs
|
Right1#(a(x0)) |
→ |
Right1#(x0) |
|
Right1#(b(x0)) |
→ |
Right1#(x0) |
|
Right1#(d(x0)) |
→ |
Right1#(x0) |
|
Right1#(g(x0)) |
→ |
Right1#(x0) |
1.1.1.1.1.1.1.1.1.1.1.5 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1
over the arctic semiring over the integers
| [g(x1)] |
= |
| 1 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [Right1#(x1)] |
= |
| 0 |
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
·
x1 +
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
| [b(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [a(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [d(x1)] |
= |
| 0 |
0 |
1 |
0 |
| 0 |
0 |
1 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
1 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
|
Right1#(a(x0)) |
→ |
Right1#(x0) |
|
Right1#(b(x0)) |
→ |
Right1#(x0) |
|
Right1#(d(x0)) |
→ |
Right1#(x0) |
remain.
1.1.1.1.1.1.1.1.1.1.1.5.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
6th
component contains the
pairs
|
Right2#(a(x0)) |
→ |
Right2#(x0) |
|
Right2#(b(x0)) |
→ |
Right2#(x0) |
|
Right2#(d(x0)) |
→ |
Right2#(x0) |
|
Right2#(g(x0)) |
→ |
Right2#(x0) |
1.1.1.1.1.1.1.1.1.1.1.6 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1
over the arctic semiring over the integers
| [g(x1)] |
= |
| 1 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [b(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [Right2#(x1)] |
= |
| 0 |
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
·
x1 +
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
| [a(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [d(x1)] |
= |
| 0 |
0 |
1 |
0 |
| 0 |
0 |
1 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
1 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
|
Right2#(a(x0)) |
→ |
Right2#(x0) |
|
Right2#(b(x0)) |
→ |
Right2#(x0) |
|
Right2#(d(x0)) |
→ |
Right2#(x0) |
remain.
1.1.1.1.1.1.1.1.1.1.1.6.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
7th
component contains the
pairs
|
Right4#(a(x0)) |
→ |
Right4#(x0) |
|
Right4#(b(x0)) |
→ |
Right4#(x0) |
|
Right4#(d(x0)) |
→ |
Right4#(x0) |
|
Right4#(g(x0)) |
→ |
Right4#(x0) |
1.1.1.1.1.1.1.1.1.1.1.7 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1
over the arctic semiring over the integers
| [g(x1)] |
= |
| 1 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 1 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [b(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [a(x1)] |
= |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
0 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
| [Right4#(x1)] |
= |
| 0 |
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
·
x1 +
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
-∞
|
|
| [d(x1)] |
= |
| 0 |
0 |
1 |
0 |
| 0 |
0 |
1 |
0 |
| 0 |
0 |
0 |
0 |
| 0 |
0 |
1 |
0 |
·
x1 +
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
| 0 |
-∞
|
-∞
|
-∞
|
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
|
Right4#(a(x0)) |
→ |
Right4#(x0) |
|
Right4#(b(x0)) |
→ |
Right4#(x0) |
|
Right4#(d(x0)) |
→ |
Right4#(x0) |
remain.
1.1.1.1.1.1.1.1.1.1.1.7.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
8th
component contains the
pairs
|
b#(b(x0)) |
→ |
g#(g(x0)) |
|
g#(g(g(x0))) |
→ |
b#(b(x0)) |
|
b#(b(x0)) |
→ |
g#(x0) |
|
g#(g(g(x0))) |
→ |
b#(x0) |
1.1.1.1.1.1.1.1.1.1.1.8 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [g(x1)] |
= |
3 ·
x1 + 6 |
| [b#(x1)] |
= |
4 ·
x1 + 0 |
| [b(x1)] |
= |
2 ·
x1 + 4 |
| [g#(x1)] |
= |
0 ·
x1 + 0 |
| [a(x1)] |
= |
-∞
·
x1 + 6 |
| [d(x1)] |
= |
-∞
·
x1 + 2 |
together with the usable
rules
|
g(g(g(x0))) |
→ |
b(b(x0)) |
|
b(b(x0)) |
→ |
a(g(g(x0))) |
|
a(x0) |
→ |
g(d(x0)) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
remains.
1.1.1.1.1.1.1.1.1.1.1.8.1 Dependency Graph Processor
The dependency pairs are split into 0
components.