(STRATEGY
    INNERMOST)

(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 = µX.< #0, #neg(X), #pos(X), #s(X), ::(X, X), nil, tuple#2(X, X), #false, #true, #EQ, #GT, #LT, #divByZero >)
(SIGNATURES
    #abs :: [A] -> A
    #equal :: [A x A] -> A
    #greater :: [A x A] -> A
    #less :: [A x A] -> A
    * :: [A x A] -> A
    + :: [A x A] -> A
    - :: [A x A] -> A
    add :: [A x A] -> A
    add' :: [A x A x A] -> A
    add'#1 :: [A x A x A] -> A
    add'#2 :: [A x A x A x A] -> A
    add'#3 :: [A x A x A] -> A
    bitToInt :: [A] -> A
    bitToInt' :: [A x A] -> A
    bitToInt'#1 :: [A x A] -> A
    compare :: [A x A] -> A
    compare#1 :: [A x A] -> A
    compare#2 :: [A x A x A] -> A
    compare#3 :: [A x A x A] -> A
    compare#4 :: [A x A x A x A] -> A
    compare#5 :: [A x A x A] -> A
    compare#6 :: [A] -> A
    diff :: [A x A x A] -> A
    diff#1 :: [A] -> A
    div :: [A x A] -> A
    leq :: [A x A] -> A
    mod :: [A x A] -> A
    mult :: [A x A] -> A
    mult#1 :: [A x A] -> A
    mult#2 :: [A x A x A] -> A
    mult#3 :: [A x A x A] -> A
    mult3 :: [A x A x A] -> A
    sub :: [A x A] -> A
    sub#1 :: [A] -> A
    sub' :: [A x A x A] -> A
    sub'#1 :: [A x A x A] -> A
    sub'#2 :: [A x A x A x A] -> A
    sub'#3 :: [A x A x A] -> A
    sub'#4 :: [A x A] -> A
    sub'#5 :: [A x A x A] -> A
    sum :: [A x A x A] -> A
    sum#1 :: [A] -> A
    sum#2 :: [A x A] -> A
    sum#3 :: [A x A] -> A
    sum#4 :: [A] -> A
    #add :: [A x A] -> A
    #and :: [A x A] -> A
    #ckgt :: [A] -> A
    #cklt :: [A] -> A
    #compare :: [A x A] -> A
    #div :: [A x A] -> A
    #eq :: [A x A] -> A
    #mult :: [A x A] -> A
    #natdiv :: [A x A] -> A
    #natmult :: [A x A] -> A
    #natsub :: [A x A] -> A
    #pred :: [A] -> A
    #sub :: [A x A] -> A
    #succ :: [A] -> A)
(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))
    *(@x,@y) -> #mult(@x,@y)
    +(@x,@y) -> #add(@x,@y)
    -(@x,@y) -> #sub(@x,@y)
    add(@b1,@b2) -> add'(@b1
                        ,@b2
                        ,#abs(#0()))
    add'(@b1,@b2,@r) -> add'#1(@b1
                              ,@b2
                              ,@r)
    add'#1(::(@x,@xs),@b2,@r) ->
      add'#2(@b2,@r,@x,@xs)
    add'#1(nil(),@b2,@r) -> nil()
    add'#2(::(@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) -> ::(@z
                     ,add'(@xs,@ys,@r'))
    bitToInt(@b) -> bitToInt'(@b
                             ,#abs(#pos(#s(#0()))))
    bitToInt'(@b,@n) ->
      bitToInt'#1(@b,@n)
    bitToInt'#1(::(@x,@xs),@n) ->
      +(*(@x,@n)
       ,bitToInt'(@xs
                 ,*(@n,#pos(#s(#s(#0()))))))
    bitToInt'#1(nil(),@n) ->
      #abs(#0())
    compare(@b1,@b2) ->
      compare#1(@b1,@b2)
    compare#1(::(@x,@xs),@b2) ->
      compare#2(@b2,@x,@xs)
    compare#1(nil(),@b2) ->
      #abs(#0())
    compare#2(::(@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) ->
      -(#0(),#pos(#s(#0())))
    compare#6(#false()) ->
      #abs(#0())
    compare#6(#true()) ->
      #abs(#pos(#s(#0())))
    diff(@x,@y,@r) ->
      tuple#2(mod(+(+(@x,@y),@r)
                 ,#pos(#s(#s(#0()))))
             ,diff#1(#less(-(-(@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) -> -(@x
                   ,*(@x,div(@x,@y)))
    mult(@b1,@b2) -> mult#1(@b1,@b2)
    mult#1(::(@x,@xs),@b2) ->
      mult#2(::(#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(::(@x,@xs),@b2,@r) ->
      sub'#2(@b2,@r,@x,@xs)
    sub'#1(nil(),@b2,@r) ->
      tuple#2(nil(),@r)
    sub'#2(::(@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) -> ::(@z
                                 ,@zs)
    sub'#5(#true(),@z,@zs) ->
      ::(#abs(#0()),@zs)
    sum(@x,@y,@r) -> sum#1(+(+(@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)) ->=
      #pos(#natdiv(@x,@y))
    #div(#neg(@x),#pos(@y)) ->=
      #neg(#natdiv(@x,@y))
    #div(#pos(@x),#0()) ->=
      #divByZero()
    #div(#pos(@x),#neg(@y)) ->=
      #neg(#natdiv(@x,@y))
    #div(#pos(@x),#pos(@y)) ->=
      #pos(#natdiv(@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(::(@x_1,@x_2)
       ,::(@y_1,@y_2)) ->=
      #and(#eq(@x_1,@y_1)
          ,#eq(@x_2,@y_2))
    #eq(::(@x_1,@x_2),nil()) ->=
      #false()
    #eq(::(@x_1,@x_2)
       ,tuple#2(@y_1,@y_2)) ->=
      #false()
    #eq(nil(),::(@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)
       ,::(@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))
    #natdiv(#0(),#0()) ->=
      #divByZero()
    #natdiv(#s(@x),#s(@y)) ->=
      #s(#natdiv(#natsub(@x,@y)
                ,#s(@y)))
    #natmult(#0(),@y) ->= #0()
    #natmult(#s(@x),@y) ->=
      #add(#pos(@y),#natmult(@x,@y))
    #natsub(@x,#0()) ->= @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))))