def Collect.collect {n m : ℕ} (O : OBdd n m) : List (Fin m)

Return a list of all reachable node indices.

Equations

• Collect.collect O = (Collect.collect_helper✝ O (Vector.replicate m false, [])).2

theorem Collect.collect_terminal {n m : ℕ} {b : Bool} {O : OBdd n m} (h : (↑O).root = Pointer.terminal b) : collect O = []

theorem Collect.collect_spec {n m : ℕ} {O : OBdd n m} {j : Fin m} : Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) → j ∈ collect O

collect is correct.

theorem Collect.collect_spec_reverse {n m : ℕ} {O : OBdd n m} {j : Fin m} : j ∈ collect O → Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j)

theorem Collect.mem_collect_iff_reachable {n m : ℕ} {O : OBdd n m} {j : Fin m} : j ∈ collect O ↔ Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j)

theorem Collect.collect_nodup {n m : ℕ} {O : OBdd n m} : (collect O).Nodup