(STRATEGY
    INNERMOST)

(VAR
    dummy dummy2 x y z)
(DATATYPES
    A = µX.< iszero, 0, true, s(X), false, p, plus, if, third >)
(SIGNATURES
    function :: [A x A x A x A] -> A)
(RULES
    function(iszero()
            ,0()
            ,dummy
            ,dummy2) -> true()
    function(iszero()
            ,s(x)
            ,dummy
            ,dummy2) -> false()
    function(p()
            ,0()
            ,dummy
            ,dummy2) -> 0()
    function(p()
            ,s(0())
            ,dummy
            ,dummy2) -> 0()
    function(p()
            ,s(s(x))
            ,dummy
            ,dummy2) -> s(function(p()
                                  ,s(x)
                                  ,x
                                  ,x))
    function(plus(),dummy,x,y) ->
      function(if()
              ,function(iszero(),x,x,x)
              ,x
              ,y)
    function(if(),true(),x,y) -> y
    function(if(),false(),x,y) ->
      function(plus()
              ,function(third(),x,y,y)
              ,function(p(),x,x,y)
              ,s(y))
    function(third(),x,y,z) -> z)