(VAR int int2 x x' xs xs' y )
(STRATEGY INNERMOST)
(RULES 
        head(Cons(x,xs)) -> x
        factor(Cons(RPar,xs)) -> xs
        factor(Cons(Div,xs)) -> xs
        factor(Cons(Mul,xs)) -> xs
        factor(Cons(Plus,xs)) -> xs
        factor(Cons(Minus,xs)) -> xs
        factor(Cons(Val(int),xs)) -> xs
        factor(Cons(LPar,xs)) -> factor[Ite][True][Let](Cons(LPar,xs),expr(Cons(LPar,xs)))
        member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs))
        member(x,Nil) -> False
        atom(Cons(x,xs)) -> xs
        atom(Nil) -> Nil
        eqAlph(RPar,RPar) -> True
        eqAlph(RPar,LPar) -> False
        eqAlph(RPar,Div) -> False
        eqAlph(RPar,Mul) -> False
        eqAlph(RPar,Plus) -> False
        eqAlph(RPar,Minus) -> False
        eqAlph(RPar,Val(int2)) -> False
        eqAlph(LPar,RPar) -> False
        eqAlph(LPar,LPar) -> True
        eqAlph(LPar,Div) -> False
        eqAlph(LPar,Mul) -> False
        eqAlph(LPar,Plus) -> False
        eqAlph(LPar,Minus) -> False
        eqAlph(LPar,Val(int2)) -> False
        eqAlph(Div,RPar) -> False
        eqAlph(Div,LPar) -> False
        eqAlph(Div,Div) -> True
        eqAlph(Div,Mul) -> False
        eqAlph(Div,Plus) -> False
        eqAlph(Div,Minus) -> False
        eqAlph(Div,Val(int2)) -> False
        eqAlph(Mul,RPar) -> False
        eqAlph(Mul,LPar) -> False
        eqAlph(Mul,Div) -> False
        eqAlph(Mul,Mul) -> True
        eqAlph(Mul,Plus) -> False
        eqAlph(Mul,Minus) -> False
        eqAlph(Mul,Val(int2)) -> False
        eqAlph(Plus,RPar) -> False
        eqAlph(Plus,LPar) -> False
        eqAlph(Plus,Div) -> False
        eqAlph(Plus,Mul) -> False
        eqAlph(Plus,Plus) -> True
        eqAlph(Plus,Minus) -> False
        eqAlph(Plus,Val(int2)) -> False
        eqAlph(Minus,RPar) -> False
        eqAlph(Minus,LPar) -> False
        eqAlph(Minus,Div) -> False
        eqAlph(Minus,Mul) -> False
        eqAlph(Minus,Plus) -> False
        eqAlph(Minus,Minus) -> True
        eqAlph(Minus,Val(int2)) -> False
        eqAlph(Val(int),RPar) -> False
        eqAlph(Val(int),LPar) -> False
        eqAlph(Val(int),Div) -> False
        eqAlph(Val(int),Mul) -> False
        eqAlph(Val(int),Plus) -> False
        eqAlph(Val(int),Minus) -> False
        eqAlph(Val(int),Val(int2)) -> !EQ(int2,int)
        notEmpty(Cons(x,xs)) -> True
        notEmpty(Nil) -> False
        term(xs) -> term[Let](xs,factor(xs))
        parsexp(xs) -> expr(xs)
        expr(xs) -> expr[Let](xs,term(xs))
        and(False,False) ->= False
        and(True,False) ->= False
        and(False,True) ->= False
        and(True,True) ->= True
        !EQ(S(x),S(y)) ->= !EQ(x,y)
        !EQ(0,S(y)) ->= False
        !EQ(S(x),0) ->= False
        !EQ(0,0) ->= True
        factor[Ite][True][Let](xs',Cons(RPar,xs)) ->= factor[Ite][True][Let][Ite](True,xs',Cons(RPar,xs))
        factor[Ite][True][Let](xs',Cons(LPar,xs)) ->= factor[Ite][True][Let][Ite](False,xs',Cons(LPar,xs))
        factor[Ite][True][Let](xs',Cons(Div,xs)) ->= factor[Ite][True][Let][Ite](False,xs',Cons(Div,xs))
        factor[Ite][True][Let](xs',Cons(Mul,xs)) ->= factor[Ite][True][Let][Ite](False,xs',Cons(Mul,xs))
        factor[Ite][True][Let](xs',Cons(Plus,xs)) ->= factor[Ite][True][Let][Ite](False,xs',Cons(Plus,xs))
        factor[Ite][True][Let](xs',Cons(Minus,xs)) ->= factor[Ite][True][Let][Ite](False,xs',Cons(Minus,xs))
        factor[Ite][True][Let](xs',Cons(Val(int),xs)) ->= factor[Ite][True][Let][Ite](False,xs',Cons(Val(int),xs))
        term[Let](xs',Cons(x,xs)) ->= term[Let][Ite][False][Ite](member(x,Cons(Mul,Cons(Div,Nil))),xs',Cons(x,xs))
        expr[Let](xs',Cons(x,xs)) ->= expr[Let][Ite][False][Ite](member(x,Cons(Plus,Cons(Minus,Nil))),xs',Cons(x,xs))
        term[Let](xs,Nil) ->= Nil
        member[Ite][True][Ite](False,x',Cons(x,xs)) ->= member(x',xs)
        factor[Ite][True][Let](xs,Nil) ->= factor[Ite][True][Let][Ite](and(False,eqAlph(head(Nil),RPar)),xs,Nil)
        expr[Let](xs,Nil) ->= Nil
        member[Ite][True][Ite](True,x,xs) ->= True
)