structure Reduce.StepInv {n m : ℕ} (O : OBdd n m) (ps : ProvedState n m) (i s₀ : ℕ) (curkey : RawBdd.RawPointer × RawBdd.RawPointer) (curptr : RawBdd.RawPointer) (Q : List ((RawBdd.RawPointer × RawBdd.RawPointer) × 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 = Sum.inr ↑k → ↑ps.state.heap[k].va = i
• hnonred (e : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) : e ∈ Q → e.1.1 ≠ e.1.2
• hbounds0 (e : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) : e ∈ Q → RawBdd.RawPointer.Bounded s₀ e.1.1 ∧ RawBdd.RawPointer.Bounded s₀ e.1.2
• hsorted : List.Pairwise (fun (a b : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) => KeyLE a.1 b.1) Q
• hcur_le (e : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) : e ∈ Q → KeyLE curkey e.1
• hpushed_le (k : Fin ps.state.size) : s₀ ≤ ↑k → KeyLE (ps.state.heap[k].lo, ps.state.heap[k].hi) curkey

theorem Reduce.keyLE_sentinel (a : RawBdd.RawPointer × RawBdd.RawPointer) : KeyLE (Sum.inl false, Sum.inl false) a

The sentinel key (.inl false, .inl false) is the least key: .inl 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 ((RawBdd.RawPointer × RawBdd.RawPointer) × Fin m)) (hnonred : ∀ entry ∈ Q, entry.1.1 ≠ entry.1.2) (entry : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) : entry ∈ Q → entry.1 ≠ (Sum.inl false, Sum.inl false)

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

def Reduce.process_queue {n m i : ℕ} (O : OBdd n m) (curkey : RawBdd.RawPointer × RawBdd.RawPointer) (curptr : RawBdd.RawPointer) (s₀ : ℕ) (Q : List ((RawBdd.RawPointer × RawBdd.RawPointer) × 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).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 ⋯ }.Ordered), OBdd.Reduced ⟨{ heap := RawBdd.cook_heap ps.state.heap ⋯, root := curptr.cook ⋯ }, ⋯⟩ ∧ ∀ (I : Vector Bool n), OBdd.evaluate ⟨{ heap := RawBdd.cook_heap ps.state.heap ⋯, root := curptr.cook ⋯ }, ⋯⟩ I = OBdd.evaluate ⟨{ heap := (↑O).heap, root := Pointer.node entry.2 }, ⋯⟩ 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, ⋯⟩