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