(STRATEGY
    INNERMOST)

(VAR
    M N X)
(DATATYPES
    A = µX.< tt, s(X), 0 >)
(SIGNATURES
    U11 :: [A x A x A] -> A
    U12 :: [A x A x A] -> A
    U21 :: [A x A x A] -> A
    U22 :: [A x A x A] -> A
    plus :: [A x A] -> A
    x :: [A x A] -> A
    activate :: [A] -> A)
(RULES
    U11(tt(),M,N) -> U12(tt()
                        ,activate(M)
                        ,activate(N))
    U12(tt(),M,N) ->
      s(plus(activate(N),activate(M)))
    U21(tt(),M,N) -> U22(tt()
                        ,activate(M)
                        ,activate(N))
    U22(tt(),M,N) ->
      plus(x(activate(N),activate(M))
          ,activate(N))
    plus(N,0()) -> N
    plus(N,s(M)) -> U11(tt(),M,N)
    x(N,0()) -> 0()
    x(N,s(M)) -> U21(tt(),M,N)
    activate(X) -> X)