YES
TRS:
 {                  and(true(), y) -> y,
                   and(false(), y) -> false(),
                  eq(nil(), nil()) -> true(),
             eq(nil(), cons(t, l)) -> false(),
             eq(cons(t, l), nil()) -> 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(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))),
      ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
 DP:
  Strict:
   {    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#(l, l'),
                 eq#(var(l), var(l')) -> eq#(l, l'),
      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#(s, s'),
    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'),
              ren#(x, y, apply(t, s)) -> ren#(x, y, 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#(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#(var(l), var(k), var(l')) -> if#(eq(l, l'), var(k), var(l'))}
  Weak:
  {                  and(true(), y) -> y,
                    and(false(), y) -> false(),
                   eq(nil(), nil()) -> true(),
              eq(nil(), cons(t, l)) -> false(),
              eq(cons(t, l), nil()) -> 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(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))),
       ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
  EDG:
   {
    (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, 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#(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, 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, 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#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), 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#(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')) -> and#(eq(t, t'), 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')) -> 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')) -> and#(eq(t, t'), eq(l, l')))
    (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#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), 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#(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')) -> and#(eq(t, t'), 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')) -> 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')) -> and#(eq(t, t'), eq(l, l')))
    (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#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), 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#(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')) -> and#(eq(t, t'), 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')) -> 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')) -> and#(eq(t, t'), eq(l, l')))
    (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#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), 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#(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')) -> and#(eq(t, t'), 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')) -> 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')) -> and#(eq(t, t'), eq(l, l')))
    (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#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), 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#(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')) -> and#(eq(t, t'), 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')) -> 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')) -> and#(eq(t, t'), 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#(t, t'), eq#(var(l), var(l')) -> eq#(l, l'))
    (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#(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#(t, t'))
    (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
    (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#(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#(var(l), var(k), var(l')) -> eq#(l, l'))
    (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')))
    (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#(var(l), var(l')) -> eq#(l, l'), eq#(var(l), var(l')) -> eq#(l, l'))
    (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#(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#(t, t'))
    (eq#(var(l), var(l')) -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
    (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#(x, x'), eq#(var(l), var(l')) -> eq#(l, l'))
    (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#(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#(t, t'))
    (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
    (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#(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#(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#(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#(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#(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#(var(l), var(k), var(l')) -> eq#(l, 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')) -> if#(eq(l, l'), var(k), var(l')))
   }
   SCCS:
    Scc:
     { ren#(x, y, apply(t, s)) -> ren#(x, y, 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#(x, y, lambda(z, t)) -> ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)}
    Scc:
     {    eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
          eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                   eq#(var(l), var(l')) -> eq#(l, l'),
        eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
        eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
      eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
      eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
    SCC:
     Strict:
      { ren#(x, y, apply(t, s)) -> ren#(x, y, 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#(x, y, lambda(z, t)) -> ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)}
     Weak:
     {                  and(true(), y) -> y,
                       and(false(), y) -> false(),
                      eq(nil(), nil()) -> true(),
                 eq(nil(), cons(t, l)) -> false(),
                 eq(cons(t, l), nil()) -> 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(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))),
          ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
     POLY:
      Argument Filtering:
       pi(ren#) = [2], pi(ren) = 2, pi(if) = [], pi(lambda) = 1, pi(apply) = [0,1], pi(var) = [], pi(cons) = [], pi(nil) = [], pi(eq) = [], pi(false) = [], pi(true) = [], pi(and) = []
      Usable Rules:
       {}
      Interpretation:
       [ren#](x0) = x0 + 1,
       [apply](x0, x1) = x0 + x1 + 1
      Strict:
       {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)}
      Weak:
       {                  and(true(), y) -> y,
                         and(false(), y) -> false(),
                        eq(nil(), nil()) -> true(),
                   eq(nil(), cons(t, l)) -> false(),
                   eq(cons(t, l), nil()) -> 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(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))),
            ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
      EDG:
       {(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, 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, 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))}
       SCCS:
        Scc:
         {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)}
        SCC:
         Strict:
          {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)}
         Weak:
         {                  and(true(), y) -> y,
                           and(false(), y) -> false(),
                          eq(nil(), nil()) -> true(),
                     eq(nil(), cons(t, l)) -> false(),
                     eq(cons(t, l), nil()) -> 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(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))),
              ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
         POLY:
          Argument Filtering:
           pi(ren#) = [2], pi(ren) = 2, pi(if) = [], pi(lambda) = [1], pi(apply) = [], pi(var) = [], pi(cons) = [], pi(nil) = [], pi(eq) = [], pi(false) = [], pi(true) = [], pi(and) = []
          Usable Rules:
           {}
          Interpretation:
           [ren#](x0) = x0 + 1,
           [lambda](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {                  and(true(), y) -> y,
                             and(false(), y) -> false(),
                            eq(nil(), nil()) -> true(),
                       eq(nil(), cons(t, l)) -> false(),
                       eq(cons(t, l), nil()) -> 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(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))),
                ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
          Qed
    SCC:
     Strict:
      {    eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
           eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                    eq#(var(l), var(l')) -> eq#(l, l'),
         eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
         eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
       eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
       eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
     Weak:
     {                  and(true(), y) -> y,
                       and(false(), y) -> false(),
                      eq(nil(), nil()) -> true(),
                 eq(nil(), cons(t, l)) -> false(),
                 eq(cons(t, l), nil()) -> 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(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))),
          ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
     SPSC:
      Simple Projection:
       pi(eq#) = 0
      Strict:
       {    eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
            eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                     eq#(var(l), var(l')) -> eq#(l, l'),
          eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
          eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
        eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
      EDG:
       {(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#(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#(t, t'))
        (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')) -> eq#(l, l'))
        (eq#(var(l), var(l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> 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#(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#(t, t'))
        (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')) -> 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#(s, s'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
        (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#(apply(t, s), apply(t', s')) -> eq#(t, t'))
        (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')) -> eq#(l, l'))
        (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), 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#(x, x'), eq#(cons(t, l), cons(t', 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#(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#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
        (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#(t, t'), eq#(var(l), var(l')) -> eq#(l, l'))
        (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#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
        (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'))
        (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#(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#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))}
       SCCS:
        Scc:
         {    eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
              eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                       eq#(var(l), var(l')) -> eq#(l, l'),
            eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
            eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
          eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
        SCC:
         Strict:
          {    eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
               eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                        eq#(var(l), var(l')) -> eq#(l, l'),
             eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
             eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
           eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
         Weak:
         {                  and(true(), y) -> y,
                           and(false(), y) -> false(),
                          eq(nil(), nil()) -> true(),
                     eq(nil(), cons(t, l)) -> false(),
                     eq(cons(t, l), nil()) -> 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(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))),
              ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
         SPSC:
          Simple Projection:
           pi(eq#) = 0
          Strict:
           {  eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
              eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                       eq#(var(l), var(l')) -> eq#(l, l'),
            eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
            eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
          EDG:
           {(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#(apply(t, s), apply(t', s')) -> eq#(t, t'))
            (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')) -> 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#(t, t'), 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#(t, t'))
            (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')) -> eq#(l, l'))
            (eq#(cons(t, l), cons(t', l')) -> 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#(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#(t, t'), eq#(var(l), var(l')) -> eq#(l, l'))
            (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#(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#(var(l), var(l')) -> eq#(l, l'), eq#(var(l), var(l')) -> eq#(l, l'))
            (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#(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#(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#(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'))}
           SCCS:
            Scc:
             {  eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
                eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                         eq#(var(l), var(l')) -> eq#(l, l'),
              eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
              eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
            SCC:
             Strict:
              {  eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
                 eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                          eq#(var(l), var(l')) -> eq#(l, l'),
               eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
               eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
             Weak:
             {                  and(true(), y) -> y,
                               and(false(), y) -> false(),
                              eq(nil(), nil()) -> true(),
                         eq(nil(), cons(t, l)) -> false(),
                         eq(cons(t, l), nil()) -> 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(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))),
                  ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
             SPSC:
              Simple Projection:
               pi(eq#) = 0
              Strict:
               {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                           eq#(var(l), var(l')) -> eq#(l, l'),
                eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
                eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
              EDG:
               {(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#(apply(t, s), apply(t', s')) -> eq#(t, t'))
                (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')) -> eq#(l, l'))
                (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#(apply(t, s), apply(t', s')) -> eq#(t, t'))
                (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')) -> eq#(l, l'))
                (eq#(var(l), var(l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
                (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#(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#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
                (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#(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'))}
               SCCS:
                Scc:
                 {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                             eq#(var(l), var(l')) -> eq#(l, l'),
                  eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
                  eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
                SCC:
                 Strict:
                  {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                              eq#(var(l), var(l')) -> eq#(l, l'),
                   eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
                   eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
                 Weak:
                 {                  and(true(), y) -> y,
                                   and(false(), y) -> false(),
                                  eq(nil(), nil()) -> true(),
                             eq(nil(), cons(t, l)) -> false(),
                             eq(cons(t, l), nil()) -> 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(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))),
                      ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
                 SPSC:
                  Simple Projection:
                   pi(eq#) = 0
                  Strict:
                   {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                               eq#(var(l), var(l')) -> eq#(l, l'),
                    eq#(apply(t, s), apply(t', s')) -> eq#(t, t')}
                  EDG:
                   {(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#(var(l), var(l')) -> eq#(l, l'))
                    (eq#(var(l), var(l')) -> eq#(l, l'), 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#(t, t'), eq#(var(l), var(l')) -> eq#(l, l'))
                    (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
                    (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
                    (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#(apply(t, s), apply(t', s')) -> eq#(t, t'))}
                   SCCS:
                    Scc:
                     {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                                 eq#(var(l), var(l')) -> eq#(l, l'),
                      eq#(apply(t, s), apply(t', s')) -> eq#(t, t')}
                    SCC:
                     Strict:
                      {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                                  eq#(var(l), var(l')) -> eq#(l, l'),
                       eq#(apply(t, s), apply(t', s')) -> eq#(t, t')}
                     Weak:
                     {                  and(true(), y) -> y,
                                       and(false(), y) -> false(),
                                      eq(nil(), nil()) -> true(),
                                 eq(nil(), cons(t, l)) -> false(),
                                 eq(cons(t, l), nil()) -> 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(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))),
                          ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
                     SPSC:
                      Simple Projection:
                       pi(eq#) = 1
                      Strict:
                       {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                        eq#(apply(t, s), apply(t', s')) -> eq#(t, t')}
                      EDG:
                       {(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#(cons(t, l), cons(t', l')) -> eq#(l, l'))
                        (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
                        (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))}
                       SCCS:
                        Scc:
                         {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                          eq#(apply(t, s), apply(t', s')) -> eq#(t, t')}
                        SCC:
                         Strict:
                          {  eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                           eq#(apply(t, s), apply(t', s')) -> eq#(t, t')}
                         Weak:
                         {                  and(true(), y) -> y,
                                           and(false(), y) -> false(),
                                          eq(nil(), nil()) -> true(),
                                     eq(nil(), cons(t, l)) -> false(),
                                     eq(cons(t, l), nil()) -> 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(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))),
                              ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
                         SPSC:
                          Simple Projection:
                           pi(eq#) = 0
                          Strict:
                           {eq#(cons(t, l), cons(t', l')) -> eq#(l, l')}
                          EDG:
                           {(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))}
                           SCCS:
                            Scc:
                             {eq#(cons(t, l), cons(t', l')) -> eq#(l, l')}
                            SCC:
                             Strict:
                              {eq#(cons(t, l), cons(t', l')) -> eq#(l, l')}
                             Weak:
                             {                  and(true(), y) -> y,
                                               and(false(), y) -> false(),
                                              eq(nil(), nil()) -> true(),
                                         eq(nil(), cons(t, l)) -> false(),
                                         eq(cons(t, l), nil()) -> 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(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))),
                                  ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))}
                             SPSC:
                              Simple Projection:
                               pi(eq#) = 0
                              Strict:
                               {}
                              Qed