def Restrict.orestrict {n m : ℕ} (b : Bool) (i : Fin n) (O : OBdd n m) : (s : ℕ) × OBdd n s

Equations

• One or more equations did not get rendered due to their size.

theorem Restrict.orestrict_correct {n m : ℕ} {b : Bool} {i : Fin n} {O : OBdd n m} : (orestrict b i O).snd.evaluate = Nary.restrict O.evaluate b i