specification
   using natset, 
         actualize
            matrix+array
         with
            ring
            
         by morphism
            :array → vector; 
            mkarray → mkvector; 
            # → #; 
            [ ] → [ ]; 
            [ ] → [ ]; 
            [ ]r → [ ]r; 
            [ ]c → [ ]c; 
         end actualize
   functions 
       O- . : matrix → matrix;
       O- . : vector → vector;
       Σ : natset × (nat → elem) → elem;
   
   variables 
       mx : matrix;
       vec : vector;
       a : elem;
       r : nat;
       c : nat;
       m : nat;
       n : nat;
       f : nat → elem;
       ns : natset;
       g : nat × nat → elem;
   
   partial functions 
       . + . : matrix × matrix → matrix with λ mx1, mx2. #r mx1 = #r mx2 ∧ #c mx2 = #c mx2;
       . + . : vector × vector → vector with λ vec1, vec2. # vec1 = # vec2;
       . * . : matrix × matrix → matrix prio 10 right with λ mx1, mx2. #c mx1 = #r mx2;
       . * . : matrix × vector → vector prio 10 right with λ mx, vec. #r mx = # vec;
       . * . : vector × matrix → vector prio 10 right with λ vec, mx. #c mx = # vec;
       . * . : vector × vector → elem prio 10 right with λ vec1, vec2. # vec1 = # vec2;
   
   
   axioms 
      addinvvec-size: # O- vec = # vec;
      used for: s, ls;
      
      addinvvec-get: n < # vec → (O- vec)[n] = O- vec[n];
      used for: s, ls;
      
      addinvmx-rowno: #r O- mx = #r mx;
      used for: s, ls;
      
      addinvmx-colno: #c O- mx = #c mx;
      used for: s, ls;
      
      addinvmx-get: c < #c mx ∧ c < #c mx → (O- mx)[r, c] = O- mx[r, c];
      used for: s, ls;
      
      addvec-size: #(vec1 + vec2) = # vec1;
      used for: s, ls;
      
      addmvec-get: n < # vec1 → (vec1 + vec2)[n] = vec1[n] + vec2[n];
      used for: s, ls;
      
      addmx-rowno: #r(mx1 + mx2) = #r mx1;
      used for: s, ls;
      
      addmx-colno: #c(mx1 + mx2) = #c mx1;
      used for: s, ls;
      
      addmx-get: r < #r mx1 ∧ c < #c mx1 → (mx1 + mx2)[r, c] = mx1[r, c] + mx2[r, c];
      used for: s, ls;
      
      sum-base: Σ(∅, f) = O;
      used for: s, ls;
      
      sum-rec: ¬ n ∈ ns → Σ(ns ++ n, f) = f(n) + Σ(ns, f);
      used for: s, ls;
      
      multmx-rowno: #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1;
      used for: s, ls;
      
      multmx-colno: #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2;
      used for: s, ls;
      
      multmx-get: #c mx1 = #r mx2 ∧ r < #r mx1 ∧ c < #c mx2 → (mx1 * mx2)[r, c] = Σ(0 to #c mx1, λ n. mx1[r, n] * mx2[n, c]);
      used for: s, ls;
      
      multmxvec-size: #c mx = # vec → #(mx * vec) = #r mx;
      used for: s, ls;
      
      multmxvec-get: #c mx = # vec ∧ r < #r mx → (mx * vec)[r] = Σ(0 to # vec, λ n. mx[r, n] * vec[n]);
      used for: s, ls;
      
      multvecmx-size: #r mx = # vec → #(vec * mx) = #c mx;
      used for: s, ls;
      
      multvecmx-get: #r mx = # vec ∧ c < #c mx → (vec * mx)[c] = Σ(0 to # vec, λ n. vec[n] * mx[n, c]);
      used for: s, ls;
   
   
end specification