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.

@[simp]

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