The rewrite relation of the following TRS is considered.
| and(false,false) | → | false | (1) |
| and(true,false) | → | false | (2) |
| and(false,true) | → | false | (3) |
| and(true,true) | → | true | (4) |
| eq(nil,nil) | → | true | (5) |
| eq(cons(T,L),nil) | → | false | (6) |
| eq(nil,cons(T,L)) | → | false | (7) |
| eq(cons(T,L),cons(Tp,Lp)) | → | and(eq(T,Tp),eq(L,Lp)) | (8) |
| eq(var(L),var(Lp)) | → | eq(L,Lp) | (9) |
| eq(var(L),apply(T,S)) | → | false | (10) |
| eq(var(L),lambda(X,T)) | → | false | (11) |
| eq(apply(T,S),var(L)) | → | false | (12) |
| eq(apply(T,S),apply(Tp,Sp)) | → | and(eq(T,Tp),eq(S,Sp)) | (13) |
| eq(apply(T,S),lambda(X,Tp)) | → | false | (14) |
| eq(lambda(X,T),var(L)) | → | false | (15) |
| eq(lambda(X,T),apply(Tp,Sp)) | → | false | (16) |
| eq(lambda(X,T),lambda(Xp,Tp)) | → | and(eq(T,Tp),eq(X,Xp)) | (17) |
| if(true,var(K),var(L)) | → | var(K) | (18) |
| if(false,var(K),var(L)) | → | var(L) | (19) |
| ren(var(L),var(K),var(Lp)) | → | if(eq(L,Lp),var(K),var(Lp)) | (20) |
| ren(X,Y,apply(T,S)) | → | apply(ren(X,Y,T),ren(X,Y,S)) | (21) |
| 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))) | (22) |
| eq#(apply(T,S),apply(Tp,Sp)) | → | eq#(T,Tp) | (23) |
| ren#(var(L),var(K),var(Lp)) | → | eq#(L,Lp) | (24) |
| ren#(X,Y,apply(T,S)) | → | ren#(X,Y,S) | (25) |
| eq#(lambda(X,T),lambda(Xp,Tp)) | → | and#(eq(T,Tp),eq(X,Xp)) | (26) |
| eq#(lambda(X,T),lambda(Xp,Tp)) | → | eq#(X,Xp) | (27) |
| ren#(X,Y,apply(T,S)) | → | ren#(X,Y,T) | (28) |
| eq#(cons(T,L),cons(Tp,Lp)) | → | and#(eq(T,Tp),eq(L,Lp)) | (29) |
| ren#(X,Y,lambda(Z,T)) | → | ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)) | (30) |
| eq#(lambda(X,T),lambda(Xp,Tp)) | → | eq#(T,Tp) | (31) |
| ren#(var(L),var(K),var(Lp)) | → | if#(eq(L,Lp),var(K),var(Lp)) | (32) |
| eq#(cons(T,L),cons(Tp,Lp)) | → | eq#(L,Lp) | (33) |
| eq#(apply(T,S),apply(Tp,Sp)) | → | eq#(S,Sp) | (34) |
| eq#(apply(T,S),apply(Tp,Sp)) | → | and#(eq(T,Tp),eq(S,Sp)) | (35) |
| ren#(X,Y,lambda(Z,T)) | → | ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T) | (36) |
| eq#(cons(T,L),cons(Tp,Lp)) | → | eq#(T,Tp) | (37) |
| eq#(var(L),var(Lp)) | → | eq#(L,Lp) | (38) |
The dependency pairs are split into 2 components.
| ren#(X,Y,apply(T,S)) | → | ren#(X,Y,T) | (28) |
| ren#(X,Y,lambda(Z,T)) | → | ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T) | (36) |
| ren#(X,Y,apply(T,S)) | → | ren#(X,Y,S) | (25) |
| ren#(X,Y,lambda(Z,T)) | → | ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)) | (30) |
| [apply(x1, x2)] | = | x1 + x2 + 1 |
| [ren(x1, x2, x3)] | = | x3 + 0 |
| [and(x1, x2)] | = | x2 + 3 |
| [eq(x1, x2)] | = | x2 + 47562 |
| [lambda(x1, x2)] | = | x2 + 2 |
| [false] | = | 47568 |
| [true] | = | 47564 |
| [eq#(x1, x2)] | = | 0 |
| [if(x1, x2, x3)] | = | x3 + 0 |
| [nil] | = | 1 |
| [ren#(x1, x2, x3)] | = | x2 + x3 + 0 |
| [cons(x1, x2)] | = | x1 + x2 + 1 |
| [if#(x1, x2, x3)] | = | 0 |
| [var(x1)] | = | 1 |
| [and#(x1, x2)] | = | 0 |
| if(true,var(K),var(L)) | → | var(K) | (18) |
| ren(X,Y,apply(T,S)) | → | apply(ren(X,Y,T),ren(X,Y,S)) | (21) |
| if(false,var(K),var(L)) | → | var(L) | (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))) | (22) |
| ren(var(L),var(K),var(Lp)) | → | if(eq(L,Lp),var(K),var(Lp)) | (20) |
| ren#(X,Y,apply(T,S)) | → | ren#(X,Y,T) | (28) |
| ren#(X,Y,lambda(Z,T)) | → | ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T) | (36) |
| ren#(X,Y,apply(T,S)) | → | ren#(X,Y,S) | (25) |
| ren#(X,Y,lambda(Z,T)) | → | ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)) | (30) |
The dependency pairs are split into 0 components.
| eq#(var(L),var(Lp)) | → | eq#(L,Lp) | (38) |
| eq#(cons(T,L),cons(Tp,Lp)) | → | eq#(T,Tp) | (37) |
| eq#(apply(T,S),apply(Tp,Sp)) | → | eq#(S,Sp) | (34) |
| eq#(cons(T,L),cons(Tp,Lp)) | → | eq#(L,Lp) | (33) |
| eq#(lambda(X,T),lambda(Xp,Tp)) | → | eq#(X,Xp) | (27) |
| eq#(lambda(X,T),lambda(Xp,Tp)) | → | eq#(T,Tp) | (31) |
| eq#(apply(T,S),apply(Tp,Sp)) | → | eq#(T,Tp) | (23) |
| [apply(x1, x2)] | = | x1 + x2 + 1 |
| [ren(x1, x2, x3)] | = | x3 + 0 |
| [and(x1, x2)] | = | x2 + 2 |
| [eq(x1, x2)] | = | x2 + 35495 |
| [lambda(x1, x2)] | = | x1 + x2 + 1 |
| [false] | = | 35500 |
| [true] | = | 35497 |
| [eq#(x1, x2)] | = | x1 + x2 + 0 |
| [if(x1, x2, x3)] | = | x3 + 0 |
| [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 |
| if(false,var(K),var(L)) | → | var(L) | (19) |
| eq#(var(L),var(Lp)) | → | eq#(L,Lp) | (38) |
| eq#(cons(T,L),cons(Tp,Lp)) | → | eq#(T,Tp) | (37) |
| eq#(apply(T,S),apply(Tp,Sp)) | → | eq#(S,Sp) | (34) |
| eq#(cons(T,L),cons(Tp,Lp)) | → | eq#(L,Lp) | (33) |
| eq#(lambda(X,T),lambda(Xp,Tp)) | → | eq#(X,Xp) | (27) |
| eq#(lambda(X,T),lambda(Xp,Tp)) | → | eq#(T,Tp) | (31) |
| eq#(apply(T,S),apply(Tp,Sp)) | → | eq#(T,Tp) | (23) |
The dependency pairs are split into 0 components.