(STRATEGY
    INNERMOST)

(VAR
    @acc @base @l @l1 @l2 @line @ls
    @m @m' @m1 @m2 @m3 @mm @ms @x
    @xs @xss @y @ys)
(DATATYPES
    A = µX.< #0, #neg(X), #pos(X), #s(X), ::(X, X), nil, tuple#2(X, X) >)
(SIGNATURES
    #abs :: [A] -> A
    * :: [A x A] -> A
    + :: [A x A] -> A
    attach :: [A x A] -> A
    attach#1 :: [A x A] -> A
    attach#2 :: [A x A x A] -> A
    lineMult :: [A x A] -> A
    lineMult#1 :: [A x A] -> A
    m1 :: [A] -> A
    m2 :: [A] -> A
    m3 :: [A] -> A
    m4 :: [A] -> A
    makeBase :: [A] -> A
    makeBase#1 :: [A] -> A
    matrixMult :: [A x A] -> A
    matrixMult' :: [A x A] -> A
    matrixMult'#1 :: [A x A] -> A
    matrixMult3 :: [A x A x A] -> A
    matrixMultList :: [A x A] -> A
    matrixMultList#1 :: [A x A] -> A
    matrixMultOld :: [A x A] -> A
    mkBase :: [A] -> A
    mkBase#1 :: [A] -> A
    mult :: [A x A] -> A
    mult#1 :: [A x A] -> A
    mult#2 :: [A x A x A] -> A
    split :: [A] -> A
    split#1 :: [A] -> A
    split#2 :: [A x A] -> A
    split#3 :: [A x A x A] -> A
    transAcc :: [A x A] -> A
    transAcc#1 :: [A x A] -> A
    transpose :: [A] -> A
    transpose#1 :: [A x A] -> A
    transpose#2 :: [A] -> A
    transpose#3 :: [A x A] -> A
    transpose' :: [A] -> A
    #add :: [A x A] -> A
    #mult :: [A x A] -> A
    #natmult :: [A x A] -> A
    #pred :: [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))
    *(@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))))