(STRATEGY
    INNERMOST)

(VAR
    @_@3 @a @acc @as @dequeue@1
    @dequeue@2 @elem @inq @l @l1 @l2
    @line @ls @m @m1 @m2 @n @outq
    @queue @queue' @sofar @t @t1 @t2
    @toreverse @ts @x @xs @y @ys)
(DATATYPES
    A = µX.< ::(X, X), nil, tuple#2(X, X), leaf, node(X, X, X), #0, #neg(X), #s(X), #pos(X) >)
(SIGNATURES
    * :: [A x A] -> A
    + :: [A x A] -> A
    appendreverse :: [A x A] -> A
    appendreverse#1 :: [A x A] -> A
    bftMult :: [A x A] -> A
    bftMult' :: [A x A] -> A
    bftMult'#1 :: [A x A] -> A
    bftMult'#2 :: [A] -> A
    bftMult'#3 :: [A x A x A] -> A
    bftMult'#4 :: [A x A x A] -> A
    bftMult'#5 :: [A x A x A] -> A
    computeLine :: [A x A x A] -> A
    computeLine#1 :: [A x A x A] -> A
    computeLine#2 :: [A x A x A x A] -> A
    dequeue :: [A x A] -> A
    dequeue#1 :: [A x A] -> A
    dequeue#2 :: [A] -> A
    enqueue :: [A x A] -> A
    enqueue#1 :: [A x A] -> A
    lineMult :: [A x A x A] -> A
    lineMult#1 :: [A x A x A] -> A
    lineMult#2 :: [A x A x A x A] -> A
    matrixMult :: [A x A] -> A
    matrixMult#1 :: [A x A] -> A
    reverse :: [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)
    +(@x,@y) -> #add(@x,@y)
    appendreverse(@toreverse
                 ,@sofar) ->
      appendreverse#1(@toreverse
                     ,@sofar)
    appendreverse#1(::(@a,@as)
                   ,@sofar) -> appendreverse(@as
                                            ,::(@a,@sofar))
    appendreverse#1(nil(),@sofar) ->
      @sofar
    bftMult(@t,@acc) ->
      bftMult'(tuple#2(::(@t,nil())
                      ,nil())
              ,@acc)
    bftMult'(@queue,@acc) ->
      bftMult'#1(bftMult'#2(@queue)
                ,@acc)
    bftMult'#1(tuple#2(@elem,@queue)
              ,@acc) -> bftMult'#3(@elem
                                  ,@acc
                                  ,@queue)
    bftMult'#2(tuple#2(@dequeue@1
                      ,@dequeue@2)) ->
      dequeue(@dequeue@1,@dequeue@2)
    bftMult'#3(::(@t,@_@3)
              ,@acc
              ,@queue) -> bftMult'#4(@t
                                    ,@acc
                                    ,@queue)
    bftMult'#3(nil(),@acc,@queue) ->
      @acc
    bftMult'#4(leaf()
              ,@acc
              ,@queue) -> bftMult'(@queue
                                  ,@acc)
    bftMult'#4(node(@y,@t1,@t2)
              ,@acc
              ,@queue) ->
      bftMult'#5(enqueue(@t2
                        ,enqueue(@t1,@queue))
                ,@acc
                ,@y)
    bftMult'#5(@queue',@acc,@y) ->
      bftMult'(@queue'
              ,matrixMult(@acc,@y))
    computeLine(@line,@m,@acc) ->
      computeLine#1(@line,@acc,@m)
    computeLine#1(::(@x,@xs)
                 ,@acc
                 ,@m) -> computeLine#2(@m
                                      ,@acc
                                      ,@x
                                      ,@xs)
    computeLine#1(nil(),@acc,@m) ->
      @acc
    computeLine#2(::(@l,@ls)
                 ,@acc
                 ,@x
                 ,@xs) -> computeLine(@xs
                                     ,@ls
                                     ,lineMult(@x,@l,@acc))
    computeLine#2(nil()
                 ,@acc
                 ,@x
                 ,@xs) -> nil()
    dequeue(@outq,@inq) ->
      dequeue#1(@outq,@inq)
    dequeue#1(::(@t,@ts),@inq) ->
      tuple#2(::(@t,nil())
             ,tuple#2(@ts,@inq))
    dequeue#1(nil(),@inq) ->
      dequeue#2(reverse(@inq))
    dequeue#2(::(@t,@ts)) ->
      tuple#2(::(@t,nil())
             ,tuple#2(@ts,nil()))
    dequeue#2(nil()) ->
      tuple#2(nil()
             ,tuple#2(nil(),nil()))
    enqueue(@t,@queue) ->
      enqueue#1(@queue,@t)
    enqueue#1(tuple#2(@outq,@inq)
             ,@t) -> tuple#2(@outq
                            ,::(@t,@inq))
    lineMult(@n,@l1,@l2) ->
      lineMult#1(@l1,@l2,@n)
    lineMult#1(::(@x,@xs),@l2,@n) ->
      lineMult#2(@l2,@n,@x,@xs)
    lineMult#1(nil(),@l2,@n) ->
      nil()
    lineMult#2(::(@y,@ys)
              ,@n
              ,@x
              ,@xs) -> ::(+(*(@x,@n),@y)
                         ,lineMult(@n,@xs,@ys))
    lineMult#2(nil(),@n,@x,@xs) ->
      ::(*(@x,@n)
        ,lineMult(@n,@xs,nil()))
    matrixMult(@m1,@m2) ->
      matrixMult#1(@m1,@m2)
    matrixMult#1(::(@l,@ls),@m2) ->
      ::(computeLine(@l,@m2,nil())
        ,matrixMult(@ls,@m2))
    matrixMult#1(nil(),@m2) -> nil()
    reverse(@xs) ->
      appendreverse(@xs,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))))