(VAR
    l p x x'1 x'2 xs xs' y y'1 y'2 z)

(DATATYPES
   a = < 'true, 'false >
   b = µX. < dd(X,X),
             nil,
             '0,
             's(X),
             'neg(X),
             'pos(X),
             'divByZero,
             'underflow >
 )

(SIGNATURES
   'equal :: b x b -> a
   'eq :: b x b -> a
   eratos :: b -> b
   filter :: b x b -> b
   'mod :: b x b -> b
   filter' :: a x b x b -> b
   'div :: b x b -> b
   'mult :: b x b -> b
   'sub :: b x b -> b
   'add :: b x b -> b
   'pred :: b -> b
   'succ :: b -> b
   'and :: a x a -> a
   'natdiv :: b x b -> b
   'positive :: b -> b
   'negative :: b -> b
   'natmult :: b x b -> b
   'divsub :: b x b -> b
   'natdiv' :: b x b -> b
   'natadd :: b x b -> b
   'natsub :: b x b -> b
 )

(RULES
    'equal(x,y) -> 'eq(x,y)
    eratos(dd(x,xs)) -> dd(x,eratos(filter(x,xs)))
    eratos(nil) -> nil
    filter(p,nil) -> nil
    filter(p,dd(x,xs)) -> filter'('equal('mod(x,p),'0), x, filter(p,xs))
    filter'('true,x,xs) -> xs
    filter'('false,x,xs) -> dd(x,xs)

    'mod(x,y) -> 'sub(x,'mult(y,'div(x,y)))
    '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))
    'and('false,'false) -> 'false
    'and('false,'true) -> 'false
    'and('true,'false) -> 'false
    'and('true,'true) -> 'true
    'div('0,'0) -> 'divByZero
    'div('0,'neg(y)) -> '0
    'div('0,'pos(y)) -> '0
    'div('neg(x),'0) -> 'divByZero
    'div('neg(x),'neg(y)) -> 'positive('natdiv(x,y))
    'div('neg(x),'pos(y)) -> 'negative('natdiv(x,y))
    'div('pos(x),'0) -> 'divByZero
    'div('pos(x),'neg(y)) -> 'negative('natdiv(x,y))
    'div('pos(x),'pos(y)) -> 'positive('natdiv(x,y))
    'positive('0) -> '0
    'positive('s(x)) -> 'pos('s(x))
    'positive('pos(x)) -> 'pos(x)
    'positive('neg(x)) -> 'neg(x)
    'negative('0) -> '0
    'negative('s(x)) -> 'neg('s(x))
    'negative('pos(x)) -> 'neg(x)
    'negative('neg(x)) -> 'pos(x)
    'eq('0,'0) -> 'true
    'eq('0,'neg(y)) -> 'false
    'eq('0,'pos(y)) -> 'false
    'eq('0,'s(y)) -> 'false
    'eq('neg(x),'0) -> 'false
    'eq('neg(x),'neg(y)) -> 'eq(x,y)
    'eq('neg(x),'pos(y)) -> 'false
    'eq('pos(x),'0) -> 'false
    'eq('pos(x),'neg(y)) -> 'false
    'eq('pos(x),'pos(y)) -> 'eq(x,y)
    'eq('s(x),'0) -> 'false
    'eq('s(x),'s(y)) -> 'eq(x,y)
    'eq(dd(x'1,x'2),dd(y'1,y'2)) -> 'and('eq(x'1,y'1),'eq(x'2,y'2))
    'eq(dd(x'1,x'2),nil) -> 'false
    'eq(nil,dd(y'1,y'2)) -> 'false
    'eq(nil,nil) -> 'true
    '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))
    'natdiv('0,'0) -> 'divByZero
    'natdiv('0,'s(y)) -> '0
    'natdiv('s(x),'0) -> 'divByZero
    'natdiv('s(x),'s(y)) -> 'natdiv'('divsub(x,y),'s(y))
    'natdiv'('underflow,y) -> '0
    'natdiv'('0,y) -> 's('0)
    'natdiv'('s(x),y) -> 's('natdiv('s(x),y))
    'natdiv('underflow,y) -> '0
    'divsub('0,'0) -> '0
    'divsub('0,'s(y)) -> 'underflow
    'divsub('s(x),'0) -> 's(x)
    'divsub('s(x),'s(y)) -> 'divsub(x,y)
    'natmult('0,y) -> '0
    'natmult('s(x),y) -> 'natadd(y,'natmult(x,y))
    'natadd('0,y) -> y
    'natadd('s(x),y) -> 's('natadd(x,y))
    'natsub('0,'0) -> '0
    'natsub('0,'s(y)) -> '0
    'natsub('s(x),'0) -> 's(x)
    'natsub('s(x),'s(y)) -> 'natsub(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))
    'sub(x,'0) -> x
    'sub(x,'neg(y)) -> 'add(x,'pos(y))
    'sub(x,'pos(y)) -> 'add(x,'neg(y))
    '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)))
)