Specification matrixops

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,
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