YES
TRS:
 {           and(false(), false()) -> false(),
              and(false(), true()) -> false(),
              and(true(), false()) -> false(),
               and(true(), true()) -> true(),
                  eq(nil(), nil()) -> true(),
             eq(nil(), cons(T, L)) -> false(),
             eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
        if(true(), var(K), var(L)) -> var(K),
            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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
 DP:
  Strict:
   {    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#(L, Lp),
                 eq#(var(L), var(Lp)) -> eq#(L, Lp),
      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#(S, Sp),
    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#(X, Xp),
              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(Lp)) -> eq#(L, Lp),
        ren#(var(L), var(K), var(Lp)) -> if#(eq(L, Lp), var(K), var(Lp))}
  Weak:
  {           and(false(), false()) -> false(),
               and(false(), true()) -> false(),
               and(true(), false()) -> false(),
                and(true(), true()) -> true(),
                   eq(nil(), nil()) -> true(),
              eq(nil(), cons(T, L)) -> false(),
              eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
         if(true(), var(K), var(L)) -> var(K),
             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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
  EDG:
   {
    (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#(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)) -> and#(eq(T, Tp), eq(X, Xp)))
    (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#(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)) -> and#(eq(T, Tp), 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)) -> 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)) -> and#(eq(T, Tp), eq(L, Lp)))
    (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#(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)) -> and#(eq(T, Tp), eq(X, Xp)))
    (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#(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)) -> and#(eq(T, Tp), 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)) -> 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)) -> and#(eq(T, Tp), 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#(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, 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#(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, apply(T, S)) -> ren#(X, Y, T))
    (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, 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(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#(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)) -> and#(eq(T, Tp), eq(X, Xp)))
    (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#(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)) -> and#(eq(T, Tp), 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)) -> 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)) -> and#(eq(T, Tp), eq(L, Lp)))
    (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#(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)) -> and#(eq(T, Tp), eq(X, Xp)))
    (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#(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)) -> and#(eq(T, Tp), 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)) -> 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)) -> and#(eq(T, Tp), 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#(var(L), var(Lp)) -> eq#(L, Lp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
    (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#(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#(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#(X, Xp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
    (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#(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))
    (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(Lp)) -> eq#(L, 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)) -> 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, 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(Lp)) -> eq#(L, Lp))
    (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)))
    (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#(T, Tp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
    (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#(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#(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#(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#(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#(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))
   }
   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(Tp, Lp)) -> eq#(T, Tp),
          eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                   eq#(var(L), var(Lp)) -> eq#(L, Lp),
        eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
        eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
      eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp),
      eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)}
    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(false(), false()) -> false(),
                  and(false(), true()) -> false(),
                  and(true(), false()) -> false(),
                   and(true(), true()) -> true(),
                      eq(nil(), nil()) -> true(),
                 eq(nil(), cons(T, L)) -> false(),
                 eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
            if(true(), var(K), var(L)) -> var(K),
                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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
     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(true) = [], pi(and) = [], pi(false) = []
      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(false(), false()) -> false(),
                    and(false(), true()) -> false(),
                    and(true(), false()) -> false(),
                     and(true(), true()) -> true(),
                        eq(nil(), nil()) -> true(),
                   eq(nil(), cons(T, L)) -> false(),
                   eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
              if(true(), var(K), var(L)) -> var(K),
                  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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
      EDG:
       {(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, 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#(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))}
       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(false(), false()) -> false(),
                      and(false(), true()) -> false(),
                      and(true(), false()) -> false(),
                       and(true(), true()) -> true(),
                          eq(nil(), nil()) -> true(),
                     eq(nil(), cons(T, L)) -> false(),
                     eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                if(true(), var(K), var(L)) -> var(K),
                    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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
         POLY:
          Argument Filtering:
           pi(ren#) = [0,2], pi(ren) = 2, pi(if) = [], pi(lambda) = [0,1], pi(apply) = [], pi(var) = [], pi(cons) = [], pi(nil) = [], pi(eq) = [], pi(true) = [], pi(and) = [], pi(false) = []
          Usable Rules:
           {}
          Interpretation:
           [ren#](x0, x1) = x0 + x1,
           [lambda](x0, x1) = x0 + x1 + 1
          Strict:
           {}
          Weak:
           {           and(false(), false()) -> false(),
                        and(false(), true()) -> false(),
                        and(true(), false()) -> false(),
                         and(true(), true()) -> true(),
                            eq(nil(), nil()) -> true(),
                       eq(nil(), cons(T, L)) -> false(),
                       eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                  if(true(), var(K), var(L)) -> var(K),
                      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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
          Qed
    SCC:
     Strict:
      {    eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
           eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                    eq#(var(L), var(Lp)) -> eq#(L, Lp),
         eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
         eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
       eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp),
       eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)}
     Weak:
     {           and(false(), false()) -> false(),
                  and(false(), true()) -> false(),
                  and(true(), false()) -> false(),
                   and(true(), true()) -> true(),
                      eq(nil(), nil()) -> true(),
                 eq(nil(), cons(T, L)) -> false(),
                 eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
            if(true(), var(K), var(L)) -> var(K),
                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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
     SPSC:
      Simple Projection:
       pi(eq#) = 1
      Strict:
       {    eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
            eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                     eq#(var(L), var(Lp)) -> eq#(L, Lp),
          eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
          eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
        eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)}
      EDG:
       {(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)) -> 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#(var(L), var(Lp)) -> eq#(L, Lp))
        (eq#(var(L), var(Lp)) -> eq#(L, Lp), 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#(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)) -> 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#(var(L), var(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#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> 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)) -> 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#(var(L), var(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#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), 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#(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#(X, Xp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
        (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#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
        (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#(T, Tp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
        (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#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
        (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))
        (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#(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#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))}
       SCCS:
        Scc:
         {    eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
              eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                       eq#(var(L), var(Lp)) -> eq#(L, Lp),
            eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
            eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
          eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)}
        SCC:
         Strict:
          {    eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
               eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                        eq#(var(L), var(Lp)) -> eq#(L, Lp),
             eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
             eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
           eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)}
         Weak:
         {           and(false(), false()) -> false(),
                      and(false(), true()) -> false(),
                      and(true(), false()) -> false(),
                       and(true(), true()) -> true(),
                          eq(nil(), nil()) -> true(),
                     eq(nil(), cons(T, L)) -> false(),
                     eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                if(true(), var(K), var(L)) -> var(K),
                    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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
         SPSC:
          Simple Projection:
           pi(eq#) = 0
          Strict:
           {  eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
              eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                       eq#(var(L), var(Lp)) -> eq#(L, Lp),
            eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
            eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)}
          EDG:
           {(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#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
            (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)) -> eq#(L, Lp))
            (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> 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#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
            (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)) -> eq#(L, Lp))
            (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#(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#(var(L), var(Lp)) -> eq#(L, Lp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
            (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#(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#(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#(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#(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#(T, Tp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
            (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))}
           SCCS:
            Scc:
             {  eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                         eq#(var(L), var(Lp)) -> eq#(L, Lp),
              eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
              eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)}
            SCC:
             Strict:
              {  eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                 eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                          eq#(var(L), var(Lp)) -> eq#(L, Lp),
               eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
               eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)}
             Weak:
             {           and(false(), false()) -> false(),
                          and(false(), true()) -> false(),
                          and(true(), false()) -> false(),
                           and(true(), true()) -> true(),
                              eq(nil(), nil()) -> true(),
                         eq(nil(), cons(T, L)) -> false(),
                         eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                    if(true(), var(K), var(L)) -> var(K),
                        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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
             SPSC:
              Simple Projection:
               pi(eq#) = 0
              Strict:
               {  eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                  eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                           eq#(var(L), var(Lp)) -> eq#(L, Lp),
                eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)}
              EDG:
               {(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#(var(L), var(Lp)) -> eq#(L, Lp))
                (eq#(var(L), var(Lp)) -> eq#(L, Lp), 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#(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#(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)) -> eq#(L, Lp))
                (eq#(apply(T, S), apply(Tp, Sp)) -> 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#(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#(T, Tp), eq#(var(L), var(Lp)) -> eq#(L, Lp))
                (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#(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#(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#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))}
               SCCS:
                Scc:
                 {  eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                    eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                             eq#(var(L), var(Lp)) -> eq#(L, Lp),
                  eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)}
                SCC:
                 Strict:
                  {  eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                     eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                              eq#(var(L), var(Lp)) -> eq#(L, Lp),
                   eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)}
                 Weak:
                 {           and(false(), false()) -> false(),
                              and(false(), true()) -> false(),
                              and(true(), false()) -> false(),
                               and(true(), true()) -> true(),
                                  eq(nil(), nil()) -> true(),
                             eq(nil(), cons(T, L)) -> false(),
                             eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                        if(true(), var(K), var(L)) -> var(K),
                            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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
                 SPSC:
                  Simple Projection:
                   pi(eq#) = 0
                  Strict:
                   {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                    eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                             eq#(var(L), var(Lp)) -> eq#(L, Lp)}
                  EDG:
                   {(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)) -> eq#(L, Lp))
                    (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)) -> 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#(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#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
                    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var(L), var(Lp)) -> eq#(L, Lp))}
                   SCCS:
                    Scc:
                     {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                      eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                               eq#(var(L), var(Lp)) -> eq#(L, Lp)}
                    SCC:
                     Strict:
                      {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                       eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                                eq#(var(L), var(Lp)) -> eq#(L, Lp)}
                     Weak:
                     {           and(false(), false()) -> false(),
                                  and(false(), true()) -> false(),
                                  and(true(), false()) -> false(),
                                   and(true(), true()) -> true(),
                                      eq(nil(), nil()) -> true(),
                                 eq(nil(), cons(T, L)) -> false(),
                                 eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                            if(true(), var(K), var(L)) -> var(K),
                                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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
                     SPSC:
                      Simple Projection:
                       pi(eq#) = 0
                      Strict:
                       {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                        eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)}
                      EDG:
                       {(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#(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#(T, Tp))
                        (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))}
                       SCCS:
                        Scc:
                         {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                          eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)}
                        SCC:
                         Strict:
                          {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
                           eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)}
                         Weak:
                         {           and(false(), false()) -> false(),
                                      and(false(), true()) -> false(),
                                      and(true(), false()) -> false(),
                                       and(true(), true()) -> true(),
                                          eq(nil(), nil()) -> true(),
                                     eq(nil(), cons(T, L)) -> false(),
                                     eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                                if(true(), var(K), var(L)) -> var(K),
                                    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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
                         SPSC:
                          Simple Projection:
                           pi(eq#) = 0
                          Strict:
                           {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)}
                          EDG:
                           {(eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))}
                           SCCS:
                            Scc:
                             {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)}
                            SCC:
                             Strict:
                              {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)}
                             Weak:
                             {           and(false(), false()) -> false(),
                                          and(false(), true()) -> false(),
                                          and(true(), false()) -> false(),
                                           and(true(), true()) -> true(),
                                              eq(nil(), nil()) -> true(),
                                         eq(nil(), cons(T, L)) -> false(),
                                         eq(cons(T, L), nil()) -> 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(false(), var(K), var(L)) -> var(L),
                                    if(true(), var(K), var(L)) -> var(K),
                                        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(Lp)) -> if(eq(L, Lp), var(K), var(Lp))}
                             SPSC:
                              Simple Projection:
                               pi(eq#) = 0
                              Strict:
                               {}
                              Qed