(VAR
    '1 b b1 b2 b3 n r r' s x x'1 x'2 xs y y'1 y'2 ys z zs)

(DATATYPES
   a = < 'EQ, 'GT, 'LT >
   c = < 'false, 'true >
   d = µX. < '0,
             'neg(X),
             'pos(X),
             's(X),
             dd(X,X),
             nil,
             tuple'2(X,X),
             'divByZero,
             'underflow >
 )

(SIGNATURES
   'abs :: d -> d
   'equal :: d x d -> c
   'eq :: d x d -> c
   'greater :: d x d -> c
   'compare :: d x d -> a
   'ckgt :: a -> c
   'less :: d x d -> c
   'cklt :: a -> c
   'sub :: d x d -> d
   add :: d x d -> d
   'add :: d x d -> d
   add' :: d x d x d -> d
   add''1 :: d x d x d -> d
   add''2 :: d x d x d x d -> d
   sum :: d x d x d -> d
   add''3 :: d x d x d -> d
   bitToInt :: d -> d
   bitToInt' :: d x d -> d
   bitToInt''1 :: d x d -> d
   compare :: d x d -> d
   compare'1 :: d x d -> d
   compare'2 :: d x d x d -> d
   compare'3 :: d x d x d -> d
   compare'4 :: c x d x d x d -> d
   compare'5 :: c x d x d -> d
   compare'6 :: c -> d
   diff :: d x d x d -> d
   mod :: d x d -> d
   diff'1 :: c -> d
   div :: d x d -> d
   'div :: d x d -> d
   leq :: d x d -> c
   mult :: d x d -> d
   'mult :: d x d -> d
   mult'1 :: d x d -> d
   mult'2 :: d x d x d -> d
   mult'3 :: c x d x d -> d
   mult3 :: d x d x d -> d
   sub :: d x d -> d
   sub' :: d x d x d -> d
   sub'1 :: d -> d
   sub''1 :: d x d x d -> d
   sub''2 :: d x d x d x d -> d
   sub''3 :: d x d x d -> d
   sub''4 :: d x d -> d
   sub''5 :: c x d x d -> d
   sum'1 :: d -> d
   sum'2 :: c x d -> d
   sum'3 :: c x d -> d
   sum'4 :: c -> d
   'pred :: d -> d
   'succ :: d -> d
   'and :: c x c -> c
   'natdiv :: d x d -> d
   'positive :: d -> d
   'negative :: d -> d
   'divsub :: d x d -> d
   'natmult :: d x d -> d
   'natadd :: d x d -> d
   'natdiv' :: d x d -> d
   'natsub :: d x d -> d
 )

(RULES
    'abs('0) -> '0
    'abs('neg(x)) -> 'pos(x)
    'abs('pos(x)) -> 'pos(x)
    'abs('s(x)) -> 'pos('s(x))
    'equal(x,y) -> 'eq(x,y)
    'greater(x,y) -> 'ckgt('compare(x,y))
    'less(x,y) -> 'cklt('compare(x,y))
    mult(x,y) -> 'mult(x,y)
    add(x,y) -> 'add(x,y)
    sub(x,y) -> 'sub(x,y)
    add(b1,b2) -> add'(b1,b2,'abs('0))
    add'(b1,b2,r) -> add''1(b1,b2,r)
    add''1(dd(x,xs),b2,r) -> add''2(b2,r,x,xs)
    add''1(nil,b2,r) -> nil
    add''2(dd(y,ys),r,x,xs) -> add''3(sum(x,y,r),xs,ys)
    add''2(nil,r,x,xs) -> nil
    add''3(tuple'2(z,r'),xs,ys) -> dd(z,add'(xs,ys,r'))
    bitToInt(b) -> bitToInt'(b,'abs('pos('s('0))))
    bitToInt'(b,n) -> bitToInt''1(b,n)
    bitToInt''1(dd(x,xs),n) -> add(mult(x,n),bitToInt'(xs,mult(n,'pos('s('s('0))))))
    bitToInt''1(nil,n) -> 'abs('0)
    compare(b1,b2) -> compare'1(b1,b2)
    compare'1(dd(x,xs),b2) -> compare'2(b2,x,xs)
    compare'1(nil,b2) -> 'abs('0)
    compare'2(dd(y,ys),x,xs) -> compare'3(compare(xs,ys),x,y)
    compare'2(nil,x,xs) -> 'abs('0)
    compare'3(r,x,y) -> compare'4('equal(r,'0),r,x,y)
    compare'4('false,r,x,y) -> r
    compare'4('true,r,x,y) -> compare'5('less(x,y),x,y)
    compare'5('false,x,y) -> compare'6('greater(x,y))
    compare'5('true,x,y) -> sub('0,'pos('s('0)))
    compare'6('false) -> 'abs('0)
    compare'6('true) -> 'abs('pos('s('0)))
    diff(x,y,r) -> tuple'2(mod(add(add(x,y),r),'pos('s('s('0)))),diff'1('less(sub(sub(x,y),r),'0)))
    diff'1('false) -> 'abs('0)
    diff'1('true) -> 'abs('pos('s('0)))
    div(x,y) -> 'div(x,y)
    leq(b1,b2) -> 'less(compare(b1,b2),'pos('s('0)))
    mod(x,y) -> sub(x,mult(y,div(x,y)))
    mult(b1,b2) -> mult'1(b1,b2)
    mult'1(dd(x,xs),b2) -> mult'2(dd('abs('0),mult(xs,b2)),b2,x)
    mult'1(nil,b2) -> nil
    mult'2(zs,b2,x) -> mult'3('equal(x,'pos('s('0))),b2,zs)
    mult'3('false,b2,zs) -> zs
    mult'3('true,b2,zs) -> add(b2,zs)
    mult3(b1,b2,b3) -> mult(mult(b1,b2),b2)
    sub(b1,b2) -> sub'1(sub'(b1,b2,'abs('0)))
    sub'1(tuple'2(b,'1)) -> b
    sub'(b1,b2,r) -> sub''1(b1,b2,r)
    sub''1(dd(x,xs),b2,r) -> sub''2(b2,r,x,xs)
    sub''1(nil,b2,r) -> tuple'2(nil,r)
    sub''2(dd(y,ys),r,x,xs) -> sub''3(diff(x,y,r),xs,ys)
    sub''2(nil,r,x,xs) -> tuple'2(nil,r)
    sub''3(tuple'2(z,r'),xs,ys) -> sub''4(sub'(xs,ys,r'),z)
    sub''4(tuple'2(zs,s),z) -> tuple'2(sub''5('equal(s,'pos('s('0))),z,zs),s)
    sub''5('false,z,zs) -> dd(z,zs)
    sub''5('true,z,zs) -> dd('abs('0),zs)
    sum(x,y,r) -> sum'1(add(add(x,y),r))
    sum'1(s) -> sum'2('equal(s,'0),s)
    sum'2('false,s) -> sum'3('equal(s,'pos('s('0))),s)
    sum'2('true,s) -> tuple'2('abs('0),'abs('0))
    sum'3('false,s) -> sum'4('equal(s,'pos('s('s('0)))))
    sum'3('true,s) -> tuple'2('abs('pos('s('0))),'abs('0))
    sum'4('false) -> tuple'2('abs('pos('s('0))),'abs('pos('s('0))))
    sum'4('true) -> tuple'2('abs('0),'abs('pos('s('0))))
    '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
    'ckgt('EQ) -> 'false
    'ckgt('GT) -> 'true
    'ckgt('LT) -> 'false
    'cklt('EQ) -> 'false
    'cklt('GT) -> 'false
    'cklt('LT) -> 'true
    'compare('0,'0) -> 'EQ
    'compare('0,'neg(y)) -> 'GT
    'compare('0,'pos(y)) -> 'LT
    'compare('0,'s(y)) -> 'LT
    'compare('neg(x),'0) -> 'LT
    'compare('neg(x),'neg(y)) -> 'compare(y,x)
    'compare('neg(x),'pos(y)) -> 'LT
    'compare('pos(x),'0) -> 'GT
    'compare('pos(x),'neg(y)) -> 'GT
    'compare('pos(x),'pos(y)) -> 'compare(x,y)
    'compare('s(x),'0) -> 'GT
    'compare('s(x),'s(y)) -> 'compare(x,y)
    '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))
    'divsub('0,'0) -> '0
    'divsub('0,'s(y)) -> 'underflow
    'divsub('s(x),'0) -> 's(x)
    'divsub('s(x),'s(y)) -> 'divsub(x,y)
    '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(dd(x'1,x'2),tuple'2(y'1,y'2)) -> 'false
    'eq(nil,dd(y'1,y'2)) -> 'false
    'eq(nil,nil) -> 'true
    'eq(nil,tuple'2(y'1,y'2)) -> 'false
    'eq(tuple'2(x'1,x'2),dd(y'1,y'2)) -> 'false
    'eq(tuple'2(x'1,x'2),nil) -> 'false
    'eq(tuple'2(x'1,x'2),tuple'2(y'1,y'2)) -> 'and('eq(x'1,y'1),'eq(x'2,y'2))
    '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))
    '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'('0,y) -> 's('0)
    'natdiv'('s(x),y) -> 's('natdiv('s(x),y))
    'natdiv'('underflow,y) -> '0
    'natmult('0,y) -> '0
    'natmult('s(x),y) -> 'natadd(y,'natmult(x,y))
    'natsub(x,'0) -> x
    'natsub('s(x),'s(y)) -> 'natsub(x,y)
    'negative('0) -> '0
    'negative('neg(x)) -> 'pos(x)
    'negative('pos(x)) -> 'neg(x)
    'negative('s(x)) -> 'neg('s(x))
    'positive('0) -> '0
    'positive('neg(x)) -> 'neg(x)
    'positive('pos(x)) -> 'pos(x)
    'positive('s(x)) -> 'pos('s(x))
    '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))))