specification
   using natset, gen-ring, matrix+array
   functions 
       O- . : Matrix[Ring] → Matrix[Ring];
       O- . : Array[Ring] → Array[Ring];
       Σ : Set[Nat] × (Nat → Ring) → Ring;
   
   variables 
       mx : Matrix[Ring];
       vec : Array[Ring];
       a : Ring;
       r : Nat;
       c : Nat;
       m : Nat;
       n : Nat;
       f : Nat → Ring;
       ns : Set[Nat];
       g : Nat × Nat → Ring;
   
   partial functions 
       . + . : Matrix[Ring] × Matrix[Ring] → Matrix[Ring] with λ mx1, mx2. #r mx1 = #r mx2 ∧ #c mx2 = #c mx2;
       . + . : Array[Ring] × Array[Ring] → Array[Ring] with λ vec1, vec2. # vec1 = # vec2;
       . * . : Matrix[Ring] × Matrix[Ring] → Matrix[Ring] prio 10 right with λ mx1, mx2. #c mx1 = #r mx2;
       . * . : Matrix[Ring] × Array[Ring] → Array[Ring] prio 10 right with λ mx, vec. #r mx = # vec;
       . * . : Array[Ring] × Matrix[Ring] → Array[Ring] prio 10 right with λ vec, mx. #c mx = # vec;
       . * . : Array[Ring] × Array[Ring] → Ring 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