def Trim.trim {n m k : ℕ} (B : Bdd n m) (h1 : k ≤ m) (h2 : ∀ (j : Fin m), Pointer.Reachable B.heap B.root (Pointer.node j) → ↑j < k) : Bdd n k

Equations

• Trim.trim B h1_2 h2_2 = match h : B.root with | Pointer.terminal b => { heap := Vector.emptyWithCapacity 0, root := Pointer.terminal b } | Pointer.node j => let_fun this := ⋯; ⋯.elim
• Trim.trim B h1_2 h2_2 = { heap := Vector.cast ⋯ (Vector.map Trim.trim_node✝ (B.heap.take (l + 1))), root := Trim.trim_pointer✝ B.root }

theorem Trim.trim_ordered {n m k : ℕ} {B : Bdd n m} (o : B.Ordered) {h1 : k ≤ m} {h2 : ∀ (j : Fin m), Pointer.Reachable B.heap B.root (Pointer.node j) → ↑j < k} : (trim B h1 h2).Ordered

def Trim.otrim {n m k : ℕ} (O : OBdd n m) (h1 : k ≤ m) (h2 : ∀ (j : Fin m), Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) → ↑j < k) : OBdd n k

Equations

• Trim.otrim O h1 h2 = ⟨Trim.trim (↑O) h1 h2, ⋯⟩

theorem Trim.otrim_reduced {n m k : ℕ} {O : OBdd n m} {h1 : k ≤ m} {h2 : ∀ (j : Fin m), Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) → ↑j < k} (hr : O.Reduced) : (otrim O h1 h2).Reduced

theorem Trim.otrim_evaluate {n m k : ℕ} {O : OBdd n m} {h1 : k ≤ m} {h2 : ∀ (j : Fin m), Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) → ↑j < k} : (otrim O h1 h2).evaluate = O.evaluate