(STARTTERM
    CONSTRUCTOR-BASED)
(STRATEGY
    INNERMOST)

(VAR
    @acc @base @l @l1 @l2 @line @ls @m @m' @m1 @m2 @m3 @mm @ms @x @xs @xss @y @ys)
(RULES
    #abs(#0()) -> #0()
    #abs(#neg(@x)) -> #pos(@x)
    #abs(#pos(@x)) -> #pos(@x)
    #abs(#s(@x)) -> #pos(#s(@x))
    *(@x,@y) -> #mult(@x,@y)
    +(@x,@y) -> #add(@x,@y)
    attach(@line,@m) -> attach#1(@line,@m)
    attach#1(::(@x,@xs),@m) -> attach#2(@m,@x,@xs)
    attach#1(nil(),@m) -> nil()
    attach#2(::(@l,@ls),@x,@xs) -> ::(::(@x,@l),attach(@xs,@ls))
    attach#2(nil(),@x,@xs) -> nil()
    lineMult(@l,@m2) -> lineMult#1(@m2,@l)
    lineMult#1(::(@x,@xs),@l) -> ::(mult(@l,@x),lineMult(@l,@xs))
    lineMult#1(nil(),@l) -> nil()
    makeBase(@m) -> makeBase#1(@m)
    makeBase#1(::(@l,@m')) -> mkBase(@l)
    makeBase#1(nil()) -> nil()
    matrixMult(@m1,@m2) -> matrixMult'(@m1,transAcc(@m2,makeBase(@m2)))
    matrixMult'(@m1,@m2) -> matrixMult'#1(@m1,@m2)
    matrixMult'#1(::(@l,@ls),@m2) -> ::(lineMult(@l,@m2),matrixMult'(@ls,@m2))
    matrixMult'#1(nil(),@m2) -> nil()
    matrixMult3(@m1,@m2,@m3) -> matrixMult(matrixMult(@m1,@m2),@m3)
    matrixMultList(@acc,@mm) -> matrixMultList#1(@mm,@acc)
    matrixMultList#1(::(@m,@ms),@acc) -> matrixMultList(matrixMult(@acc,@m),@ms)
    matrixMultList#1(nil(),@acc) -> @acc
    matrixMultOld(@m1,@m2) -> matrixMult'(@m1,transpose(@m2))
    mkBase(@m) -> mkBase#1(@m)
    mkBase#1(::(@l,@m')) -> ::(nil(),mkBase(@m'))
    mkBase#1(nil()) -> nil()
    mult(@l1,@l2) -> mult#1(@l1,@l2)
    mult#1(::(@x,@xs),@l2) -> mult#2(@l2,@x,@xs)
    mult#1(nil(),@l2) -> #abs(#0())
    mult#2(::(@y,@ys),@x,@xs) -> +(*(@x,@y),mult(@xs,@ys))
    mult#2(nil(),@x,@xs) -> #abs(#0())
    split(@m) -> split#1(@m)
    split#1(::(@l,@ls)) -> split#2(@l,@ls)
    split#1(nil()) -> tuple#2(nil(),nil())
    split#2(::(@x,@xs),@ls) -> split#3(split(@ls),@x,@xs)
    split#2(nil(),@ls) -> tuple#2(nil(),nil())
    split#3(tuple#2(@ys,@m'),@x,@xs) -> tuple#2(::(@x,@ys),::(@xs,@m'))
    transAcc(@m,@base) -> transAcc#1(@m,@base)
    transAcc#1(::(@l,@m'),@base) -> attach(@l,transAcc(@m',@base))
    transAcc#1(nil(),@base) -> @base
    transpose(@m) -> transpose#1(@m,@m)
    transpose#1(::(@xs,@xss),@m) -> transpose#2(split(@m))
    transpose#1(nil(),@m) -> nil()
    transpose#2(tuple#2(@l,@m')) -> transpose#3(@m',@l)
    transpose#3(::(@y,@ys),@l) -> ::(@l,transpose(::(@y,@ys)))
    transpose#3(nil(),@l) -> nil()
    transpose'(@m) -> transAcc(@m,makeBase(@m))
    #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 'matrix.raml', c.f. http://raml.tcs.ifi.lmu.de/)