[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 gc-heap-base
instantiate parameter
   binheap-key
, 
   elem-index

< 
   bin-min-heap-prepost

with 
   nat, 
   lprops


   
by mapping
      : key → nat; 
      : elem → nat × nat × lpropflags; 
      : elem-index → lprops; 
      .elem → .ref-size, .size, .flags; 
      .idx → .gcheapidx; 
      .elem:= → λ lp, n0, n1, lpf. ((lp.ref-size:= n0).size:= n1).flags:= lpf; 
      .idx:= → .gcheapidx:=; 
      elemindex → mklp; 
      < → <; 
      ei → lp; 
      a → n2, n3, lpf; 
      b → n4, n5, lpf0; 
      c → n6, n7, lpf1; 
      a0 → n8, n9, lpf2; 
      key → key; 
      key0 → key0; 
      key1 → key1
   rename 
      :array → lp-array; 
      mkarray → mklparray; 
      key-index → key-index; 
      .key → .key; 
      .key:= → .key:=; 
      # → #; 
      fill → fill; 
      rev → rev; 
      ∈ → ∈; 
      id○ → id○; 
      id-idx → id-idx; 
      valid-idx → valid-idx; 
      bin-heap-inv → bin-heap-inv; 
      bubble-up-inv → bubble-up-inv; 
      bubble-down-inv → bubble-down-inv; 
      bin_min_heap_insert# → bin_min_heap_insert#; 
      bin_min_heap_remove# → bin_min_heap_remove#; 
      bin_min_heap_update# → bin_min_heap_update#; 
      bin_min_heap_extract_min# → bin_min_heap_extract_min#; 
      bin_min_heap_bubble_up# → bin_min_heap_bubble_up#; 
      bin_min_heap_bubble_down# → bin_min_heap_bubble_down#; 
      ei0 → lp2; 
      ei1 → lp3; 
      ar → lpt; 
      ar0 → lpt0; 
      ar1 → lpt1; 
      ar2 → lpt2; 
      [ ] → [ ]; 
      [ ] → [ ]; 
      fill → fill; 
      copy → copy; 
      subarray → subarray; 
      rev → rev; 
      cmp → cmp; 
      cmp → cmp; 
      idrange → idrange
end instantiate