The rewrite relation of the following TRS is considered.
app(not,app(not,x)) | → | x | (1) |
app(not,app(app(or,x),y)) | → | app(app(and,app(not,x)),app(not,y)) | (2) |
app(not,app(app(and,x),y)) | → | app(app(or,app(not,x)),app(not,y)) | (3) |
app(app(and,x),app(app(or,y),z)) | → | app(app(or,app(app(and,x),y)),app(app(and,x),z)) | (4) |
app(app(and,app(app(or,y),z)),x) | → | app(app(or,app(app(and,x),y)),app(app(and,x),z)) | (5) |
app(app(map,f),nil) | → | nil | (6) |
app(app(map,f),app(app(cons,x),xs)) | → | app(app(cons,app(f,x)),app(app(map,f),xs)) | (7) |
app(app(filter,f),nil) | → | nil | (8) |
app(app(filter,f),app(app(cons,x),xs)) | → | app(app(app(app(filter2,app(f,x)),f),x),xs) | (9) |
app(app(app(app(filter2,true),f),x),xs) | → | app(app(cons,x),app(app(filter,f),xs)) | (10) |
app(app(app(app(filter2,false),f),x),xs) | → | app(app(filter,f),xs) | (11) |
app#(not,app(app(or,x),y)) | → | app#(not,y) | (12) |
app#(not,app(app(or,x),y)) | → | app#(not,x) | (13) |
app#(not,app(app(or,x),y)) | → | app#(and,app(not,x)) | (14) |
app#(not,app(app(or,x),y)) | → | app#(app(and,app(not,x)),app(not,y)) | (15) |
app#(not,app(app(and,x),y)) | → | app#(not,y) | (16) |
app#(not,app(app(and,x),y)) | → | app#(not,x) | (17) |
app#(not,app(app(and,x),y)) | → | app#(or,app(not,x)) | (18) |
app#(not,app(app(and,x),y)) | → | app#(app(or,app(not,x)),app(not,y)) | (19) |
app#(app(and,x),app(app(or,y),z)) | → | app#(app(and,x),z) | (20) |
app#(app(and,x),app(app(or,y),z)) | → | app#(app(and,x),y) | (21) |
app#(app(and,x),app(app(or,y),z)) | → | app#(or,app(app(and,x),y)) | (22) |
app#(app(and,x),app(app(or,y),z)) | → | app#(app(or,app(app(and,x),y)),app(app(and,x),z)) | (23) |
app#(app(and,app(app(or,y),z)),x) | → | app#(app(and,x),z) | (24) |
app#(app(and,app(app(or,y),z)),x) | → | app#(and,x) | (25) |
app#(app(and,app(app(or,y),z)),x) | → | app#(app(and,x),y) | (26) |
app#(app(and,app(app(or,y),z)),x) | → | app#(or,app(app(and,x),y)) | (27) |
app#(app(and,app(app(or,y),z)),x) | → | app#(app(or,app(app(and,x),y)),app(app(and,x),z)) | (28) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (29) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (30) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(cons,app(f,x)) | (31) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(cons,app(f,x)),app(app(map,f),xs)) | (32) |
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(f,x) | (33) |
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(filter2,app(f,x)) | (34) |
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(app(filter2,app(f,x)),f) | (35) |
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(app(app(filter2,app(f,x)),f),x) | (36) |
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(f,x)),f),x),xs) | (37) |
app#(app(app(app(filter2,true),f),x),xs) | → | app#(filter,f) | (38) |
app#(app(app(app(filter2,true),f),x),xs) | → | app#(app(filter,f),xs) | (39) |
app#(app(app(app(filter2,true),f),x),xs) | → | app#(cons,x) | (40) |
app#(app(app(app(filter2,true),f),x),xs) | → | app#(app(cons,x),app(app(filter,f),xs)) | (41) |
app#(app(app(app(filter2,false),f),x),xs) | → | app#(filter,f) | (42) |
app#(app(app(app(filter2,false),f),x),xs) | → | app#(app(filter,f),xs) | (43) |
The dependency pairs are split into 3 components.
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(f,x)),f),x),xs) | (37) |
app#(app(app(app(filter2,false),f),x),xs) | → | app#(app(filter,f),xs) | (43) |
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(f,x) | (33) |
app#(app(app(app(filter2,true),f),x),xs) | → | app#(app(filter,f),xs) | (39) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (30) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (29) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(f,x)),f),x),xs) | (37) |
2 | > | 2 | |
app#(app(app(app(filter2,false),f),x),xs) | → | app#(app(filter,f),xs) | (43) |
2 | ≥ | 2 | |
app#(app(filter,f),app(app(cons,x),xs)) | → | app#(f,x) | (33) |
2 | > | 2 | |
1 | > | 1 | |
app#(app(app(app(filter2,true),f),x),xs) | → | app#(app(filter,f),xs) | (39) |
2 | ≥ | 2 | |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (30) |
2 | > | 2 | |
1 | > | 1 | |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (29) |
2 | > | 2 | |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
app#(not,app(app(and,x),y)) | → | app#(not,x) | (17) |
app#(not,app(app(and,x),y)) | → | app#(not,y) | (16) |
app#(not,app(app(or,x),y)) | → | app#(not,x) | (13) |
app#(not,app(app(or,x),y)) | → | app#(not,y) | (12) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
app#(not,app(app(and,x),y)) | → | app#(not,x) | (17) |
2 | > | 2 | |
1 | ≥ | 1 | |
app#(not,app(app(and,x),y)) | → | app#(not,y) | (16) |
2 | > | 2 | |
1 | ≥ | 1 | |
app#(not,app(app(or,x),y)) | → | app#(not,x) | (13) |
2 | > | 2 | |
1 | ≥ | 1 | |
app#(not,app(app(or,x),y)) | → | app#(not,y) | (12) |
2 | > | 2 | |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
app#(app(and,app(app(or,y),z)),x) | → | app#(app(and,x),y) | (26) |
app#(app(and,app(app(or,y),z)),x) | → | app#(app(and,x),z) | (24) |
app#(app(and,x),app(app(or,y),z)) | → | app#(app(and,x),y) | (21) |
app#(app(and,x),app(app(or,y),z)) | → | app#(app(and,x),z) | (20) |
[app(x1, x2)] | = | -1 · x1 + 2 · x2 + -16 |
[and] | = | 0 |
[app#(x1, x2)] | = | 0 · x1 + 3 · x2 + -16 |
[or] | = | 1 |
app#(app(and,app(app(or,y),z)),x) | → | app#(app(and,x),z) | (24) |
[app(x1, x2)] | = | 1 · x1 + 1 · x2 + 0 |
[and] | = | 2 |
[app#(x1, x2)] | = | 1 · x1 + 3 · x2 + 0 |
[or] | = | 1 |
app#(app(and,app(app(or,y),z)),x) | → | app#(app(and,x),y) | (26) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
app#(app(and,x),app(app(or,y),z)) | → | app#(app(and,x),y) | (21) |
2 | > | 2 | |
1 | ≥ | 1 | |
app#(app(and,x),app(app(or,y),z)) | → | app#(app(and,x),z) | (20) |
2 | > | 2 | |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.