(STRATEGY
    INNERMOST)

(VAR
    b11 b12 b21 b22 e e1 e11 e12 e2
    e21 e22 ef eq11 eq12 eq21 eq22 f
    f0 fe1 fe2 fn1 fn2 i i1 i2 input
    int n nf ns o1 o2 op op1 op2 p s
    t t1 t2 v v1 v2 vs x x' x'' xs
    xs' y)
(DATATYPES
    A = µX.< Fun(X, X), Eq(X, X), Error(X, X), False, F, T, ITE(X, X, X), Bsf(X, X, X), Var(X), Cons(X, X), True, Cst(X), S(X), 0, Nil >)
(SIGNATURES
    eeval :: [A x A x A x A] -> A
    run :: [A x A] -> A
    eqExp :: [A x A] -> A
    checkConstrExp :: [A x A] -> A
    lookname :: [A x A] -> A
    lookbody :: [A x A] -> A
    getVar :: [A] -> A
    getIfTrue :: [A] -> A
    getIfGuard :: [A] -> A
    getIfFalse :: [A] -> A
    getFuncName :: [A] -> A
    getFuncExp :: [A] -> A
    getEqSecond :: [A] -> A
    getEqFirst :: [A] -> A
    getConst :: [A] -> A
    getBsfSecondTerm :: [A] -> A
    getBsfOp :: [A] -> A
    getBsfFirstTerm :: [A] -> A
    apply :: [A x A x A] -> A
    lookvar :: [A x A x A] -> A
    eqOps :: [A x A] -> A
    !EQ :: [A x A] -> A
    and :: [A x A] -> A
    eeval[False][Ite] :: [A x A x A x A x A] -> A
    lookvar[Ite] :: [A x A x A x A] -> A
    lookname[Ite] :: [A x A x A] -> A
    lookbody[Ite] :: [A x A x A] -> A
    eeval[Ite] :: [A x A x A x A x A] -> A
    eeval[False][Let] :: [A x A x A x A x A] -> A
    eeval[False][Let][Let] :: [A x A x A x A x A x A] -> A
    eeval[Let] :: [A x A x A x A x A] -> A
    eeval[Let][Let] :: [A x A x A x A x A x A] -> A
    eeval[True][Ite] :: [A x A x A x A x A] -> A
    apply[Ite] :: [A x A x A x A] -> A
    run[Let][Let] :: [A x A x A x A] -> A
    run[Let] :: [A x A x A x A x A] -> A
    eeval[Let][Let][Let] :: [A x A x A x A x A x A x A] -> A)
(RULES
    eeval(Fun(n,e),ns,vs,p) ->
      eeval[False][Let](Fun(n,e)
                       ,ns
                       ,vs
                       ,p
                       ,lookbody(n,p))
    eeval(Eq(f,s),ns,vs,p) ->
      eeval[True][Ite](eqExp(eeval(f
                                  ,ns
                                  ,vs
                                  ,p)
                            ,eeval(s,ns,vs,p))
                      ,Eq(f,s)
                      ,ns
                      ,vs
                      ,p)
    eeval(Error(e11,e12),ns,vs,p) ->
      eeval[False][Ite](False()
                       ,Error(e11,e12)
                       ,ns
                       ,vs
                       ,p)
    eeval(F(),ns,vs,p) -> F()
    eeval(T(),ns,vs,p) -> T()
    eeval(ITE(i,t,e),ns,vs,p) ->
      eeval[Ite](checkConstrExp(eeval(i
                                     ,ns
                                     ,vs
                                     ,p)
                               ,T())
                ,ITE(i,t,e)
                ,ns
                ,vs
                ,p)
    eeval(Bsf(op,t1,t2),ns,vs,p) ->
      eeval[Let](Bsf(op,t1,t2)
                ,ns
                ,vs
                ,p
                ,eeval(t1,ns,vs,p))
    eeval(Var(int),ns,vs,p) ->
      lookvar(int,ns,vs)
    run(Cons(Fun(f0,e),xs),input) ->
      run[Let][Let](Cons(Fun(f0,e),xs)
                   ,input
                   ,f0
                   ,lookbody(f0
                            ,Cons(Fun(f0,e),xs)))
    eqExp(Error(e11,e12)
         ,Error(e21,e22)) ->
      and(eqExp(e11,e21)
         ,eqExp(e12,e22))
    eqExp(Error(e11,e12),F()) ->
      False()
    eqExp(Error(e11,e12),T()) ->
      False()
    eqExp(Error(e11,e12)
         ,Fun(fn2,fe2)) -> False()
    eqExp(Error(e11,e12)
         ,Eq(eq21,eq22)) -> False()
    eqExp(Error(e11,e12)
         ,ITE(i2,t2,e2)) -> False()
    eqExp(Error(e11,e12)
         ,Bsf(op2,b21,b22)) -> False()
    eqExp(Error(e11,e12),Var(v2)) ->
      False()
    eqExp(F(),Error(e21,e22)) ->
      False()
    eqExp(F(),F()) -> True()
    eqExp(F(),T()) -> False()
    eqExp(F(),Fun(fn2,fe2)) ->
      False()
    eqExp(F(),Eq(eq21,eq22)) ->
      False()
    eqExp(F(),ITE(i2,t2,e2)) ->
      False()
    eqExp(F(),Bsf(op2,b21,b22)) ->
      False()
    eqExp(F(),Var(v2)) -> False()
    eqExp(T(),Error(e21,e22)) ->
      False()
    eqExp(T(),F()) -> False()
    eqExp(T(),T()) -> True()
    eqExp(T(),Fun(fn2,fe2)) ->
      False()
    eqExp(T(),Eq(eq21,eq22)) ->
      False()
    eqExp(T(),ITE(i2,t2,e2)) ->
      False()
    eqExp(T(),Bsf(op2,b21,b22)) ->
      False()
    eqExp(T(),Var(v2)) -> False()
    eqExp(Fun(fn1,fe1)
         ,Error(e21,e22)) -> False()
    eqExp(Fun(fn1,fe1),F()) ->
      False()
    eqExp(Fun(fn1,fe1),T()) ->
      False()
    eqExp(Fun(fn1,fe1)
         ,Fun(fn2,fe2)) -> and(!EQ(fn1
                                  ,fn2)
                              ,eqExp(fe1,fe2))
    eqExp(Fun(fn1,fe1)
         ,Eq(eq21,eq22)) -> False()
    eqExp(Fun(fn1,fe1)
         ,ITE(i2,t2,e2)) -> False()
    eqExp(Fun(fn1,fe1)
         ,Bsf(op2,b21,b22)) -> False()
    eqExp(Fun(fn1,fe1),Var(v2)) ->
      False()
    eqExp(Eq(eq11,eq12)
         ,Error(e21,e22)) -> False()
    eqExp(Eq(eq11,eq12),F()) ->
      False()
    eqExp(Eq(eq11,eq12),T()) ->
      False()
    eqExp(Eq(eq11,eq12)
         ,Fun(fn2,fe2)) -> False()
    eqExp(Eq(eq11,eq12)
         ,Eq(eq21,eq22)) ->
      and(eqExp(eq11,eq21)
         ,eqExp(eq12,eq22))
    eqExp(Eq(eq11,eq12)
         ,ITE(i2,t2,e2)) -> False()
    eqExp(Eq(eq11,eq12)
         ,Bsf(op2,b21,b22)) -> False()
    eqExp(Eq(eq11,eq12),Var(v2)) ->
      False()
    eqExp(ITE(i1,t1,e1)
         ,Error(e21,e22)) -> False()
    eqExp(ITE(i1,t1,e1),F()) ->
      False()
    eqExp(ITE(i1,t1,e1),T()) ->
      False()
    eqExp(ITE(i1,t1,e1)
         ,Fun(fn2,fe2)) -> False()
    eqExp(ITE(i1,t1,e1)
         ,Eq(eq21,eq22)) -> False()
    eqExp(ITE(i1,t1,e1)
         ,ITE(i2,t2,e2)) -> and(eqExp(i1
                                     ,i2)
                               ,and(eqExp(t1,t2),eqExp(e1,e2)))
    eqExp(ITE(i1,t1,e1)
         ,Bsf(op2,b21,b22)) -> False()
    eqExp(ITE(i1,t1,e1),Var(v2)) ->
      False()
    eqExp(Bsf(op1,b11,b12)
         ,Error(e21,e22)) -> False()
    eqExp(Bsf(op1,b11,b12),F()) ->
      False()
    eqExp(Bsf(op1,b11,b12),T()) ->
      False()
    eqExp(Bsf(op1,b11,b12)
         ,Fun(fn2,fe2)) -> False()
    eqExp(Bsf(op1,b11,b12)
         ,Eq(eq21,eq22)) -> False()
    eqExp(Bsf(op1,b11,b12)
         ,ITE(i2,t2,e2)) -> False()
    eqExp(Bsf(o1,b11,b12)
         ,Bsf(o2,b21,b22)) -> and(True()
                                 ,and(eqExp(b11,b21)
                                     ,eqExp(b12,b22)))
    eqExp(Bsf(op1,b11,b12)
         ,Var(v2)) -> False()
    eqExp(Var(v1),Error(e21,e22)) ->
      False()
    eqExp(Var(v1),F()) -> False()
    eqExp(Var(v1),T()) -> False()
    eqExp(Var(v1),Fun(fn2,fe2)) ->
      False()
    eqExp(Var(v1),Eq(eq21,eq22)) ->
      False()
    eqExp(Var(v1),ITE(i2,t2,e2)) ->
      False()
    eqExp(Var(v1)
         ,Bsf(op2,b21,b22)) -> False()
    eqExp(Var(v1),Var(v2)) -> !EQ(v1
                                 ,v2)
    checkConstrExp(Error(e11,e12)
                  ,Error(e21,e22)) -> True()
    checkConstrExp(Error(e11,e12)
                  ,F()) -> False()
    checkConstrExp(Error(e11,e12)
                  ,T()) -> False()
    checkConstrExp(Error(e11,e12)
                  ,Fun(fn2,fe2)) -> False()
    checkConstrExp(Error(e11,e12)
                  ,Eq(eq21,eq22)) -> False()
    checkConstrExp(Error(e11,e12)
                  ,ITE(i2,t2,e2)) -> False()
    checkConstrExp(Error(e11,e12)
                  ,Bsf(op2,b21,b22)) -> False()
    checkConstrExp(Error(e11,e12)
                  ,Var(v2)) -> False()
    checkConstrExp(F()
                  ,Error(e21,e22)) -> False()
    checkConstrExp(F(),F()) ->
      True()
    checkConstrExp(F(),T()) ->
      False()
    checkConstrExp(F()
                  ,Fun(fn2,fe2)) -> False()
    checkConstrExp(F()
                  ,Eq(eq21,eq22)) -> False()
    checkConstrExp(F()
                  ,ITE(i2,t2,e2)) -> False()
    checkConstrExp(F()
                  ,Bsf(op2,b21,b22)) -> False()
    checkConstrExp(F(),Var(v2)) ->
      False()
    checkConstrExp(T()
                  ,Error(e21,e22)) -> False()
    checkConstrExp(T(),F()) ->
      False()
    checkConstrExp(T(),T()) ->
      True()
    checkConstrExp(T()
                  ,Fun(fn2,fe2)) -> False()
    checkConstrExp(T()
                  ,Eq(eq21,eq22)) -> False()
    checkConstrExp(T()
                  ,ITE(i2,t2,e2)) -> False()
    checkConstrExp(T()
                  ,Bsf(op2,b21,b22)) -> False()
    checkConstrExp(T(),Var(v2)) ->
      False()
    checkConstrExp(Fun(fn1,fe1)
                  ,Error(e21,e22)) -> False()
    checkConstrExp(Fun(fn1,fe1)
                  ,F()) -> False()
    checkConstrExp(Fun(fn1,fe1)
                  ,T()) -> False()
    checkConstrExp(Fun(fn1,fe1)
                  ,Fun(fn2,fe2)) -> True()
    checkConstrExp(Fun(fn1,fe1)
                  ,Eq(eq21,eq22)) -> False()
    checkConstrExp(Fun(fn1,fe1)
                  ,ITE(i2,t2,e2)) -> False()
    checkConstrExp(Fun(fn1,fe1)
                  ,Bsf(op2,b21,b22)) -> False()
    checkConstrExp(Fun(fn1,fe1)
                  ,Var(v2)) -> False()
    checkConstrExp(Eq(eq11,eq12)
                  ,Error(e21,e22)) -> False()
    checkConstrExp(Eq(eq11,eq12)
                  ,F()) -> False()
    checkConstrExp(Eq(eq11,eq12)
                  ,T()) -> False()
    checkConstrExp(Eq(eq11,eq12)
                  ,Fun(fn2,fe2)) -> False()
    checkConstrExp(Eq(eq11,eq12)
                  ,Eq(eq21,eq22)) -> True()
    checkConstrExp(Eq(eq11,eq12)
                  ,ITE(i2,t2,e2)) -> False()
    checkConstrExp(Eq(eq11,eq12)
                  ,Bsf(op2,b21,b22)) -> False()
    checkConstrExp(Eq(eq11,eq12)
                  ,Var(v2)) -> False()
    checkConstrExp(ITE(i1,t1,e1)
                  ,Error(e21,e22)) -> False()
    checkConstrExp(ITE(i1,t1,e1)
                  ,F()) -> False()
    checkConstrExp(ITE(i1,t1,e1)
                  ,T()) -> False()
    checkConstrExp(ITE(i1,t1,e1)
                  ,Fun(fn2,fe2)) -> False()
    checkConstrExp(ITE(i1,t1,e1)
                  ,Eq(eq21,eq22)) -> False()
    checkConstrExp(ITE(i1,t1,e1)
                  ,ITE(i2,t2,e2)) -> True()
    checkConstrExp(ITE(i1,t1,e1)
                  ,Bsf(op2,b21,b22)) -> False()
    checkConstrExp(ITE(i1,t1,e1)
                  ,Var(v2)) -> False()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,Error(e21,e22)) -> False()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,F()) -> False()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,T()) -> False()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,Fun(fn2,fe2)) -> False()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,Eq(eq21,eq22)) -> False()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,ITE(i2,t2,e2)) -> False()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,Bsf(op2,b21,b22)) -> True()
    checkConstrExp(Bsf(op1,b11,b12)
                  ,Var(v2)) -> False()
    checkConstrExp(Var(v1)
                  ,Error(e21,e22)) -> False()
    checkConstrExp(Var(v1),F()) ->
      False()
    checkConstrExp(Var(v1),T()) ->
      False()
    checkConstrExp(Var(v1)
                  ,Fun(fn2,fe2)) -> False()
    checkConstrExp(Var(v1)
                  ,Eq(eq21,eq22)) -> False()
    checkConstrExp(Var(v1)
                  ,ITE(i2,t2,e2)) -> False()
    checkConstrExp(Var(v1)
                  ,Bsf(op2,b21,b22)) -> False()
    checkConstrExp(Var(v1)
                  ,Var(v2)) -> True()
    lookname(f,Cons(Fun(n,e),xs)) ->
      lookname[Ite](!EQ(f,n)
                   ,f
                   ,Cons(Fun(n,e),xs))
    lookbody(f,Cons(Fun(n,e),xs)) ->
      lookbody[Ite](!EQ(f,n)
                   ,f
                   ,Cons(Fun(n,e),xs))
    getVar(Var(int)) -> int
    getIfTrue(ITE(i,t,e)) -> t
    getIfGuard(ITE(i,t,e)) -> i
    getIfFalse(ITE(i,t,e)) -> e
    getFuncName(Fun(n,e)) -> n
    getFuncExp(Fun(n,e)) -> e
    getEqSecond(Eq(f,s)) -> s
    getEqFirst(Eq(f,s)) -> f
    getConst(Cst(int)) -> int
    getBsfSecondTerm(Bsf(op
                        ,t1
                        ,t2)) -> t2
    getBsfOp(Bsf(op,t1,t2)) -> op
    getBsfFirstTerm(Bsf(op
                       ,t1
                       ,t2)) -> t1
    apply(op,v1,v2) ->
      apply[Ite](eqExp(v1,v2)
                ,op
                ,v1
                ,v2)
    lookvar(x',Cons(x,xs),vs) ->
      lookvar[Ite](!EQ(x',x)
                  ,x'
                  ,Cons(x,xs)
                  ,vs)
    eqOps(o1,o2) -> True()
    !EQ(S(x),S(y)) ->= !EQ(x,y)
    !EQ(0(),S(y)) ->= False()
    !EQ(S(x),0()) ->= False()
    !EQ(0(),0()) ->= True()
    and(False(),False()) ->= False()
    and(True(),False()) ->= False()
    and(False(),True()) ->= False()
    and(True(),True()) ->= True()
    eeval[False][Ite](True()
                     ,Eq(f,s)
                     ,ns
                     ,vs
                     ,p) ->=
      eeval[True][Ite](eqExp(eeval(f
                                  ,ns
                                  ,vs
                                  ,p)
                            ,eeval(s,ns,vs,p))
                      ,Eq(f,s)
                      ,ns
                      ,vs
                      ,p)
    lookvar[Ite](False()
                ,x'
                ,Cons(x'',xs')
                ,Cons(x,xs)) ->= lookvar(x'
                                        ,xs'
                                        ,xs)
    lookname[Ite](True()
                 ,f
                 ,Cons(Fun(n,e),xs)) ->= n
    lookbody[Ite](True()
                 ,f
                 ,Cons(Fun(n,e),xs)) ->= e
    eeval[False][Ite](False()
                     ,Fun(n,e)
                     ,ns
                     ,vs
                     ,p) ->= eeval[False][Let](Fun(n
                                                  ,e)
                                              ,ns
                                              ,vs
                                              ,p
                                              ,lookbody(n,p))
    eeval[Ite](False()
              ,ITE(i,t,e)
              ,ns
              ,vs
              ,p) ->= eeval(e,ns,vs,p)
    eeval[Ite](True()
              ,ITE(i,t,e)
              ,ns
              ,vs
              ,p) ->= eeval(t,ns,vs,p)
    eeval[False][Let](Fun(n,e)
                     ,ns
                     ,vs
                     ,p
                     ,ef) ->=
      eeval[False][Let][Let](Fun(n,e)
                            ,ns
                            ,vs
                            ,p
                            ,ef
                            ,lookname(n,p))
    eeval[False][Let][Let](Fun(n,e)
                          ,ns
                          ,vs
                          ,p
                          ,ef
                          ,nf) ->=
      eeval[Let][Let][Let](Fun(n,e)
                          ,ns
                          ,vs
                          ,p
                          ,ef
                          ,nf
                          ,eeval(e,ns,vs,p))
    eeval[Let](Bsf(op,t1,t2)
              ,ns
              ,vs
              ,p
              ,v1) ->= eeval[Let][Let](Bsf(op
                                          ,t1
                                          ,t2)
                                      ,ns
                                      ,vs
                                      ,p
                                      ,v1
                                      ,eeval(t2,ns,vs,p))
    eeval[Let][Let](Bsf(op,t1,t2)
                   ,ns
                   ,vs
                   ,p
                   ,v1
                   ,v2) ->= apply(op,v1,v2)
    lookvar[Ite](True()
                ,x'
                ,ns
                ,Cons(x,xs)) ->= x
    lookname[Ite](False()
                 ,f
                 ,Cons(x,xs)) ->= lookname(f,xs)
    lookbody[Ite](False()
                 ,f
                 ,Cons(x,xs)) ->= lookbody(f,xs)
    eeval[True][Ite](False()
                    ,e
                    ,ns
                    ,vs
                    ,p) ->= F()
    eeval[True][Ite](True()
                    ,e
                    ,ns
                    ,vs
                    ,p) ->= T()
    apply[Ite](False(),op,v1,v2) ->=
      F()
    apply[Ite](True(),op,v1,v2) ->=
      T()
    run[Let][Let](p,input,f0,ef) ->=
      run[Let](p
              ,input
              ,f0
              ,ef
              ,lookname(f0,p))
    run[Let](p,input,f0,ef,nf) ->=
      eeval(ef
           ,Cons(nf,Nil())
           ,Cons(input,Nil())
           ,p)
    eeval[Let][Let][Let](e
                        ,ns
                        ,vs
                        ,p
                        ,ef
                        ,nf
                        ,v) ->= eeval(ef
                                     ,Cons(nf,Nil())
                                     ,Cons(v,Nil())
                                     ,p))