YES Problem: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Proof: DP Processor: DPs: eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp)) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) TDG Processor: DPs: eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp)) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) graph: ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) -> ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) -> ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) -> ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp)) ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) -> ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) -> ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) -> ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) -> ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp)) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) -> ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) -> ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) -> ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) -> ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp)) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) -> ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) -> ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) -> ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) -> ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) -> ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp)) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) -> ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(var(L),var(Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp)) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp)) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp)) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) SCC Processor: #sccs: 2 #rules: 11 #arcs: 104/256 DPs: ren#(X,Y,lambda(Z,T)) -> ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Arctic Interpretation Processor: dimension: 1 usable rules: if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) interpretation: [ren#](x0, x1, x2) = -16x0 + -4x1 + 5x2 + -8, [ren](x0, x1, x2) = x2, [if](x0, x1, x2) = -4x1 + x2, [lambda](x0, x1) = -5x0 + 2x1 + -5, [apply](x0, x1) = x0 + 2x1 + 0, [var](x0) = 0, [cons](x0, x1) = x0 + x1 + -13, [eq](x0, x1) = 5x0 + 5x1 + 0, [nil] = 1, [true] = 5, [and](x0, x1) = -5x0 + 0, [false] = 0 orientation: ren#(X,Y,lambda(Z,T)) = 7T + -16X + -4Y + Z + 0 >= 5T + -16Z + -4 = ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T) ren#(X,Y,apply(T,S)) = 7S + 5T + -16X + -4Y + 5 >= 5S + -16X + -4Y + -8 = ren#(X,Y,S) ren#(X,Y,apply(T,S)) = 7S + 5T + -16X + -4Y + 5 >= 5T + -16X + -4Y + -8 = ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) = 7T + -16X + -4Y + Z + 0 >= 5T + -16X + -4Y + -8 = ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) and(false(),false()) = 0 >= 0 = false() and(true(),false()) = 0 >= 0 = false() and(false(),true()) = 0 >= 0 = false() and(true(),true()) = 0 >= 5 = true() eq(nil(),nil()) = 6 >= 5 = true() eq(cons(T,L),nil()) = 5L + 5T + 6 >= 0 = false() eq(nil(),cons(T,L)) = 5L + 5T + 6 >= 0 = false() eq(cons(T,L),cons(Tp,Lp)) = 5L + 5Lp + 5T + 5Tp + 0 >= T + Tp + 0 = and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) = 5 >= 5L + 5Lp + 0 = eq(L,Lp) eq(var(L),apply(T,S)) = 7S + 5T + 5 >= 0 = false() eq(var(L),lambda(X,T)) = 7T + X + 5 >= 0 = false() eq(apply(T,S),var(L)) = 7S + 5T + 5 >= 0 = false() eq(apply(T,S),apply(Tp,Sp)) = 7S + 7Sp + 5T + 5Tp + 5 >= T + Tp + 0 = and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) = 7S + 5T + 7Tp + X + 5 >= 0 = false() eq(lambda(X,T),var(L)) = 7T + X + 5 >= 0 = false() eq(lambda(X,T),apply(Tp,Sp)) = 7Sp + 7T + 5Tp + X + 5 >= 0 = false() eq(lambda(X,T),lambda(Xp,Tp)) = 7T + 7Tp + X + Xp + 0 >= T + Tp + 0 = and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) = 0 >= 0 = var(K) if(false(),var(K),var(L)) = 0 >= 0 = var(L) ren(var(L),var(K),var(Lp)) = 0 >= 0 = if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) = 2S + T + 0 >= 2S + T + 0 = apply(ren(X,Y,T),ren(X,Y,S)) ren(X,Y,lambda(Z,T)) = 2T + -5Z + -5 >= 2T + -5 = 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))) problem: DPs: ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Restore Modifier: DPs: ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) -> ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Arctic Interpretation Processor: dimension: 1 usable rules: if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) interpretation: [ren#](x0, x1, x2) = x2, [ren](x0, x1, x2) = x2, [if](x0, x1, x2) = x1 + x2 + 0, [lambda](x0, x1) = x0 + 4x1 + 0, [apply](x0, x1) = 6x0 + x1 + 5, [var](x0) = 0, [cons](x0, x1) = x0 + 0, [eq](x0, x1) = x1 + 0, [nil] = 2, [true] = 0, [and](x0, x1) = 5x1 + 0, [false] = 1 orientation: ren#(X,Y,apply(T,S)) = S + 6T + 5 >= S = ren#(X,Y,S) ren#(X,Y,apply(T,S)) = S + 6T + 5 >= T = ren#(X,Y,T) ren#(X,Y,lambda(Z,T)) = 4T + Z + 0 >= T = ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)) and(false(),false()) = 6 >= 1 = false() and(true(),false()) = 6 >= 1 = false() and(false(),true()) = 5 >= 1 = false() and(true(),true()) = 5 >= 0 = true() eq(nil(),nil()) = 2 >= 0 = true() eq(cons(T,L),nil()) = 2 >= 1 = false() eq(nil(),cons(T,L)) = T + 0 >= 1 = false() eq(cons(T,L),cons(Tp,Lp)) = Tp + 0 >= 5Lp + 5 = and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) = 0 >= Lp + 0 = eq(L,Lp) eq(var(L),apply(T,S)) = S + 6T + 5 >= 1 = false() eq(var(L),lambda(X,T)) = 4T + X + 0 >= 1 = false() eq(apply(T,S),var(L)) = 0 >= 1 = false() eq(apply(T,S),apply(Tp,Sp)) = Sp + 6Tp + 5 >= 5Sp + 5 = and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) = 4Tp + X + 0 >= 1 = false() eq(lambda(X,T),var(L)) = 0 >= 1 = false() eq(lambda(X,T),apply(Tp,Sp)) = Sp + 6Tp + 5 >= 1 = false() eq(lambda(X,T),lambda(Xp,Tp)) = 4Tp + Xp + 0 >= 5Xp + 5 = and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) = 0 >= 0 = var(K) if(false(),var(K),var(L)) = 0 >= 0 = var(L) ren(var(L),var(K),var(Lp)) = 0 >= 0 = if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) = S + 6T + 5 >= S + 6T + 5 = apply(ren(X,Y,T),ren(X,Y,S)) ren(X,Y,lambda(Z,T)) = 4T + Z + 0 >= 4T + 0 = 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))) problem: DPs: ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Restore Modifier: DPs: ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Size-Change Termination Processor: DPs: TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) The DP: ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) has the edges: 0 >= 0 1 >= 1 2 > 2 The DP: ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) has the edges: 0 >= 0 1 >= 1 2 > 2 Qed DPs: eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) eq#(var(L),var(Lp)) -> eq#(L,Lp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Subterm Criterion Processor: simple projection: pi(eq#) = 0 problem: DPs: TRS: and(false(),false()) -> false() and(true(),false()) -> false() and(false(),true()) -> false() and(true(),true()) -> true() eq(nil(),nil()) -> true() eq(cons(T,L),nil()) -> false() eq(nil(),cons(T,L)) -> false() eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) eq(var(L),var(Lp)) -> eq(L,Lp) eq(var(L),apply(T,S)) -> false() eq(var(L),lambda(X,T)) -> false() eq(apply(T,S),var(L)) -> false() eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) eq(apply(T,S),lambda(X,Tp)) -> false() eq(lambda(X,T),var(L)) -> false() eq(lambda(X,T),apply(Tp,Sp)) -> false() eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) if(true(),var(K),var(L)) -> var(K) if(false(),var(K),var(L)) -> var(L) ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) 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))) Qed