The rewrite relation of the following TRS is considered.
| and(true,y) | → | y | (1) |
| and(false,y) | → | false | (2) |
| eq(nil,nil) | → | true | (3) |
| eq(cons(t,l),nil) | → | false | (4) |
| eq(nil,cons(t,l)) | → | false | (5) |
| eq(cons(t,l),cons(t',l')) | → | and(eq(t,t'),eq(l,l')) | (6) |
| eq(var(l),var(l')) | → | eq(l,l') | (7) |
| eq(var(l),apply(t,s)) | → | false | (8) |
| eq(var(l),lambda(x,t)) | → | false | (9) |
| eq(apply(t,s),var(l)) | → | false | (10) |
| eq(apply(t,s),apply(t',s')) | → | and(eq(t,t'),eq(s,s')) | (11) |
| eq(apply(t,s),lambda(x,t)) | → | false | (12) |
| eq(lambda(x,t),var(l)) | → | false | (13) |
| eq(lambda(x,t),apply(t,s)) | → | false | (14) |
| eq(lambda(x,t),lambda(x',t')) | → | and(eq(x,x'),eq(t,t')) | (15) |
| if(true,var(k),var(l')) | → | var(k) | (16) |
| if(false,var(k),var(l')) | → | var(l') | (17) |
| ren(var(l),var(k),var(l')) | → | if(eq(l,l'),var(k),var(l')) | (18) |
| ren(x,y,apply(t,s)) | → | apply(ren(x,y,t),ren(x,y,s)) | (19) |
| ren(x,y,lambda(z,t)) | → | lambda(var(cons(x,cons(y,cons(lambda(z,t),nil)))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t))) | (20) |
| eq#(cons(t,l),cons(t',l')) | → | eq#(t,t') | (21) |
| eq#(apply(t,s),apply(t',s')) | → | eq#(s,s') | (22) |
| eq#(lambda(x,t),lambda(x',t')) | → | eq#(x,x') | (23) |
| eq#(var(l),var(l')) | → | eq#(l,l') | (24) |
| ren#(x,y,apply(t,s)) | → | ren#(x,y,s) | (25) |
| eq#(lambda(x,t),lambda(x',t')) | → | and#(eq(x,x'),eq(t,t')) | (26) |
| eq#(lambda(x,t),lambda(x',t')) | → | eq#(t,t') | (27) |
| ren#(x,y,lambda(z,t)) | → | ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)) | (28) |
| ren#(x,y,apply(t,s)) | → | ren#(x,y,t) | (29) |
| eq#(apply(t,s),apply(t',s')) | → | eq#(t,t') | (30) |
| ren#(var(l),var(k),var(l')) | → | eq#(l,l') | (31) |
| eq#(cons(t,l),cons(t',l')) | → | eq#(l,l') | (32) |
| eq#(cons(t,l),cons(t',l')) | → | and#(eq(t,t'),eq(l,l')) | (33) |
| ren#(x,y,lambda(z,t)) | → | ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t) | (34) |
| ren#(var(l),var(k),var(l')) | → | if#(eq(l,l'),var(k),var(l')) | (35) |
| eq#(apply(t,s),apply(t',s')) | → | and#(eq(t,t'),eq(s,s')) | (36) |
The dependency pairs are split into 2 components.
| ren#(x,y,lambda(z,t)) | → | ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t) | (34) |
| ren#(x,y,apply(t,s)) | → | ren#(x,y,s) | (25) |
| ren#(x,y,apply(t,s)) | → | ren#(x,y,t) | (29) |
| ren#(x,y,lambda(z,t)) | → | ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)) | (28) |
| [apply(x1, x2)] | = | x1 + x2 + 1 |
| [ren(x1, x2, x3)] | = | x3 + 0 |
| [and(x1, x2)] | = | x1 + x2 + 2 |
| [eq(x1, x2)] | = | x1 + x2 + 3 |
| [lambda(x1, x2)] | = | x1 + x2 + 2 |
| [false] | = | 7 |
| [true] | = | 6 |
| [eq#(x1, x2)] | = | 0 |
| [if(x1, x2, x3)] | = | 0 |
| [nil] | = | 1 |
| [ren#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
| [cons(x1, x2)] | = | 1 |
| [if#(x1, x2, x3)] | = | 0 |
| [var(x1)] | = | 0 |
| [and#(x1, x2)] | = | 0 |
| ren(var(l),var(k),var(l')) | → | if(eq(l,l'),var(k),var(l')) | (18) |
| if(true,var(k),var(l')) | → | var(k) | (16) |
| ren(x,y,apply(t,s)) | → | apply(ren(x,y,t),ren(x,y,s)) | (19) |
| if(false,var(k),var(l')) | → | var(l') | (17) |
| ren(x,y,lambda(z,t)) | → | lambda(var(cons(x,cons(y,cons(lambda(z,t),nil)))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t))) | (20) |
| ren#(x,y,lambda(z,t)) | → | ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t) | (34) |
| ren#(x,y,apply(t,s)) | → | ren#(x,y,s) | (25) |
| ren#(x,y,apply(t,s)) | → | ren#(x,y,t) | (29) |
| ren#(x,y,lambda(z,t)) | → | ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)) | (28) |
The dependency pairs are split into 0 components.
| eq#(lambda(x,t),lambda(x',t')) | → | eq#(t,t') | (27) |
| eq#(cons(t,l),cons(t',l')) | → | eq#(l,l') | (32) |
| eq#(var(l),var(l')) | → | eq#(l,l') | (24) |
| eq#(lambda(x,t),lambda(x',t')) | → | eq#(x,x') | (23) |
| eq#(apply(t,s),apply(t',s')) | → | eq#(s,s') | (22) |
| eq#(apply(t,s),apply(t',s')) | → | eq#(t,t') | (30) |
| eq#(cons(t,l),cons(t',l')) | → | eq#(t,t') | (21) |
| [apply(x1, x2)] | = | x1 + x2 + 1 |
| [ren(x1, x2, x3)] | = | x1 + x2 + 0 |
| [and(x1, x2)] | = | x1 + x2 + 2 |
| [eq(x1, x2)] | = | x1 + x2 + 1 |
| [lambda(x1, x2)] | = | x1 + x2 + 1 |
| [false] | = | 4 |
| [true] | = | 4 |
| [eq#(x1, x2)] | = | x1 + 0 |
| [if(x1, x2, x3)] | = | 1 |
| [nil] | = | 1 |
| [ren#(x1, x2, x3)] | = | 0 |
| [cons(x1, x2)] | = | x1 + x2 + 1 |
| [if#(x1, x2, x3)] | = | 0 |
| [var(x1)] | = | x1 + 1 |
| [and#(x1, x2)] | = | 0 |
| eq#(lambda(x,t),lambda(x',t')) | → | eq#(t,t') | (27) |
| eq#(cons(t,l),cons(t',l')) | → | eq#(l,l') | (32) |
| eq#(var(l),var(l')) | → | eq#(l,l') | (24) |
| eq#(lambda(x,t),lambda(x',t')) | → | eq#(x,x') | (23) |
| eq#(apply(t,s),apply(t',s')) | → | eq#(s,s') | (22) |
| eq#(apply(t,s),apply(t',s')) | → | eq#(t,t') | (30) |
| eq#(cons(t,l),cons(t',l')) | → | eq#(t,t') | (21) |
The dependency pairs are split into 0 components.