(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 )
(STRATEGY INNERMOST)
(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)
)