def Reduce.oreduce {n m : ℕ} (O : OBdd n m) : { p : (s : ℕ) × OBdd n s // p.snd.Reduced ∧ p.snd.evaluate = O.evaluate }

Equations

• One or more equations did not get rendered due to their size.
• Reduce.oreduce O_2 = match hroot : (↑O_2).root with | Pointer.terminal b => ⟨⟨0, ⟨{ heap := Vector.emptyWithCapacity 0, root := Pointer.terminal b }, ⋯⟩⟩, ⋯⟩ | Pointer.node j => absurd ⋯ ⋯

@[simp]

theorem Reduce.oreduce_evaluate {n m : ℕ} {O : OBdd n m} : (↑(oreduce O)).snd.evaluate = O.evaluate