(STRATEGY
    INNERMOST)

(VAR
    K L Lp S Sp T Tp X Xp Y Z)
(DATATYPES
    A = µX.< false, true, nil, cons(X, X), var(X), apply(X, X), lambda(X, X) >)
(SIGNATURES
    and :: [A x A] -> A
    eq :: [A x A] -> A
    if :: [A x A x A] -> A
    ren :: [A x A x A] -> A)
(RULES
    and(false(),false()) -> false()
    and(true(),false()) -> false()
    and(false(),true()) -> false()
    and(true(),true()) -> true()
    eq(nil(),nil()) -> true()
    eq(cons(T,L),nil()) -> false()
    eq(nil(),cons(T,L)) -> false()
    eq(cons(T,L),cons(Tp,Lp)) ->
      and(eq(T,Tp),eq(L,Lp))
    eq(var(L),var(Lp)) -> eq(L,Lp)
    eq(var(L),apply(T,S)) -> false()
    eq(var(L),lambda(X,T)) ->
      false()
    eq(apply(T,S),var(L)) -> false()
    eq(apply(T,S),apply(Tp,Sp)) ->
      and(eq(T,Tp),eq(S,Sp))
    eq(apply(T,S),lambda(X,Tp)) ->
      false()
    eq(lambda(X,T),var(L)) ->
      false()
    eq(lambda(X,T),apply(Tp,Sp)) ->
      false()
    eq(lambda(X,T),lambda(Xp,Tp)) ->
      and(eq(T,Tp),eq(X,Xp))
    if(true(),var(K),var(L)) ->
      var(K)
    if(false(),var(K),var(L)) ->
      var(L)
    ren(var(L),var(K),var(Lp)) ->
      if(eq(L,Lp),var(K),var(Lp))
    ren(X,Y,apply(T,S)) ->
      apply(ren(X,Y,T),ren(X,Y,S))
    ren(X,Y,lambda(Z,T)) ->
      lambda(var(cons(X
                     ,cons(Y
                          ,cons(lambda(Z,T),nil()))))
            ,ren(X
                ,Y
                ,ren(Z
                    ,var(cons(X
                             ,cons(Y
                                  ,cons(lambda(Z,T),nil()))))
                    ,T))))