(VAR
    l l1 l2 n x xs y)

(DATATYPES a = µX. < dd(X,X), nil, #0, #s(X), #neg(X), #pos(X) >
 )

(SIGNATURES
   #mult :: 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
   #pred :: a -> a
   #succ :: a -> a
   #natmult :: a x a -> a
   #natadd :: a x a -> a
 )

(RULES
    mult(x,y) -> #mult(x,y)
    dyade(l1,l2) -> dyade#1(l1,l2)
    dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2))
    dyade#1(nil,l2) -> nil
    mult(n,l) -> mult#1(l,n)
    mult#1(dd(x,xs),n) -> dd(mult(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))
    #natadd(#0,y) -> y
    #natadd(#s(x),y) -> #s(#natadd(x,y))
    #natmult(#0,y) -> #0
    #natmult(#s(x),y) -> #natadd(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))))