The rewrite relation of the following TRS is considered.
| p(0) | → | 0 | (1) |
| p(s(x)) | → | x | (2) |
| plus(x,0) | → | x | (3) |
| plus(0,y) | → | y | (4) |
| plus(s(x),y) | → | s(plus(x,y)) | (5) |
| plus(s(x),y) | → | s(plus(p(s(x)),y)) | (6) |
| plus(x,s(y)) | → | s(plus(x,p(s(y)))) | (7) |
| times(0,y) | → | 0 | (8) |
| times(s(0),y) | → | y | (9) |
| times(s(x),y) | → | plus(y,times(x,y)) | (10) |
| div(0,y) | → | 0 | (11) |
| div(x,y) | → | quot(x,y,y) | (12) |
| quot(zero(y),s(y),z) | → | 0 | (13) |
| quot(s(x),s(y),z) | → | quot(x,y,z) | (14) |
| quot(x,0,s(z)) | → | s(div(x,s(z))) | (15) |
| div(div(x,y),z) | → | div(x,times(zero(y),z)) | (16) |
| eq(0,0) | → | true | (17) |
| eq(s(x),0) | → | false | (18) |
| eq(0,s(y)) | → | false | (19) |
| eq(s(x),s(y)) | → | eq(x,y) | (20) |
| divides(y,x) | → | eq(x,times(div(x,y),y)) | (21) |
| prime(s(s(x))) | → | pr(s(s(x)),s(x)) | (22) |
| pr(x,s(0)) | → | true | (23) |
| pr(x,s(s(y))) | → | if(divides(s(s(y)),x),x,s(y)) | (24) |
| if(true,x,y) | → | false | (25) |
| if(false,x,y) | → | pr(x,y) | (26) |
| zero(div(x,x)) | → | x | (27) |
| zero(divides(x,x)) | → | x | (28) |
| zero(times(x,x)) | → | x | (29) |
| zero(quot(x,x,x)) | → | x | (30) |
| zero(s(x)) | → | if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0)))) | (31) |
| plus#(s(x),y) | → | plus#(x,y) | (32) |
| plus#(s(x),y) | → | p#(s(x)) | (33) |
| plus#(s(x),y) | → | plus#(p(s(x)),y) | (34) |
| plus#(x,s(y)) | → | p#(s(y)) | (35) |
| plus#(x,s(y)) | → | plus#(x,p(s(y))) | (36) |
| times#(s(x),y) | → | times#(x,y) | (37) |
| times#(s(x),y) | → | plus#(y,times(x,y)) | (38) |
| div#(x,y) | → | quot#(x,y,y) | (39) |
| quot#(s(x),s(y),z) | → | quot#(x,y,z) | (40) |
| quot#(x,0,s(z)) | → | div#(x,s(z)) | (41) |
| div#(div(x,y),z) | → | zero#(y) | (42) |
| div#(div(x,y),z) | → | times#(zero(y),z) | (43) |
| div#(div(x,y),z) | → | div#(x,times(zero(y),z)) | (44) |
| eq#(s(x),s(y)) | → | eq#(x,y) | (45) |
| divides#(y,x) | → | div#(x,y) | (46) |
| divides#(y,x) | → | times#(div(x,y),y) | (47) |
| divides#(y,x) | → | eq#(x,times(div(x,y),y)) | (48) |
| prime#(s(s(x))) | → | pr#(s(s(x)),s(x)) | (49) |
| pr#(x,s(s(y))) | → | divides#(s(s(y)),x) | (50) |
| pr#(x,s(s(y))) | → | if#(divides(s(s(y)),x),x,s(y)) | (51) |
| if#(false,x,y) | → | pr#(x,y) | (52) |
| zero#(s(x)) | → | plus#(0,zero(0)) | (53) |
| zero#(s(x)) | → | zero#(0) | (54) |
| zero#(s(x)) | → | plus#(zero(0),0) | (55) |
| zero#(s(x)) | → | eq#(x,s(0)) | (56) |
| zero#(s(x)) | → | if#(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0)))) | (57) |
The dependency pairs are split into 4 components.
| if#(false,x,y) | → | pr#(x,y) | (52) |
| pr#(x,s(s(y))) | → | if#(divides(s(s(y)),x),x,s(y)) | (51) |
| pr#(x,s(s(y))) | → | divides#(s(s(y)),x) | (50) |
| divides#(y,x) | → | div#(x,y) | (46) |
| div#(div(x,y),z) | → | div#(x,times(zero(y),z)) | (44) |
| div#(div(x,y),z) | → | zero#(y) | (42) |
| zero#(s(x)) | → | if#(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0)))) | (57) |
| div#(x,y) | → | quot#(x,y,y) | (39) |
| quot#(x,0,s(z)) | → | div#(x,s(z)) | (41) |
| quot#(s(x),s(y),z) | → | quot#(x,y,z) | (40) |
| [div#(x1, x2)] | = | 4 · x1 + 2 · x2 + -∞ |
| [times(x1, x2)] | = | 4 · x1 + 0 · x2 + 0 |
| [eq(x1, x2)] | = | 0 · x1 + -∞ · x2 + 0 |
| [p(x1)] | = | 0 · x1 + 0 |
| [plus(x1, x2)] | = | 0 · x1 + 0 · x2 + 0 |
| [quot#(x1, x2, x3)] | = | 4 · x1 + 0 · x2 + 2 · x3 + -∞ |
| [divides#(x1, x2)] | = | 3 · x1 + 5 · x2 + 0 |
| [div(x1, x2)] | = | 0 · x1 + 2 · x2 + 3 |
| [false] | = | 0 |
| [0] | = | 0 |
| [zero(x1)] | = | 0 · x1 + 1 |
| [zero#(x1)] | = | 4 · x1 + 7 |
| [if#(x1, x2, x3)] | = | 0 · x1 + 5 · x2 + 6 · x3 + 0 |
| [if(x1, x2, x3)] | = | -∞ · x1 + 0 · x2 + -∞ · x3 + 0 |
| [pr#(x1, x2)] | = | 5 · x1 + 6 · x2 + 0 |
| [divides(x1, x2)] | = | 3 · x1 + 0 · x2 + 0 |
| [true] | = | 0 |
| [pr(x1, x2)] | = | 0 · x1 + -∞ · x2 + 0 |
| [quot(x1, x2, x3)] | = | -∞ · x1 + 4 · x2 + 6 · x3 + -∞ |
| [s(x1)] | = | 0 · x1 + -∞ |
| divides(y,x) | → | eq(x,times(div(x,y),y)) | (21) |
| eq(0,0) | → | true | (17) |
| eq(s(x),0) | → | false | (18) |
| eq(0,s(y)) | → | false | (19) |
| eq(s(x),s(y)) | → | eq(x,y) | (20) |
| zero(div(x,x)) | → | x | (27) |
| zero(divides(x,x)) | → | x | (28) |
| zero(times(x,x)) | → | x | (29) |
| zero(quot(x,x,x)) | → | x | (30) |
| zero(s(x)) | → | if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0)))) | (31) |
| if(true,x,y) | → | false | (25) |
| if(false,x,y) | → | pr(x,y) | (26) |
| plus(0,y) | → | y | (4) |
| plus(x,0) | → | x | (3) |
| pr(x,s(0)) | → | true | (23) |
| pr(x,s(s(y))) | → | if(divides(s(s(y)),x),x,s(y)) | (24) |
| times(0,y) | → | 0 | (8) |
| times(s(0),y) | → | y | (9) |
| times(s(x),y) | → | plus(y,times(x,y)) | (10) |
| plus(s(x),y) | → | s(plus(x,y)) | (5) |
| plus(s(x),y) | → | s(plus(p(s(x)),y)) | (6) |
| plus(x,s(y)) | → | s(plus(x,p(s(y)))) | (7) |
| p(s(x)) | → | x | (2) |
| divides#(y,x) | → | div#(x,y) | (46) |
The dependency pairs are split into 2 components.
| quot#(s(x),s(y),z) | → | quot#(x,y,z) | (40) |
| quot#(x,0,s(z)) | → | div#(x,s(z)) | (41) |
| div#(div(x,y),z) | → | div#(x,times(zero(y),z)) | (44) |
| div#(x,y) | → | quot#(x,y,y) | (39) |
| π(quot#) | = | 1 |
| π(div#) | = | 1 |
| quot#(s(x),s(y),z) | → | quot#(x,y,z) | (40) |
| div#(div(x,y),z) | → | div#(x,times(zero(y),z)) | (44) |
| [div#(x1, x2)] | = | -∞ · x1 + 0 · x2 + 0 |
| [quot#(x1, x2, x3)] | = | -∞ · x1 + 0 · x2 + 0 · x3 + 0 |
| [0] | = | 1 |
| [s(x1)] | = | -∞ · x1 + 0 |
| quot#(x,0,s(z)) | → | div#(x,s(z)) | (41) |
The dependency pairs are split into 0 components.
| if#(false,x,y) | → | pr#(x,y) | (52) |
| pr#(x,s(s(y))) | → | if#(divides(s(s(y)),x),x,s(y)) | (51) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| if#(false,x,y) | → | pr#(x,y) | (52) |
| 3 | ≥ | 2 | |
| 2 | ≥ | 1 | |
| pr#(x,s(s(y))) | → | if#(divides(s(s(y)),x),x,s(y)) | (51) |
| 2 | > | 3 | |
| 1 | ≥ | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| times#(s(x),y) | → | times#(x,y) | (37) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| times#(s(x),y) | → | times#(x,y) | (37) |
| 2 | ≥ | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| plus#(x,s(y)) | → | plus#(x,p(s(y))) | (36) |
| plus#(s(x),y) | → | plus#(p(s(x)),y) | (34) |
| plus#(s(x),y) | → | plus#(x,y) | (32) |
| π(plus#) | = | { 1 } |
| π(p) | = | { 1 } |
| plus#(s(x),y) | → | plus#(x,y) | (32) |
| [p(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| [plus#(x1, x2)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| [s(x1)] | = |
|
| p(s(x)) | → | x | (2) |
| plus#(s(x),y) | → | plus#(p(s(x)),y) | (34) |
| [p(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| [plus#(x1, x2)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| [s(x1)] | = |
|
| p(s(x)) | → | x | (2) |
| plus#(x,s(y)) | → | plus#(x,p(s(y))) | (36) |
There are no pairs anymore.
| eq#(s(x),s(y)) | → | eq#(x,y) | (45) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| eq#(s(x),s(y)) | → | eq#(x,y) | (45) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.