[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-revops
enrich
   rowcol-upd
, 
   gen-tord-min-max

with
   comment: partial functions with reverted arguments must be defined,
         since partial functions can be instantiated with partial functions with the same domain only.;
   variables 
       mx : matrix('a);
       r : nat;
       c : nat;
       a : 'a;
   
   partial functions 
       . [ . ]rv : matrix('a) × nat × nat → 'a with λ mx, c, r. c < #c mx ∧ r < #r mx;
       . [ . ]rv : matrix('a) × nat × nat × 'a → matrix('a) with λ mx, c, r, a. c < #c mx ∧ r < #r mx;
   
   
   axioms 
      revselect-def: mx[c, r]rv = mx[r, c];
      used for: ls;
      
      revput-def: mx[c, r, a]rv = mx[r, c, a];
      used for: ls;
   
   
end enrich