(VAR
    acc l l1 l2 line ls m m1 m2 n x xs y ys)

(DATATYPES a = µX. < dd(X,X), nil, '0, 's(X), 'neg(X), 'pos(X) >
 )

(SIGNATURES
   mult :: a x a -> a
   'mult :: a x a -> a
   add :: a x a -> a
   'add :: 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
   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
   'pred :: a -> a
   'succ :: a -> a
   'natmult :: a x a -> a
   'natadd :: a x a -> a
 )

(RULES
    mult(x,y) -> 'mult(x,y)
    add(x,y) -> 'add(x,y)
    computeLine(line,m,acc) -> computeLine'1(line,acc,m)
    computeLine'1(dd(x,xs),acc,m) -> computeLine'2(m,acc,x,xs)
    computeLine'1(nil,acc,m) -> acc
    computeLine'2(dd(l,ls),acc,x,xs) -> computeLine(xs,ls,lineMult(x,l,acc))
    computeLine'2(nil,acc,x,xs) -> nil
    lineMult(n,l1,l2) -> lineMult'1(l1,l2,n)
    lineMult'1(dd(x,xs),l2,n) -> lineMult'2(l2,n,x,xs)
    lineMult'1(nil,l2,n) -> nil
    lineMult'2(dd(y,ys),n,x,xs) -> dd(add(mult(x,n),y),lineMult(n,xs,ys))
    lineMult'2(nil,n,x,xs) -> dd(mult(x,n),lineMult(n,xs,nil))
    matrixMult(m1,m2) -> matrixMult'1(m1,m2)
    matrixMult'1(dd(l,ls),m2) -> dd(computeLine(l,m2,nil),matrixMult(ls,m2))
    matrixMult'1(nil,m2) -> 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))))