[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 cube+array
enrich
   cube, 
   array
with
   variables 
       cu : cube('a);
       nx : nat;
       ny : nat;
       nz : nat;
   
   partial functions 
       . [ . ]xy : cube('a) × nat × nat → array('a) with λ cu, nx, ny. nx < #x cu ∧ ny < #y cu;
      comment: selects the array at a certain width and depth;
       . [ . ]xz : cube('a) × nat × nat → array('a) with λ cu, nx, nz. nx < #x cu ∧ nz < #z cu;
      comment: selects the array at a certain width and height;
       . [ . ]yz : cube('a) × nat × nat → array('a) with λ cu, ny, nz. ny < #y cu ∧ nz < #z cu;
      comment: selects the array at a certain depth and height;
   
   
   axioms 
      sel-wd-size: # cu[nx, ny]xy = #z cu;
      used for: s, ls;
      
      sel-wh-size: # cu[nx, nz]xz = #y cu;
      used for: s, ls;
      
      sel-dh-size: # cu[ny, nz]yz = #x cu;
      used for: s, ls;
      
      sel-wd-get: cu[nx, ny]xy[nz] = cu[nx, ny, nz];
      used for: s, ls;
      
      sel-wh-get: cu[nx, nz]xz[ny] = cu[nx, ny, nz];
      used for: s, ls;
      
      sel-dh-get: cu[ny, nz]yz[nx] = cu[nx, ny, nz];
      used for: s, ls;
   
   
end enrich