(STRATEGY
    INNERMOST)

(VAR
    a1 ab b1 c c1 exp n x y)
(DATATYPES
    A = µX.< Val(X), Op(X, X), False, True >)
(SIGNATURES
    rw :: [A x A] -> A
    rewrite :: [A] -> A
    second :: [A] -> A
    isOp :: [A] -> A
    first :: [A] -> A
    assrewrite :: [A] -> A
    rw[Let] :: [A x A x A] -> A
    rw[Let][Let] :: [A x A x A x A] -> A
    rw[Let][Let][Let] :: [A x A x A x A] -> A)
(RULES
    rw(Val(n),c) -> Op(Val(n)
                      ,rewrite(c))
    rewrite(Op(x,y)) -> rw(x,y)
    rw(Op(x,y),c) -> rw[Let](Op(x,y)
                            ,c
                            ,rewrite(x))
    rewrite(Val(n)) -> Val(n)
    second(Op(x,y)) -> y
    isOp(Val(n)) -> False()
    isOp(Op(x,y)) -> True()
    first(Val(n)) -> Val(n)
    first(Op(x,y)) -> x
    assrewrite(exp) -> rewrite(exp)
    rw[Let](Op(x,y),c,a1) ->=
      rw[Let][Let](Op(x,y)
                  ,c
                  ,a1
                  ,rewrite(y))
    rw[Let][Let](ab,c,a1,b1) ->=
      rw[Let][Let][Let](c
                       ,a1
                       ,b1
                       ,rewrite(c))
    rw[Let][Let][Let](c
                     ,a1
                     ,b1
                     ,c1) ->= rw(a1,Op(b1,c1)))