def Apply.oapply {n m n' m' : ℕ} (op : Bool → Bool → Bool) (O : OBdd n m) (U : OBdd n' m') : (s : ℕ) × OBdd (max n n') s

Equations

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

theorem Apply.oapply_correct {n m n' m' : ℕ} (op : Bool → Bool → Bool) (O : OBdd n m) (U : OBdd n' m') (I : Vector Bool (max n n')) : (oapply op O U).snd.evaluate I = op (O.evaluate (Vector.cast ⋯ (I.take n))) (U.evaluate (Vector.cast ⋯ (I.take n')))