The rewrite relation of the following TRS is considered.
[b#(x1)] |
= |
|
0 |
0 |
0 |
0 |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
|
|
· x1 +
|
1 |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
|
|
|
[b(x1)] |
= |
|
-∞ |
0 |
-∞ |
0 |
-∞ |
0 |
-∞ |
-∞ |
0 |
1 |
0 |
0 |
-∞ |
0 |
-∞ |
-∞ |
|
|
· x1 +
|
0 |
-∞ |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
1 |
-∞ |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
|
|
|
[a#(x1)] |
= |
|
0 |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
|
|
· x1 +
|
0 |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
-∞ |
|
|
|
[a(x1)] |
= |
|
0 |
0 |
0 |
0 |
-∞ |
0 |
-∞ |
-∞ |
0 |
0 |
0 |
0 |
0 |
0 |
-∞ |
0 |
|
|
· x1 +
|
0 |
-∞ |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
1 |
-∞ |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
|
|
|
[c(x1)] |
= |
|
0 |
0 |
0 |
0 |
0 |
0 |
-∞ |
0 |
1 |
0 |
0 |
1 |
0 |
0 |
0 |
0 |
|
|
· x1 +
|
0 |
-∞ |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
0 |
-∞ |
-∞ |
-∞ |
|
|
|
together with the usable
rulesThe dependency pairs are split into 1
component.