(STRATEGY
    INNERMOST)

(VAR
    k l l' s s' t t' x x' y z)
(DATATYPES
    A = µX.< true, false, 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(true(),y) -> y
    and(false(),y) -> false()
    eq(nil(),nil()) -> true()
    eq(cons(t,l),nil()) -> false()
    eq(nil(),cons(t,l)) -> false()
    eq(cons(t,l),cons(t',l')) ->
      and(eq(t,t'),eq(l,l'))
    eq(var(l),var(l')) -> eq(l,l')
    eq(var(l),apply(t,s)) -> false()
    eq(var(l),lambda(x,t)) ->
      false()
    eq(apply(t,s),var(l)) -> false()
    eq(apply(t,s),apply(t',s')) ->
      and(eq(t,t'),eq(s,s'))
    eq(apply(t,s),lambda(x,t)) ->
      false()
    eq(lambda(x,t),var(l)) ->
      false()
    eq(lambda(x,t),apply(t,s)) ->
      false()
    eq(lambda(x,t),lambda(x',t')) ->
      and(eq(x,x'),eq(t,t'))
    if(true(),var(k),var(l')) ->
      var(k)
    if(false(),var(k),var(l')) ->
      var(l')
    ren(var(l),var(k),var(l')) ->
      if(eq(l,l'),var(k),var(l'))
    ren(x,y,apply(t,s)) ->
      apply(ren(x,y,t),ren(x,y,s))
    ren(x,y,lambda(z,t)) ->
      lambda(var(cons(x
                     ,cons(y
                          ,cons(lambda(z,t),nil()))))
            ,ren(x
                ,y
                ,ren(z
                    ,var(cons(x
                             ,cons(y
                                  ,cons(lambda(z,t),nil()))))
                    ,t))))