[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;
       r : nat;
       c : nat;
   
   partial functions 
       . [ . ]r : matrix × nat → array with λ mx, r. r < #r mx;
      comment: selects a row;
       . [ . ]c : matrix × nat → array 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