[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,

Specification bin-min-heap-inv
enrich
   bin-min-heap-ops
, 
   keyindex-set
with
   

   
   
   functions  keyset : key-array × nat → set;
   predicates  2exp-size : nat;
               no-dups : key-array × nat;
               no-dups-idx : key-array × nat;
               heap-order : key-array × nat;
               valid-idx : key-array × array × nat;
   
   variables  m1 : nat;
   
   

   

   axioms 2exp-size :  ⊦ 2exp-size(m) ↔ (∃ n. m = 2^ n);
          used for: ls;
          no-dups :  ⊦ no-dups(kar, n) ↔ (∀ m0, m1. m0 < # kar ∧ m0 < n ∧ m1 < # kar ∧ m1 < n ∧ m0 ≠ m1 → kar[m0] ≠ kar[m1]);
          used for: ls;
          no-dups-idx
          :  ⊦ no-dups-idx(kar, n) ↔ (∀ m0, m1. m0 < # kar ∧ m0 < n ∧ m1 < # kar ∧ m1 < n ∧ m0 ≠ m1 → kar[m0].idx ≠ kar[m1].idx);
          used for: ls;
          keyset-base :  ⊦ keyset(kar, 0) = ∅;
          used for: s, ls;
          keyset-rec :  ⊦ n < # kar → keyset(kar, n + 1) = keyset(kar, n) ++ kar[n];
          used for: s, ls;
          heap-order :  ⊦ heap-order(kar, n) ↔ (∀ m. m < n ∧ m ≠ 0 → ¬ kar[m].key < kar[(m - 1) / 2].key);
          used for: ls;
          valid-idx :  ⊦ valid-idx(kar, ar, n) ↔ n ≤ # kar ∧ (∀ m. m < n → kar[m].idx < # ar ∧ ar[kar[m].idx].idx = m);
          used for: ls;

   

   
end enrich