Proof step 2 from proof prepost-create-gcheap (previous step)

Heuristic nonrecursive calls applied rule call right

And obtained the following new goals

• Proof step 3:

  log = nx, lpt0 = lpt ⊦ ⟪gc_heap_empty#(; gch); let n = 0 in while n < # lpt do {/* (prepost-create-gcheap : invariant n ≤ # lpt ∧ bin-heap-inv(gch, lpt) ∧ gc-heap(lpt, log, n) = keyset(gch) ∧ id-idx(lpt`, lpt) wfbound # lpt - n) */; if lpt[n].flags = LP_GROUP_NODES ∧ ¬ n ∈ log then let ki = key-index(lpt[n].ref-size, n) in gc_heap_insert#(ki; gch, lpt); n := n + 1}⟫ (bin-heap-inv(gch, lpt) ∧ gc-heap(lpt0, nx) = keyset(gch) ∧ id-idx(lpt0, lpt))

Rule argument

Additional information

Used simplifier rules: create-gcheap: ⊦ ;