structure Reduce.StepInv {n m : ℕ} (O : OBdd n m) (ps : ProvedState n m) (i s₀ : ℕ) (curkey : KeyPair) (curptr : RawBdd.RawPointer) (Q : List (KeyPair × Fin m)) : Prop

• hs0 : s₀ ≤ ps.state.size
• hbase (k : Fin ps.state.size) : ↑k < s₀ → i < ↑ps.state.heap[k].va
• hsuffix (k : Fin ps.state.size) : s₀ ≤ ↑k → ↑ps.state.heap[k].va = i
• hheapinj : HeapInjective ps
• hvarinv : VarInvariant O ps
• hcurlvl (k : Fin ps.state.size) : curptr = RawBdd.RawPointer.node ↑k → ↑ps.state.heap[k].va = i
• hnonred (e : KeyPair × Fin m) : e ∈ Q → e.1.1 ≠ e.1.2
• hbounds0 (e : KeyPair × Fin m) : e ∈ Q → RawBdd.RawPointer.Bounded s₀ e.1.1 ∧ RawBdd.RawPointer.Bounded s₀ e.1.2
• hsorted : List.Pairwise (fun (a b : KeyPair × Fin m) => a.1 ≤ b.1) Q
• hcur_le (e : KeyPair × Fin m) : e ∈ Q → curkey ≤ e.1
• hpushed_le (k : Fin ps.state.size) : s₀ ≤ ↑k → toLex (ps.state.heap[k].lo, ps.state.heap[k].hi) ≤ curkey

theorem Reduce.keyLE_sentinel (a : KeyPair) : toLex (RawBdd.RawPointer.terminal false, RawBdd.RawPointer.terminal false) ≤ a

The sentinel key (.terminal false, .terminal false) is the least key: .terminal false is the least RawPointer, so it is ≤ every key. Used as the initial curkey in step.

theorem Reduce.sentinel_no_match {m : ℕ} (Q : List (KeyPair × Fin m)) (hnonred : ∀ entry ∈ Q, entry.1.1 ≠ entry.1.2) (entry : KeyPair × Fin m) : entry ∈ Q → entry.1 ≠ (RawBdd.RawPointer.terminal false, RawBdd.RawPointer.terminal false)

In a non-redundant queue, no entry's key matches the sentinel ⟨.terminal false, .terminal false⟩.

def Reduce.process_queue {n m i : ℕ} (O : OBdd n m) (curkey : KeyPair) (curptr : RawBdd.RawPointer) (s₀ : ℕ) (Q : List (KeyPair × Fin m)) (ps : ProvedState n m) : Invariant O ps i → (∀ entry ∈ Q, RawBdd.RawPointer.Bounded ps.state.size entry.1.1 ∧ RawBdd.RawPointer.Bounded ps.state.size entry.1.2) → (hcurptr_sem : ∀ entry ∈ Q, entry.1 = curkey → ∃ (hj : { heap := O.bdd.heap, root := Pointer.node entry.2 }.Ordered) (hp : RawBdd.RawPointer.Bounded ps.state.size curptr) (ho : { heap := RawBdd.cook_heap ps.state.heap ⋯, root := curptr.cook hp }.Ordered), { bdd := { heap := RawBdd.cook_heap ps.state.heap ⋯, root := curptr.cook hp }, ordered := ho }.Reduced ∧ ∀ (I : Vector Bool n), { bdd := { heap := RawBdd.cook_heap ps.state.heap ⋯, root := curptr.cook hp }, ordered := ho }.evaluate I = { bdd := { heap := O.bdd.heap, root := Pointer.node entry.2 }, ordered := hj }.evaluate I) → (hec : ∀ entry ∈ Q, EntryCorrect O ps i entry) → (si : StepInv O ps i s₀ curkey curptr Q) → { ps' : ProvedState n m // Invariant O ps' i ∧ (∀ (k : Fin m), ps.state.ids[k].isSome = true → ps'.state.ids[k].isSome = true) ∧ (∀ entry ∈ Q, ps'.state.ids[entry.2].isSome = true) ∧ VarInvariant O ps' ∧ HeapInjective ps' ∧ ∀ (k : Fin ps'.state.size), i ≤ ↑ps'.state.heap[k].va }

Equations

• One or more equations did not get rendered due to their size.
• Reduce.process_queue O curkey curptr s₀ [] x x_1 x_2 x_3 x_4 x_5 = ⟨x, ⋯⟩