Specification array-revin

[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
   functions 
       rev : Array → Array;
   
   predicates 
       . ∈ . : Elem × Array;
   
   variables 
       m : Nat;
       n : Nat;
       ar : Array;
       a : Elem;
   
   partial functions 
       rev : Array × Nat → Array with λ ar, n. n ≤ # ar;
   
   axioms 
      in: a ∈ ar ↔ (∃ n. n < # ar ∧ ar(n) = a);
      used for: ls;
      
      rev-base: rev(ar, 0) = mkarray(# ar);
      used for: s, ls;
      
      rev-rec: n < # ar → rev(ar, n + 1) = rev(ar, n)(n := ar(# ar - n + 1));
      used for: s, ls;
      
      rev: rev(ar) = rev(ar, # ar);
   
   
end enrich