[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 matrix+array
enrich
   matrix, 
   array
with
   variables 
       mx : Matrix[A];
       r : Nat;
       c : Nat;
   
   partial functions 
       . [ . ]r : Matrix[A] × Nat → Array[A] with λ mx, r. r < #r mx;
      comment: selects a row;
       . [ . ]c : Matrix[A] × Nat → Array[A] with λ mx, c. c < #c mx;
      comment: selects a column;
   
   axioms 
      selrow-size: # mx[r]r = #c mx;
      used for: s, ls;
      
      selrow-get: mx[r]r(c) = mx(r, c);
      used for: s, ls;
      
      selcol-size: # mx[c]c = #r mx;
      used for: s, ls;
      
      selcol-get: mx[c]c(r) = mx(r, c);
      used for: s, ls;
   
   
end enrich