(STRATEGY
    INNERMOST)

(VAR
    int int2 x x' xs xs' y)
(DATATYPES
    A = µX.< Cons(X, X), RPar, Div, Mul, Plus, Minus, Val(X), LPar, Nil, False, True, S(X), 0, factor[Ite][True][Let][Ite](X, X, X), term[Let][Ite][False][Ite](X, X, X), expr[Let][Ite][False][Ite](X, X, X) >)
(SIGNATURES
    head :: [A] -> A
    factor :: [A] -> A
    member :: [A x A] -> A
    atom :: [A] -> A
    eqAlph :: [A x A] -> A
    notEmpty :: [A] -> A
    term :: [A] -> A
    parsexp :: [A] -> A
    expr :: [A] -> A
    and :: [A x A] -> A
    !EQ :: [A x A] -> A
    factor[Ite][True][Let] :: [A x A] -> A
    term[Let] :: [A x A] -> A
    expr[Let] :: [A x A] -> A
    member[Ite][True][Ite] :: [A x A x A] -> A)
(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())