Specification array-listops

[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,

enrich
   array-copy
with
   constants 
       [] : array('a);
   
   functions 
       . + . : 'a × array('a) → array('a);
   
   predicates 
       . < . : array('a) × array('a);
   
   variables 
       ar : array('a);
       a : 'a;
       n : nat;
   
   partial functions 
       . .first : array('a) → 'a with λ ar. ar ≠ [];
       . .rest : array('a) → array('a) with λ ar. ar ≠ [];
   
   
   axioms 
      nil: [] = mkarray(0);
      
      cons: a + ar = copy(ar, 0, mkarray(# ar + 1), 1, # ar)[0 := a];
      
      first: ar.first = ar[0];
      
      rest: ar.rest = subarray(ar, 1, # ar - 1);
      
      postfix: ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0);
   
   
end enrich