(VAR @acc @base @l @l1 @l2 @line @ls @m @m' @m1 @m2 @m3 @mm @ms @x @xs @xss @y @ys )
(STRATEGY INNERMOST)
(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
        m1(@x) -> ::(::(#abs(#pos(#s(#0))),::(#abs(#pos(#s(#s(#0)))),::(#abs(#pos(#s(#s(#s(#0))))),nil))),::(::(#abs(#pos(#s(#s(#0)))),::(#abs(#pos(#s(#s(#s(#0))))),::(#abs(#pos(#s(#s(#s(#s(#0)))))),nil))),nil))
        m2(@x) -> ::(::(#abs(#pos(#s(#0))),::(#abs(#pos(#s(#s(#0)))),nil)),::(::(#abs(#pos(#s(#s(#0)))),::(#abs(#pos(#s(#s(#s(#0))))),nil)),::(::(#abs(#pos(#s(#s(#s(#s(#0)))))),::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))),nil)),nil)))
        m3(@x) -> ::(::(#abs(#pos(#s(#0))),::(#abs(#pos(#s(#s(#0)))),::(#abs(#pos(#s(#s(#s(#0))))),::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))),nil)))),::(::(#abs(#pos(#s(#s(#0)))),::(#abs(#pos(#s(#s(#s(#0))))),::(#abs(#pos(#s(#s(#s(#s(#0)))))),::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))),nil)))),nil))
        m4(@x) -> ::(::(#abs(#pos(#s(#0))),nil),::(::(#abs(#pos(#s(#s(#0)))),nil),::(::(#abs(#pos(#s(#s(#s(#0))))),nil),::(::(#abs(#pos(#s(#s(#s(#s(#0)))))),nil),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))
        #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)))
)