Specification matrix-dot

[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,

enrich
   matrix
with
   

   
   
   functions  Σ : nat × (nat → int) → int;
              . * . : matrix × matrix → matrix prio 10 right;
   
   
   variables  k : nat;
              nf : nat → int;
              nnf : nat × nat → int;
   
   

   

   axioms at-dot :  ⊦ A.cols = B.rows → (A * B)[m, n] = Σ(A.cols, λ k. A[m, k] * B[k, n]);
          used for: s, ls, c, lc;
          rows-dot :  ⊦ A.cols = B.rows → (A * B).rows = A.rows;
          used for: s, ls, c, lc;
          cols-dot :  ⊦ A.cols = B.rows → (A * B).cols = B.cols;
          used for: s, ls, c, lc;
          sum-base :  ⊦ Σ(0, nf) = 0;
          used for: s, ls;
          sum-rec :  ⊦ Σ(n + 1, nf) = nf(n) + Σ(n, nf);
          used for: s, ls;

   

   
end enrich