(STARTTERM
    CONSTRUCTOR-BASED)
(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)
(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))
    #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))))
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'bft_mmult.raml', c.f. http://raml.tcs.ifi.lmu.de/)