[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 rowcol-upd
enrich
   matrix+array, 
   list-as-arrayinstance, 
   nat-mult
with
   functions 
       toArr : matrix('a) × nat → array('a);
      comment: concatenate the rows upto row n into a long array;
       . .toArr : matrix('a) → array('a);
      comment: concatenate all rows  into a long array;
       toArc : matrix('a) × nat → array('a);
      comment: concatenate the columns upto row n elemo a long array;
       . .toArc : matrix('a) → array('a);
      comment: concatenate all columns elemo a long array;
   
   variables 
       mx : matrix('a);
       a : array('a);
       i : 'a;
       j : 'a;
       m : nat;
       n : nat;
       r : nat;
       c : nat;
   
   partial functions 
       . [ . := . ]r : matrix('a) × nat × array('a) → matrix('a) with λ mx, r, a. r < #r mx ∧ # a = #c mx;
      comment: mx[r, a]r overwrites row r of mx with a. Identity if row is outside matrix;
       . [ . := . ]c : matrix('a) × nat × array('a) → matrix('a) with λ mx, c, a. c < #c mx ∧ # a = #r mx;
      comment: mx[c, a]r overwrites column c of mx with a. Identity if row is outside matrix;
   
   
   axioms 
      rowno-updrow: #c mx = # a ⊦ #r mx[r := a]r = #r mx;
      used for: s, ls;
      
      rowno-updcol: #r mx = # a ⊦ #r mx[c := a]c = #r mx;
      used for: s, ls;
      
      colno-updrow: #c mx = # a ⊦ #c mx[r := a]r = #c mx;
      used for: s, ls;
      
      colno-updcol: #r mx = # a ⊦ #c mx[c := a]c = #c mx;
      used for: s, ls;
      
      updrow-sel: # a = #c mx ∧ r0 < #r mx ∧ c0 < #c mx → (mx[r := a]r)[r0, c0] = (r = r0 ⊃ a[c0];mx[r0, c0]);
      used for: s, ls;
      
      updcol-sel: # a = #r mx ∧ r0 < #r mx ∧ c0 < #c mx → (mx[c := a]c)[r0, c0] = (c = c0 ⊃ a[r0];mx[r0, c0]);
      used for: s, ls;
      
      toArr-def: mx.toArr = toArr(mx, #r mx);
      
      toArr-base: toArr(mx, 0) = [];
      used for: s, ls;
      
      toArr-rec: toArr(mx, m + 1) = toArr(mx, m) + mx[m]r;
      used for: s, ls;
      
      toArc-def: mx.toArc = toArc(mx, #c mx);
      
      toArc-base: toArc(mx, 0) = [];
      used for: s, ls;
      
      toArc-rec: toArc(mx, m + 1) = toArc(mx, m) + mx[m]c;
      used for: s, ls;
   
   
end enrich