YES

Problem:
 and(true(),y) -> y
 and(false(),y) -> false()
 eq(nil(),nil()) -> true()
 eq(cons(t,l),nil()) -> false()
 eq(nil(),cons(t,l)) -> false()
 eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
 eq(var(l),var(l')) -> eq(l,l')
 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(t',s')) -> and(eq(t,t'),eq(s,s'))
 eq(apply(t,s),lambda(x,t)) -> false()
 eq(lambda(x,t),var(l)) -> false()
 eq(lambda(x,t),apply(t,s)) -> false()
 eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
 if(true(),var(k),var(l')) -> var(k)
 if(false(),var(k),var(l')) -> var(l')
 ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
 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(t',l')) -> eq#(l,l')
   eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
   eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
   eq#(var(l),var(l')) -> eq#(l,l')
   eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
   eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
   eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
   eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
   eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
   eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
   ren#(var(l),var(k),var(l')) -> eq#(l,l')
   ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
   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(true(),y) -> y
   and(false(),y) -> false()
   eq(nil(),nil()) -> true()
   eq(cons(t,l),nil()) -> false()
   eq(nil(),cons(t,l)) -> false()
   eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
   eq(var(l),var(l')) -> eq(l,l')
   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(t',s')) -> and(eq(t,t'),eq(s,s'))
   eq(apply(t,s),lambda(x,t)) -> false()
   eq(lambda(x,t),var(l)) -> false()
   eq(lambda(x,t),apply(t,s)) -> false()
   eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
   if(true(),var(k),var(l')) -> var(k)
   if(false(),var(k),var(l')) -> var(l')
   ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
   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(t',l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
    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(true(),y) -> y
    and(false(),y) -> false()
    eq(nil(),nil()) -> true()
    eq(cons(t,l),nil()) -> false()
    eq(nil(),cons(t,l)) -> false()
    eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
    eq(var(l),var(l')) -> eq(l,l')
    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(t',s')) -> and(eq(t,t'),eq(s,s'))
    eq(apply(t,s),lambda(x,t)) -> false()
    eq(lambda(x,t),var(l)) -> false()
    eq(lambda(x,t),apply(t,s)) -> false()
    eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
    if(true(),var(k),var(l')) -> var(k)
    if(false(),var(k),var(l')) -> var(l')
    ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
    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(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    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(l')) -> if#(eq(l,l'),var(k),var(l'))
    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(l')) -> eq#(l,l')
    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(l')) -> if#(eq(l,l'),var(k),var(l'))
    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(l')) -> eq#(l,l')
    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(l')) -> if#(eq(l,l'),var(k),var(l'))
    ren#(x,y,apply(t,s)) -> ren#(x,y,t) ->
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    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(l')) -> if#(eq(l,l'),var(k),var(l'))
    ren#(x,y,apply(t,s)) -> ren#(x,y,s) ->
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') -> eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
   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(true(),y) -> y
     and(false(),y) -> false()
     eq(nil(),nil()) -> true()
     eq(cons(t,l),nil()) -> false()
     eq(nil(),cons(t,l)) -> false()
     eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
     eq(var(l),var(l')) -> eq(l,l')
     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(t',s')) -> and(eq(t,t'),eq(s,s'))
     eq(apply(t,s),lambda(x,t)) -> false()
     eq(lambda(x,t),var(l)) -> false()
     eq(lambda(x,t),apply(t,s)) -> false()
     eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
     if(true(),var(k),var(l')) -> var(k)
     if(false(),var(k),var(l')) -> var(l')
     ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
     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(l')) -> if(eq(l,l'),var(k),var(l'))
      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) = x0 + 1x2,
      
      [ren](x0, x1, x2) = x2,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [lambda](x0, x1) = 3x0 + 1x1 + 5,
      
      [apply](x0, x1) = 4x0 + 4x1 + 1,
      
      [var](x0) = 2,
      
      [cons](x0, x1) = 1x0 + x1 + 4,
      
      [eq](x0, x1) = x1,
      
      [nil] = 5,
      
      [false] = 0,
      
      [and](x0, x1) = x0 + x1,
      
      [true] = 0
     orientation:
      ren#(x,y,lambda(z,t)) = 2t + x + 4z + 6 >= 1t + z = ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
      
      ren#(x,y,apply(t,s)) = 5s + 5t + x + 2 >= 1s + x = ren#(x,y,s)
      
      ren#(x,y,apply(t,s)) = 5s + 5t + x + 2 >= 1t + x = ren#(x,y,t)
      
      ren#(x,y,lambda(z,t)) = 2t + x + 4z + 6 >= 1t + x = ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
      
      and(true(),y) = y + 0 >= y = y
      
      and(false(),y) = y + 0 >= 0 = false()
      
      eq(nil(),nil()) = 5 >= 0 = true()
      
      eq(cons(t,l),nil()) = 5 >= 0 = false()
      
      eq(nil(),cons(t,l)) = l + 1t + 4 >= 0 = false()
      
      eq(cons(t,l),cons(t',l')) = l' + 1t' + 4 >= l' + t' = and(eq(t,t'),eq(l,l'))
      
      eq(var(l),var(l')) = 2 >= l' = eq(l,l')
      
      eq(var(l),apply(t,s)) = 4s + 4t + 1 >= 0 = false()
      
      eq(var(l),lambda(x,t)) = 1t + 3x + 5 >= 0 = false()
      
      eq(apply(t,s),var(l)) = 2 >= 0 = false()
      
      eq(apply(t,s),apply(t',s')) = 4s' + 4t' + 1 >= s' + t' = and(eq(t,t'),eq(s,s'))
      
      eq(apply(t,s),lambda(x,t)) = 1t + 3x + 5 >= 0 = false()
      
      eq(lambda(x,t),var(l)) = 2 >= 0 = false()
      
      eq(lambda(x,t),apply(t,s)) = 4s + 4t + 1 >= 0 = false()
      
      eq(lambda(x,t),lambda(x',t')) = 1t' + 3x' + 5 >= t' + x' = and(eq(x,x'),eq(t,t'))
      
      if(true(),var(k),var(l')) = 2 >= 2 = var(k)
      
      if(false(),var(k),var(l')) = 2 >= 2 = var(l')
      
      ren(var(l),var(k),var(l')) = 2 >= 2 = if(eq(l,l'),var(k),var(l'))
      
      ren(x,y,apply(t,s)) = 4s + 4t + 1 >= 4s + 4t + 1 = apply(ren(x,y,t),ren(x,y,s))
      
      ren(x,y,lambda(z,t)) = 1t + 3z + 5 >= 1t + 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(true(),y) -> y
       and(false(),y) -> false()
       eq(nil(),nil()) -> true()
       eq(cons(t,l),nil()) -> false()
       eq(nil(),cons(t,l)) -> false()
       eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
       eq(var(l),var(l')) -> eq(l,l')
       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(t',s')) -> and(eq(t,t'),eq(s,s'))
       eq(apply(t,s),lambda(x,t)) -> false()
       eq(lambda(x,t),var(l)) -> false()
       eq(lambda(x,t),apply(t,s)) -> false()
       eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
       if(true(),var(k),var(l')) -> var(k)
       if(false(),var(k),var(l')) -> var(l')
       ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
       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(true(),y) -> y
       and(false(),y) -> false()
       eq(nil(),nil()) -> true()
       eq(cons(t,l),nil()) -> false()
       eq(nil(),cons(t,l)) -> false()
       eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
       eq(var(l),var(l')) -> eq(l,l')
       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(t',s')) -> and(eq(t,t'),eq(s,s'))
       eq(apply(t,s),lambda(x,t)) -> false()
       eq(lambda(x,t),var(l)) -> false()
       eq(lambda(x,t),apply(t,s)) -> false()
       eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
       if(true(),var(k),var(l')) -> var(k)
       if(false(),var(k),var(l')) -> var(l')
       ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
       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:
        and(true(),y) -> y
        and(false(),y) -> false()
        eq(nil(),nil()) -> true()
        eq(cons(t,l),nil()) -> false()
        eq(nil(),cons(t,l)) -> false()
        eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
        eq(var(l),var(l')) -> eq(l,l')
        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(t',s')) -> and(eq(t,t'),eq(s,s'))
        eq(apply(t,s),lambda(x,t)) -> false()
        eq(lambda(x,t),var(l)) -> false()
        eq(lambda(x,t),apply(t,s)) -> false()
        eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
        if(true(),var(k),var(l')) -> var(k)
        if(false(),var(k),var(l')) -> var(l')
        ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
        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) = x0 + -8x1 + -8x2 + 0,
        
        [lambda](x0, x1) = 1x1,
        
        [apply](x0, x1) = 3x0 + x1 + 2,
        
        [var](x0) = 0,
        
        [cons](x0, x1) = -4x0 + x1 + 0,
        
        [eq](x0, x1) = 0,
        
        [nil] = 3,
        
        [false] = 0,
        
        [and](x0, x1) = x0 + x1 + 0,
        
        [true] = 0
       orientation:
        ren#(x,y,apply(t,s)) = s + 3t + 2 >= s = ren#(x,y,s)
        
        ren#(x,y,apply(t,s)) = s + 3t + 2 >= t = ren#(x,y,t)
        
        ren#(x,y,lambda(z,t)) = 1t >= t = ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
        
        and(true(),y) = y + 0 >= y = y
        
        and(false(),y) = y + 0 >= 0 = false()
        
        eq(nil(),nil()) = 0 >= 0 = true()
        
        eq(cons(t,l),nil()) = 0 >= 0 = false()
        
        eq(nil(),cons(t,l)) = 0 >= 0 = false()
        
        eq(cons(t,l),cons(t',l')) = 0 >= 0 = and(eq(t,t'),eq(l,l'))
        
        eq(var(l),var(l')) = 0 >= 0 = eq(l,l')
        
        eq(var(l),apply(t,s)) = 0 >= 0 = false()
        
        eq(var(l),lambda(x,t)) = 0 >= 0 = false()
        
        eq(apply(t,s),var(l)) = 0 >= 0 = false()
        
        eq(apply(t,s),apply(t',s')) = 0 >= 0 = and(eq(t,t'),eq(s,s'))
        
        eq(apply(t,s),lambda(x,t)) = 0 >= 0 = false()
        
        eq(lambda(x,t),var(l)) = 0 >= 0 = false()
        
        eq(lambda(x,t),apply(t,s)) = 0 >= 0 = false()
        
        eq(lambda(x,t),lambda(x',t')) = 0 >= 0 = and(eq(x,x'),eq(t,t'))
        
        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(l')) = 0 >= 0 = if(eq(l,l'),var(k),var(l'))
        
        ren(x,y,apply(t,s)) = s + 3t + 2 >= s + 3t + 2 = apply(ren(x,y,t),ren(x,y,s))
        
        ren(x,y,lambda(z,t)) = 1t >= 1t = 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(true(),y) -> y
         and(false(),y) -> false()
         eq(nil(),nil()) -> true()
         eq(cons(t,l),nil()) -> false()
         eq(nil(),cons(t,l)) -> false()
         eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
         eq(var(l),var(l')) -> eq(l,l')
         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(t',s')) -> and(eq(t,t'),eq(s,s'))
         eq(apply(t,s),lambda(x,t)) -> false()
         eq(lambda(x,t),var(l)) -> false()
         eq(lambda(x,t),apply(t,s)) -> false()
         eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
         if(true(),var(k),var(l')) -> var(k)
         if(false(),var(k),var(l')) -> var(l')
         ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
         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(true(),y) -> y
         and(false(),y) -> false()
         eq(nil(),nil()) -> true()
         eq(cons(t,l),nil()) -> false()
         eq(nil(),cons(t,l)) -> false()
         eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
         eq(var(l),var(l')) -> eq(l,l')
         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(t',s')) -> and(eq(t,t'),eq(s,s'))
         eq(apply(t,s),lambda(x,t)) -> false()
         eq(lambda(x,t),var(l)) -> false()
         eq(lambda(x,t),apply(t,s)) -> false()
         eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
         if(true(),var(k),var(l')) -> var(k)
         if(false(),var(k),var(l')) -> var(l')
         ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
         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(true(),y) -> y
          and(false(),y) -> false()
          eq(nil(),nil()) -> true()
          eq(cons(t,l),nil()) -> false()
          eq(nil(),cons(t,l)) -> false()
          eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
          eq(var(l),var(l')) -> eq(l,l')
          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(t',s')) -> and(eq(t,t'),eq(s,s'))
          eq(apply(t,s),lambda(x,t)) -> false()
          eq(lambda(x,t),var(l)) -> false()
          eq(lambda(x,t),apply(t,s)) -> false()
          eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
          if(true(),var(k),var(l')) -> var(k)
          if(false(),var(k),var(l')) -> var(l')
          ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
          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(t',l')) -> eq#(l,l')
     eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
     eq#(var(l),var(l')) -> eq#(l,l')
     eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
     eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
     eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
     eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    TRS:
     and(true(),y) -> y
     and(false(),y) -> false()
     eq(nil(),nil()) -> true()
     eq(cons(t,l),nil()) -> false()
     eq(nil(),cons(t,l)) -> false()
     eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
     eq(var(l),var(l')) -> eq(l,l')
     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(t',s')) -> and(eq(t,t'),eq(s,s'))
     eq(apply(t,s),lambda(x,t)) -> false()
     eq(lambda(x,t),var(l)) -> false()
     eq(lambda(x,t),apply(t,s)) -> false()
     eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
     if(true(),var(k),var(l')) -> var(k)
     if(false(),var(k),var(l')) -> var(l')
     ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
     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(true(),y) -> y
       and(false(),y) -> false()
       eq(nil(),nil()) -> true()
       eq(cons(t,l),nil()) -> false()
       eq(nil(),cons(t,l)) -> false()
       eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
       eq(var(l),var(l')) -> eq(l,l')
       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(t',s')) -> and(eq(t,t'),eq(s,s'))
       eq(apply(t,s),lambda(x,t)) -> false()
       eq(lambda(x,t),var(l)) -> false()
       eq(lambda(x,t),apply(t,s)) -> false()
       eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
       if(true(),var(k),var(l')) -> var(k)
       if(false(),var(k),var(l')) -> var(l')
       ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
       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