The rewrite relation of the following TRS is considered.
| minus(x,0) | → | x | (1) |
| minus(s(x),s(y)) | → | minus(x,y) | (2) |
| quot(0,s(y)) | → | 0 | (3) |
| quot(s(x),s(y)) | → | s(quot(minus(x,y),s(y))) | (4) |
| minus(minus(x,y),z) | → | minus(x,plus(y,z)) | (5) |
| plus(s(x),s(y)) | → | s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) | (6) |
| plus(s(x),x) | → | plus(if(gt(x,x),id(x),id(x)),s(x)) | (7) |
| plus(zero,y) | → | y | (8) |
| plus(id(x),s(y)) | → | s(plus(x,if(gt(s(y),y),y,s(y)))) | (9) |
| id(x) | → | x | (10) |
| if(true,x,y) | → | x | (11) |
| if(false,x,y) | → | y | (12) |
| not(x) | → | if(x,false,true) | (13) |
| gt(s(x),zero) | → | true | (14) |
| gt(zero,y) | → | false | (15) |
| gt(s(x),s(y)) | → | gt(x,y) | (16) |
| minus#(s(x),s(y)) | → | minus#(x,y) | (17) |
| quot#(s(x),s(y)) | → | minus#(x,y) | (18) |
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (19) |
| minus#(minus(x,y),z) | → | plus#(y,z) | (20) |
| minus#(minus(x,y),z) | → | minus#(x,plus(y,z)) | (21) |
| plus#(s(x),s(y)) | → | id#(y) | (22) |
| plus#(s(x),s(y)) | → | id#(x) | (23) |
| plus#(s(x),s(y)) | → | not#(gt(x,y)) | (24) |
| plus#(s(x),s(y)) | → | if#(not(gt(x,y)),id(x),id(y)) | (25) |
| plus#(s(x),s(y)) | → | gt#(x,y) | (26) |
| plus#(s(x),s(y)) | → | if#(gt(x,y),x,y) | (27) |
| plus#(s(x),s(y)) | → | plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) | (28) |
| plus#(s(x),x) | → | id#(x) | (29) |
| plus#(s(x),x) | → | gt#(x,x) | (30) |
| plus#(s(x),x) | → | if#(gt(x,x),id(x),id(x)) | (31) |
| plus#(s(x),x) | → | plus#(if(gt(x,x),id(x),id(x)),s(x)) | (32) |
| plus#(id(x),s(y)) | → | gt#(s(y),y) | (33) |
| plus#(id(x),s(y)) | → | if#(gt(s(y),y),y,s(y)) | (34) |
| plus#(id(x),s(y)) | → | plus#(x,if(gt(s(y),y),y,s(y))) | (35) |
| not#(x) | → | if#(x,false,true) | (36) |
| gt#(s(x),s(y)) | → | gt#(x,y) | (37) |
The dependency pairs are split into 4 components.
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (19) |
| π(quot#) | = | { 1 } |
| π(minus) | = | { 1 } |
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (19) |
There are no pairs anymore.
| minus#(s(x),s(y)) | → | minus#(x,y) | (17) |
| minus#(minus(x,y),z) | → | minus#(x,plus(y,z)) | (21) |
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) | (17) |
| 2 | > | 2 | |
| 1 | > | 1 | |
| minus#(minus(x,y),z) | → | minus#(x,plus(y,z)) | (21) |
| 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))) | (35) |
| plus#(s(x),s(y)) | → | plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) | (28) |
| plus#(s(x),x) | → | plus#(if(gt(x,x),id(x),id(x)),s(x)) | (32) |
| [id(x1)] | = | 0 · x1 + 0 |
| [gt(x1, x2)] | = | -8 · x1 + 0 · x2 + 0 |
| [true] | = | 0 |
| [not(x1)] | = | 0 · x1 + 0 |
| [plus#(x1, x2)] | = | 0 · x1 + 0 · x2 + 0 |
| [false] | = | 0 |
| [zero] | = | 1 |
| [if(x1, x2, x3)] | = | 0 · x1 + 0 · x2 + 0 · x3 + 0 |
| [s(x1)] | = | 1 · x1 + 4 |
| gt(s(x),zero) | → | true | (14) |
| gt(s(x),s(y)) | → | gt(x,y) | (16) |
| gt(zero,y) | → | false | (15) |
| if(true,x,y) | → | x | (11) |
| if(false,x,y) | → | y | (12) |
| id(x) | → | x | (10) |
| not(x) | → | if(x,false,true) | (13) |
| plus#(s(x),s(y)) | → | plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) | (28) |
| [id(x1)] | = | 0 · x1 + -∞ |
| [gt(x1, x2)] | = | 0 · x1 + 6 · x2 + 0 |
| [true] | = | 1 |
| [plus#(x1, x2)] | = | 2 · x1 + 0 · x2 + 0 |
| [false] | = | 2 |
| [zero] | = | 0 |
| [if(x1, x2, x3)] | = | -∞ · x1 + 0 · x2 + 0 · x3 + -∞ |
| [s(x1)] | = | 1 · x1 + 0 |
| if(true,x,y) | → | x | (11) |
| if(false,x,y) | → | y | (12) |
| id(x) | → | x | (10) |
| plus#(s(x),x) | → | plus#(if(gt(x,x),id(x),id(x)),s(x)) | (32) |
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))) | (35) |
| 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) | (37) |
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) | (37) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.