Specification sorted

[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 bag-array , 
       order with
   predicates 
      sorted : array × (elem × elem → bool);
      sorted : array × nat × nat × (elem × elem → bool);
   variables 
      ⊑ : elem × elem → bool; 
   
   axioms 
      sorted-sub :  ⊦ sorted(ar, n0, n1, ⊑) ↔ (∀ n, m. n0 ≤ n ∧ n < m ∧ m < n1 → ⊑(ar[n], ar[m]));
      used for : ls;
       
      sorted-entire :  ⊦ sorted(ar, ⊑) ↔ (∀ n, m. n < m ∧ m < # ar → ⊑(ar[n], ar[m]));
      used for : ls;
       
end enrich