(STRATEGY
    INNERMOST)

(VAR
    m n)
(DATATYPES
    A = µX.< 0, ack_out(X), s(X) >)
(SIGNATURES
    ack_in :: [A x A] -> A
    u11 :: [A] -> A
    u21 :: [A x A] -> A
    u22 :: [A] -> A)
(RULES
    ack_in(0(),n) -> ack_out(s(n))
    ack_in(s(m),0()) -> u11(ack_in(m
                                  ,s(0())))
    u11(ack_out(n)) -> ack_out(n)
    ack_in(s(m),s(n)) ->
      u21(ack_in(s(m),n),m)
    u21(ack_out(n),m) ->
      u22(ack_in(m,n))
    u22(ack_out(n)) -> ack_out(n))