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