(STRATEGY
    INNERMOST)

(VAR
    @l @l1 @l2 @n @x @xs @y)
(DATATYPES
    A = µX.< ::(X, X), nil, #0, #neg(X), #s(X), #pos(X) >)
(SIGNATURES
    * :: [A x A] -> A
    dyade :: [A x A] -> A
    dyade#1 :: [A x A] -> A
    mult :: [A x A] -> A
    mult#1 :: [A x A] -> A
    #add :: [A x A] -> A
    #mult :: [A x A] -> A
    #natmult :: [A x A] -> A
    #pred :: [A] -> A
    #succ :: [A] -> A)
(RULES
    *(@x,@y) -> #mult(@x,@y)
    dyade(@l1,@l2) -> dyade#1(@l1
                             ,@l2)
    dyade#1(::(@x,@xs),@l2) ->
      ::(mult(@x,@l2),dyade(@xs,@l2))
    dyade#1(nil(),@l2) -> nil()
    mult(@n,@l) -> mult#1(@l,@n)
    mult#1(::(@x,@xs),@n) -> ::(*(@n
                                 ,@x)
                               ,mult(@n,@xs))
    mult#1(nil(),@n) -> nil()
    #add(#0(),@y) ->= @y
    #add(#neg(#s(#0())),@y) ->=
      #pred(@y)
    #add(#neg(#s(#s(@x))),@y) ->=
      #pred(#add(#pos(#s(@x)),@y))
    #add(#pos(#s(#0())),@y) ->=
      #succ(@y)
    #add(#pos(#s(#s(@x))),@y) ->=
      #succ(#add(#pos(#s(@x)),@y))
    #mult(#0(),#0()) ->= #0()
    #mult(#0(),#neg(@y)) ->= #0()
    #mult(#0(),#pos(@y)) ->= #0()
    #mult(#neg(@x),#0()) ->= #0()
    #mult(#neg(@x),#neg(@y)) ->=
      #pos(#natmult(@x,@y))
    #mult(#neg(@x),#pos(@y)) ->=
      #neg(#natmult(@x,@y))
    #mult(#pos(@x),#0()) ->= #0()
    #mult(#pos(@x),#neg(@y)) ->=
      #neg(#natmult(@x,@y))
    #mult(#pos(@x),#pos(@y)) ->=
      #pos(#natmult(@x,@y))
    #natmult(#0(),@y) ->= #0()
    #natmult(#s(@x),@y) ->=
      #add(#pos(@y),#natmult(@x,@y))
    #pred(#0()) ->= #neg(#s(#0()))
    #pred(#neg(#s(@x))) ->=
      #neg(#s(#s(@x)))
    #pred(#pos(#s(#0()))) ->= #0()
    #pred(#pos(#s(#s(@x)))) ->=
      #pos(#s(@x))
    #succ(#0()) ->= #pos(#s(#0()))
    #succ(#neg(#s(#0()))) ->= #0()
    #succ(#neg(#s(#s(@x)))) ->=
      #neg(#s(@x))
    #succ(#pos(#s(@x))) ->=
      #pos(#s(#s(@x))))