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;
   
   functions 
       . + . : Elem × Array → Array;
   
   predicates 
       . < . : Array × Array;
   
   variables 
       ar : Array;
       a : Elem;
       n : Nat;
   
   partial functions 
       . first : Array → Elem with λ ar. ar ≠ [];
       . rest : Array → Array 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