The rewrite relation of the following TRS is considered.
|
g(s(x),s(y)) |
→ |
if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))),g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) |
(1) |
|
n(0,y) |
→ |
0 |
(2) |
|
n(x,0) |
→ |
0 |
(3) |
|
n(s(x),s(y)) |
→ |
s(n(x,y)) |
(4) |
|
m(0,y) |
→ |
y |
(5) |
|
m(x,0) |
→ |
x |
(6) |
|
m(s(x),s(y)) |
→ |
s(m(x,y)) |
(7) |
|
k(0,s(y)) |
→ |
0 |
(8) |
|
k(s(x),s(y)) |
→ |
s(k(minus(x,y),s(y))) |
(9) |
|
t(x) |
→ |
p(x,x) |
(10) |
|
p(s(x),s(y)) |
→ |
s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) |
(11) |
|
p(s(x),x) |
→ |
p(if(gt(x,x),id(x),id(x)),s(x)) |
(12) |
|
p(0,y) |
→ |
y |
(13) |
|
p(id(x),s(y)) |
→ |
s(p(x,if(gt(s(y),y),y,s(y)))) |
(14) |
|
minus(x,0) |
→ |
x |
(15) |
|
minus(s(x),s(y)) |
→ |
minus(x,y) |
(16) |
|
id(x) |
→ |
x |
(17) |
|
if(true,x,y) |
→ |
x |
(18) |
|
if(false,x,y) |
→ |
y |
(19) |
|
not(x) |
→ |
if(x,false,true) |
(20) |
|
and(x,false) |
→ |
false |
(21) |
|
and(true,true) |
→ |
true |
(22) |
|
f(0) |
→ |
true |
(23) |
|
f(s(x)) |
→ |
h(x) |
(24) |
|
h(0) |
→ |
false |
(25) |
|
h(s(x)) |
→ |
f(x) |
(26) |
|
gt(s(x),0) |
→ |
true |
(27) |
|
gt(0,y) |
→ |
false |
(28) |
|
gt(s(x),s(y)) |
→ |
gt(x,y) |
(29) |
|
g#(s(x),s(y)) |
→ |
g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) |
(30) |
|
g#(s(x),s(y)) |
→ |
n#(s(x),s(y)) |
(31) |
|
g#(s(x),s(y)) |
→ |
k#(n(s(x),s(y)),s(s(0))) |
(32) |
|
g#(s(x),s(y)) |
→ |
n#(x,y) |
(33) |
|
g#(s(x),s(y)) |
→ |
m#(x,y) |
(34) |
|
g#(s(x),s(y)) |
→ |
minus#(m(x,y),n(x,y)) |
(35) |
|
g#(s(x),s(y)) |
→ |
k#(minus(m(x,y),n(x,y)),s(s(0))) |
(36) |
|
g#(s(x),s(y)) |
→ |
g#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0)))) |
(37) |
|
g#(s(x),s(y)) |
→ |
t#(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))) |
(38) |
|
g#(s(x),s(y)) |
→ |
f#(s(y)) |
(39) |
|
g#(s(x),s(y)) |
→ |
f#(s(x)) |
(40) |
|
g#(s(x),s(y)) |
→ |
and#(f(s(x)),f(s(y))) |
(41) |
|
g#(s(x),s(y)) |
→ |
if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))),g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) |
(42) |
|
n#(s(x),s(y)) |
→ |
n#(x,y) |
(43) |
|
m#(s(x),s(y)) |
→ |
m#(x,y) |
(44) |
|
k#(s(x),s(y)) |
→ |
minus#(x,y) |
(45) |
|
k#(s(x),s(y)) |
→ |
k#(minus(x,y),s(y)) |
(46) |
|
t#(x) |
→ |
p#(x,x) |
(47) |
|
p#(s(x),s(y)) |
→ |
id#(y) |
(48) |
|
p#(s(x),s(y)) |
→ |
id#(x) |
(49) |
|
p#(s(x),s(y)) |
→ |
not#(gt(x,y)) |
(50) |
|
p#(s(x),s(y)) |
→ |
if#(not(gt(x,y)),id(x),id(y)) |
(51) |
|
p#(s(x),s(y)) |
→ |
gt#(x,y) |
(52) |
|
p#(s(x),s(y)) |
→ |
if#(gt(x,y),x,y) |
(53) |
|
p#(s(x),s(y)) |
→ |
p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) |
(54) |
|
p#(s(x),x) |
→ |
id#(x) |
(55) |
|
p#(s(x),x) |
→ |
gt#(x,x) |
(56) |
|
p#(s(x),x) |
→ |
if#(gt(x,x),id(x),id(x)) |
(57) |
|
p#(s(x),x) |
→ |
p#(if(gt(x,x),id(x),id(x)),s(x)) |
(58) |
|
p#(id(x),s(y)) |
→ |
gt#(s(y),y) |
(59) |
|
p#(id(x),s(y)) |
→ |
if#(gt(s(y),y),y,s(y)) |
(60) |
|
p#(id(x),s(y)) |
→ |
p#(x,if(gt(s(y),y),y,s(y))) |
(61) |
|
minus#(s(x),s(y)) |
→ |
minus#(x,y) |
(62) |
|
not#(x) |
→ |
if#(x,false,true) |
(63) |
|
f#(s(x)) |
→ |
h#(x) |
(64) |
|
h#(s(x)) |
→ |
f#(x) |
(65) |
|
gt#(s(x),s(y)) |
→ |
gt#(x,y) |
(66) |
The dependency pairs are split into 8
components.
-
The
1st
component contains the
pair
|
g#(s(x),s(y)) |
→ |
g#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0)))) |
(37) |
|
g#(s(x),s(y)) |
→ |
g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) |
(30) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [g#(x1, x2)] |
= |
2 · x1 + 0 · x2 + 0 |
| [m(x1, x2)] |
= |
2 · x1 + 0 · x2 + 3 |
| [k(x1, x2)] |
= |
1 · x1 +
-∞ · x2 + 0 |
| [n(x1, x2)] |
= |
1 · x1 +
-∞ · x2 + 0 |
| [s(x1)] |
= |
3 · x1 + 4 |
| [0] |
= |
0 |
| [minus(x1, x2)] |
= |
0 · x1 +
-∞ · x2 + 1 |
together with the usable
rules
|
n(s(x),s(y)) |
→ |
s(n(x,y)) |
(4) |
|
n(0,y) |
→ |
0 |
(2) |
|
n(x,0) |
→ |
0 |
(3) |
|
k(0,s(y)) |
→ |
0 |
(8) |
|
k(s(x),s(y)) |
→ |
s(k(minus(x,y),s(y))) |
(9) |
|
minus(x,0) |
→ |
x |
(15) |
|
minus(s(x),s(y)) |
→ |
minus(x,y) |
(16) |
|
m(0,y) |
→ |
y |
(5) |
|
m(x,0) |
→ |
x |
(6) |
|
m(s(x),s(y)) |
→ |
s(m(x,y)) |
(7) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
|
g#(s(x),s(y)) |
→ |
g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) |
(30) |
could be deleted.
1.1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [g#(x1, x2)] |
= |
3 · x1 + 1 · x2 + 0 |
| [m(x1, x2)] |
= |
2 · x1 + 0 · x2 + 0 |
| [k(x1, x2)] |
= |
0 · x1 +
-∞ · x2 +
-∞ |
| [n(x1, x2)] |
= |
1 · x1 +
-∞ · x2 + 0 |
| [s(x1)] |
= |
3 · x1 + 2 |
| [0] |
= |
0 |
| [minus(x1, x2)] |
= |
0 · x1 +
-∞ · x2 +
-∞ |
together with the usable
rules
|
n(s(x),s(y)) |
→ |
s(n(x,y)) |
(4) |
|
n(0,y) |
→ |
0 |
(2) |
|
n(x,0) |
→ |
0 |
(3) |
|
k(0,s(y)) |
→ |
0 |
(8) |
|
k(s(x),s(y)) |
→ |
s(k(minus(x,y),s(y))) |
(9) |
|
minus(x,0) |
→ |
x |
(15) |
|
minus(s(x),s(y)) |
→ |
minus(x,y) |
(16) |
|
m(0,y) |
→ |
y |
(5) |
|
m(x,0) |
→ |
x |
(6) |
|
m(s(x),s(y)) |
→ |
s(m(x,y)) |
(7) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
|
g#(s(x),s(y)) |
→ |
g#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0)))) |
(37) |
could be deleted.
1.1.1.1.1 P is empty
There are no pairs anymore.
-
The
2nd
component contains the
pair
|
n#(s(x),s(y)) |
→ |
n#(x,y) |
(43) |
1.1.2 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
n#(s(x),s(y)) |
→ |
n#(x,y) |
(43) |
|
|
| 2 |
> |
2 |
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
3rd
component contains the
pair
|
k#(s(x),s(y)) |
→ |
k#(minus(x,y),s(y)) |
(46) |
1.1.3 Subterm Criterion Processor
We use the projection to multisets
| π(k#)
|
= |
{
1
}
|
| π(minus)
|
= |
{
1
}
|
to remove the pairs:
|
k#(s(x),s(y)) |
→ |
k#(minus(x,y),s(y)) |
(46) |
1.1.3.1 P is empty
There are no pairs anymore.
-
The
4th
component contains the
pair
|
m#(s(x),s(y)) |
→ |
m#(x,y) |
(44) |
1.1.4 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
m#(s(x),s(y)) |
→ |
m#(x,y) |
(44) |
|
|
| 2 |
> |
2 |
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
5th
component contains the
pair
|
minus#(s(x),s(y)) |
→ |
minus#(x,y) |
(62) |
1.1.5 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
minus#(s(x),s(y)) |
→ |
minus#(x,y) |
(62) |
|
|
| 2 |
> |
2 |
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
6th
component contains the
pair
|
p#(id(x),s(y)) |
→ |
p#(x,if(gt(s(y),y),y,s(y))) |
(61) |
|
p#(s(x),s(y)) |
→ |
p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) |
(54) |
|
p#(s(x),x) |
→ |
p#(if(gt(x,x),id(x),id(x)),s(x)) |
(58) |
1.1.6 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [true] |
= |
0 |
| [false] |
= |
0 |
| [p#(x1, x2)] |
= |
2 · x1 + 0 · x2 + 0 |
| [if(x1, x2, x3)] |
= |
0 · x1 + 0 · x2 + 0 · x3 + 0 |
| [s(x1)] |
= |
4 · x1 + 2 |
| [0] |
= |
2 |
| [id(x1)] |
= |
0 · x1 + 1 |
| [gt(x1, x2)] |
= |
-∞ · x1 + 2 · x2 + 1 |
| [not(x1)] |
= |
2 · x1 + 1 |
together with the usable
rules
|
gt(s(x),0) |
→ |
true |
(27) |
|
gt(s(x),s(y)) |
→ |
gt(x,y) |
(29) |
|
gt(0,y) |
→ |
false |
(28) |
|
if(true,x,y) |
→ |
x |
(18) |
|
if(false,x,y) |
→ |
y |
(19) |
|
id(x) |
→ |
x |
(17) |
|
not(x) |
→ |
if(x,false,true) |
(20) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
|
p#(s(x),x) |
→ |
p#(if(gt(x,x),id(x),id(x)),s(x)) |
(58) |
could be deleted.
1.1.6.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [true] |
= |
5 |
| [false] |
= |
1 |
| [p#(x1, x2)] |
= |
0 · x1 + 0 · x2 +
-∞ |
| [if(x1, x2, x3)] |
= |
-∞ · x1 + 0 · x2 + 0 · x3 +
-∞ |
| [s(x1)] |
= |
1 · x1 +
-∞ |
| [0] |
= |
1 |
| [id(x1)] |
= |
0 · x1 +
-∞ |
| [gt(x1, x2)] |
= |
0 · x1 + 4 · x2 + 3 |
| [not(x1)] |
= |
-∞ · x1 + 2 |
together with the usable
rules
|
if(true,x,y) |
→ |
x |
(18) |
|
if(false,x,y) |
→ |
y |
(19) |
|
id(x) |
→ |
x |
(17) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
|
p#(s(x),s(y)) |
→ |
p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) |
(54) |
could be deleted.
1.1.6.1.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
p#(id(x),s(y)) |
→ |
p#(x,if(gt(s(y),y),y,s(y))) |
(61) |
|
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
7th
component contains the
pair
|
gt#(s(x),s(y)) |
→ |
gt#(x,y) |
(66) |
1.1.7 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
gt#(s(x),s(y)) |
→ |
gt#(x,y) |
(66) |
|
|
| 2 |
> |
2 |
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
8th
component contains the
pair
|
h#(s(x)) |
→ |
f#(x) |
(65) |
|
f#(s(x)) |
→ |
h#(x) |
(64) |
1.1.8 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
h#(s(x)) |
→ |
f#(x) |
(65) |
|
| 1 |
> |
1 |
|
f#(s(x)) |
→ |
h#(x) |
(64) |
|
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.