The rewrite relation of the following TRS is considered.
| if(true,x,y) | → | x | (1) |
| if(false,x,y) | → | y | (2) |
| eq(0,0) | → | true | (3) |
| eq(0,s(x)) | → | false | (4) |
| eq(s(x),0) | → | false | (5) |
| eq(s(x),s(y)) | → | eq(x,y) | (6) |
| app(nil,l) | → | l | (7) |
| app(cons(x,l1),l2) | → | cons(x,app(l1,l2)) | (8) |
| app(app(l1,l2),l3) | → | app(l1,app(l2,l3)) | (9) |
| mem(x,nil) | → | false | (10) |
| mem(x,cons(y,l)) | → | ifmem(eq(x,y),x,l) | (11) |
| ifmem(true,x,l) | → | true | (12) |
| ifmem(false,x,l) | → | mem(x,l) | (13) |
| inter(x,nil) | → | nil | (14) |
| inter(nil,x) | → | nil | (15) |
| inter(app(l1,l2),l3) | → | app(inter(l1,l3),inter(l2,l3)) | (16) |
| inter(l1,app(l2,l3)) | → | app(inter(l1,l2),inter(l1,l3)) | (17) |
| inter(cons(x,l1),l2) | → | ifinter(mem(x,l2),x,l1,l2) | (18) |
| inter(l1,cons(x,l2)) | → | ifinter(mem(x,l1),x,l2,l1) | (19) |
| ifinter(true,x,l1,l2) | → | cons(x,inter(l1,l2)) | (20) |
| ifinter(false,x,l1,l2) | → | inter(l1,l2) | (21) |
| eq#(s(x),s(y)) | → | eq#(x,y) | (22) |
| app#(cons(x,l1),l2) | → | app#(l1,l2) | (23) |
| app#(app(l1,l2),l3) | → | app#(l2,l3) | (24) |
| app#(app(l1,l2),l3) | → | app#(l1,app(l2,l3)) | (25) |
| mem#(x,cons(y,l)) | → | eq#(x,y) | (26) |
| mem#(x,cons(y,l)) | → | ifmem#(eq(x,y),x,l) | (27) |
| ifmem#(false,x,l) | → | mem#(x,l) | (28) |
| inter#(app(l1,l2),l3) | → | inter#(l2,l3) | (29) |
| inter#(app(l1,l2),l3) | → | inter#(l1,l3) | (30) |
| inter#(app(l1,l2),l3) | → | app#(inter(l1,l3),inter(l2,l3)) | (31) |
| inter#(l1,app(l2,l3)) | → | inter#(l1,l3) | (32) |
| inter#(l1,app(l2,l3)) | → | inter#(l1,l2) | (33) |
| inter#(l1,app(l2,l3)) | → | app#(inter(l1,l2),inter(l1,l3)) | (34) |
| inter#(cons(x,l1),l2) | → | mem#(x,l2) | (35) |
| inter#(cons(x,l1),l2) | → | ifinter#(mem(x,l2),x,l1,l2) | (36) |
| inter#(l1,cons(x,l2)) | → | mem#(x,l1) | (37) |
| inter#(l1,cons(x,l2)) | → | ifinter#(mem(x,l1),x,l2,l1) | (38) |
| ifinter#(true,x,l1,l2) | → | inter#(l1,l2) | (39) |
| ifinter#(false,x,l1,l2) | → | inter#(l1,l2) | (40) |
The dependency pairs are split into 4 components.
| ifinter#(false,x,l1,l2) | → | inter#(l1,l2) | (40) |
| inter#(app(l1,l2),l3) | → | inter#(l2,l3) | (29) |
| inter#(app(l1,l2),l3) | → | inter#(l1,l3) | (30) |
| inter#(l1,app(l2,l3)) | → | inter#(l1,l3) | (32) |
| inter#(l1,app(l2,l3)) | → | inter#(l1,l2) | (33) |
| inter#(cons(x,l1),l2) | → | ifinter#(mem(x,l2),x,l1,l2) | (36) |
| ifinter#(true,x,l1,l2) | → | inter#(l1,l2) | (39) |
| inter#(l1,cons(x,l2)) | → | ifinter#(mem(x,l1),x,l2,l1) | (38) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| ifinter#(false,x,l1,l2) | → | inter#(l1,l2) | (40) |
| 4 | ≥ | 2 | |
| 3 | ≥ | 1 | |
| inter#(app(l1,l2),l3) | → | inter#(l2,l3) | (29) |
| 2 | ≥ | 2 | |
| 1 | > | 1 | |
| inter#(app(l1,l2),l3) | → | inter#(l1,l3) | (30) |
| 2 | ≥ | 2 | |
| 1 | > | 1 | |
| inter#(l1,app(l2,l3)) | → | inter#(l1,l3) | (32) |
| 2 | > | 2 | |
| 1 | ≥ | 1 | |
| inter#(l1,app(l2,l3)) | → | inter#(l1,l2) | (33) |
| 2 | > | 2 | |
| 1 | ≥ | 1 | |
| inter#(cons(x,l1),l2) | → | ifinter#(mem(x,l2),x,l1,l2) | (36) |
| 2 | ≥ | 4 | |
| 1 | > | 3 | |
| 1 | > | 2 | |
| ifinter#(true,x,l1,l2) | → | inter#(l1,l2) | (39) |
| 4 | ≥ | 2 | |
| 3 | ≥ | 1 | |
| inter#(l1,cons(x,l2)) | → | ifinter#(mem(x,l1),x,l2,l1) | (38) |
| 2 | > | 3 | |
| 2 | > | 2 | |
| 1 | ≥ | 4 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| mem#(x,cons(y,l)) | → | ifmem#(eq(x,y),x,l) | (27) |
| ifmem#(false,x,l) | → | mem#(x,l) | (28) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| mem#(x,cons(y,l)) | → | ifmem#(eq(x,y),x,l) | (27) |
| 2 | > | 3 | |
| 1 | ≥ | 2 | |
| ifmem#(false,x,l) | → | mem#(x,l) | (28) |
| 3 | ≥ | 2 | |
| 2 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| eq#(s(x),s(y)) | → | eq#(x,y) | (22) |
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) | (22) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| app#(cons(x,l1),l2) | → | app#(l1,l2) | (23) |
| app#(app(l1,l2),l3) | → | app#(l2,l3) | (24) |
| app#(app(l1,l2),l3) | → | app#(l1,app(l2,l3)) | (25) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(cons(x,l1),l2) | → | app#(l1,l2) | (23) |
| 2 | ≥ | 2 | |
| 1 | > | 1 | |
| app#(app(l1,l2),l3) | → | app#(l2,l3) | (24) |
| 2 | ≥ | 2 | |
| 1 | > | 1 | |
| app#(app(l1,l2),l3) | → | app#(l1,app(l2,l3)) | (25) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.