The rewrite relation of the following TRS is considered.
| not(not(x)) | → | x | (1) |
| not(or(x,y)) | → | and(not(x),not(y)) | (2) |
| not(and(x,y)) | → | or(not(x),not(y)) | (3) |
| and(x,or(y,z)) | → | or(and(x,y),and(x,z)) | (4) |
| and(or(y,z),x) | → | or(and(x,y),and(x,z)) | (5) |
| not#(or(x,y)) | → | not#(y) | (6) |
| not#(or(x,y)) | → | not#(x) | (7) |
| not#(or(x,y)) | → | and#(not(x),not(y)) | (8) |
| not#(and(x,y)) | → | not#(y) | (9) |
| not#(and(x,y)) | → | not#(x) | (10) |
| and#(x,or(y,z)) | → | and#(x,z) | (11) |
| and#(x,or(y,z)) | → | and#(x,y) | (12) |
| and#(or(y,z),x) | → | and#(x,z) | (13) |
| and#(or(y,z),x) | → | and#(x,y) | (14) |
The dependency pairs are split into 2 components.
| not#(and(x,y)) | → | not#(y) | (9) |
| not#(or(x,y)) | → | not#(y) | (6) |
| not#(or(x,y)) | → | not#(x) | (7) |
| not#(and(x,y)) | → | not#(x) | (10) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| not#(and(x,y)) | → | not#(y) | (9) |
| 1 | > | 1 | |
| not#(or(x,y)) | → | not#(y) | (6) |
| 1 | > | 1 | |
| not#(or(x,y)) | → | not#(x) | (7) |
| 1 | > | 1 | |
| not#(and(x,y)) | → | not#(x) | (10) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| and#(or(y,z),x) | → | and#(x,z) | (13) |
| and#(x,or(y,z)) | → | and#(x,z) | (11) |
| and#(x,or(y,z)) | → | and#(x,y) | (12) |
| and#(or(y,z),x) | → | and#(x,y) | (14) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| and#(or(y,z),x) | → | and#(x,z) | (13) |
| 2 | ≥ | 1 | |
| 1 | > | 2 | |
| and#(x,or(y,z)) | → | and#(x,z) | (11) |
| 2 | > | 2 | |
| 1 | ≥ | 1 | |
| and#(x,or(y,z)) | → | and#(x,y) | (12) |
| 2 | > | 2 | |
| 1 | ≥ | 1 | |
| and#(or(y,z),x) | → | and#(x,y) | (14) |
| 2 | ≥ | 1 | |
| 1 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.