(STRATEGY
    INNERMOST)

(VAR
    a1 b1 c1 exp n opab x y y')
(DATATYPES
    A = µX.< Op(X, X), Val(X), False, True >)
(SIGNATURES
    rewrite :: [A] -> A
    second :: [A] -> A
    isOp :: [A] -> A
    first :: [A] -> A
    assrewrite :: [A] -> A
    rewrite[Let] :: [A x A x A] -> A
    rewrite[Let][Let] :: [A x A x A x A] -> A
    rewrite[Let][Let][Let] :: [A x A x A x A] -> A)
(RULES
    rewrite(Op(Val(n),y)) ->
      Op(rewrite(y),Val(n))
    rewrite(Op(Op(x,y),y')) ->
      rewrite[Let](Op(Op(x,y),y')
                  ,Op(x,y)
                  ,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)
    rewrite[Let](exp,Op(x,y),a1) ->=
      rewrite[Let][Let](exp
                       ,Op(x,y)
                       ,a1
                       ,rewrite(y))
    rewrite[Let][Let](Op(x,y)
                     ,opab
                     ,a1
                     ,b1) ->=
      rewrite[Let][Let][Let](Op(x,y)
                            ,a1
                            ,b1
                            ,rewrite(y))
    rewrite[Let][Let][Let](exp
                          ,a1
                          ,b1
                          ,c1) ->= rewrite(Op(a1
                                             ,Op(b1,rewrite(c1)))))