The rewrite relation of the following TRS is considered.
| check(0) | → | zero | (1) |
| check(s(0)) | → | odd | (2) |
| check(s(s(0))) | → | even | (3) |
| check(s(s(s(x)))) | → | check(s(x)) | (4) |
| half(0) | → | 0 | (5) |
| half(s(0)) | → | 0 | (6) |
| half(s(s(x))) | → | s(half(x)) | (7) |
| plus(0,y) | → | y | (8) |
| plus(s(x),y) | → | s(plus(x,y)) | (9) |
| times(x,y) | → | timesIter(x,y,0) | (10) |
| timesIter(x,y,z) | → | if(check(x),x,y,z,plus(z,y)) | (11) |
| p(s(x)) | → | x | (12) |
| p(0) | → | 0 | (13) |
| if(zero,x,y,z,u) | → | z | (14) |
| if(odd,x,y,z,u) | → | timesIter(p(x),y,u) | (15) |
| if(even,x,y,z,u) | → | plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z)))) | (16) |
| check#(s(s(s(x)))) | → | check#(s(x)) | (17) |
| half#(s(s(x))) | → | half#(x) | (18) |
| plus#(s(x),y) | → | plus#(x,y) | (19) |
| times#(x,y) | → | timesIter#(x,y,0) | (20) |
| timesIter#(x,y,z) | → | plus#(z,y) | (21) |
| timesIter#(x,y,z) | → | check#(x) | (22) |
| timesIter#(x,y,z) | → | if#(check(x),x,y,z,plus(z,y)) | (23) |
| if#(odd,x,y,z,u) | → | p#(x) | (24) |
| if#(odd,x,y,z,u) | → | timesIter#(p(x),y,u) | (25) |
| if#(even,x,y,z,u) | → | half#(s(z)) | (26) |
| if#(even,x,y,z,u) | → | timesIter#(half(x),y,half(s(z))) | (27) |
| if#(even,x,y,z,u) | → | half#(z) | (28) |
| if#(even,x,y,z,u) | → | half#(x) | (29) |
| if#(even,x,y,z,u) | → | timesIter#(half(x),y,half(z)) | (30) |
| if#(even,x,y,z,u) | → | plus#(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z)))) | (31) |
The dependency pairs are split into 4 components.
| if#(even,x,y,z,u) | → | timesIter#(half(x),y,half(s(z))) | (27) |
| timesIter#(x,y,z) | → | if#(check(x),x,y,z,plus(z,y)) | (23) |
| if#(odd,x,y,z,u) | → | timesIter#(p(x),y,u) | (25) |
| if#(even,x,y,z,u) | → | timesIter#(half(x),y,half(z)) | (30) |
| [odd] | = | 6 |
| [check(x1)] | = | 0 · x1 + -∞ |
| [s(x1)] | = | 1 · x1 + 0 |
| [timesIter#(x1, x2, x3)] | = | 0 · x1 + -∞ · x2 + -∞ · x3 + -16 |
| [if#(x1,...,x5)] | = | 0 · x1 + 0 · x2 + -∞ · x3 + -∞ · x4 + -∞ · x5 + -16 |
| [even] | = | 0 |
| [0] | = | 5 |
| [plus(x1, x2)] | = | -∞ · x1 + 0 · x2 + 0 |
| [p(x1)] | = | -1 · x1 + 5 |
| [half(x1)] | = | 0 · x1 + -∞ |
| [zero] | = | 2 |
| half(s(0)) | → | 0 | (6) |
| half(s(s(x))) | → | s(half(x)) | (7) |
| half(0) | → | 0 | (5) |
| check(0) | → | zero | (1) |
| check(s(0)) | → | odd | (2) |
| check(s(s(0))) | → | even | (3) |
| check(s(s(s(x)))) | → | check(s(x)) | (4) |
| p(s(x)) | → | x | (12) |
| p(0) | → | 0 | (13) |
| if#(odd,x,y,z,u) | → | timesIter#(p(x),y,u) | (25) |
| [odd] | = | 0 |
| [check(x1)] | = | 2 · x1 + 0 |
| [s(x1)] | = | 3 · x1 + 2 |
| [timesIter#(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 0 · x3 + 3/2 |
| [if#(x1,...,x5)] | = | 1/2 · x1 + 1 · x2 + 1 · x3 + 0 · x4 + 0 · x5 + 1 |
| [even] | = | 1 |
| [0] | = | 0 |
| [plus(x1, x2)] | = | 0 · x1 + 0 · x2 + 1/2 |
| [half(x1)] | = | 1/2 · x1 + 0 |
| [zero] | = | 0 |
| half(s(0)) | → | 0 | (6) |
| half(s(s(x))) | → | s(half(x)) | (7) |
| half(0) | → | 0 | (5) |
| check(0) | → | zero | (1) |
| check(s(0)) | → | odd | (2) |
| check(s(s(0))) | → | even | (3) |
| check(s(s(s(x)))) | → | check(s(x)) | (4) |
| timesIter#(x,y,z) | → | if#(check(x),x,y,z,plus(z,y)) | (23) |
The dependency pairs are split into 0 components.
| half#(s(s(x))) | → | half#(x) | (18) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| half#(s(s(x))) | → | half#(x) | (18) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| check#(s(s(s(x)))) | → | check#(s(x)) | (17) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| check#(s(s(s(x)))) | → | check#(s(x)) | (17) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| plus#(s(x),y) | → | plus#(x,y) | (19) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| plus#(s(x),y) | → | plus#(x,y) | (19) |
| 2 | ≥ | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.