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