@[simp]

theorem Apply.toVar_or_terminal_eq {b : Bool} {i n m : ℕ} (w : Vector (Node n m) m) : RawBdd.toVar_or w (Pointer.terminal b) i = i

@[simp]

theorem Apply.toVar_or_node_eq {i n m : ℕ} (w : Vector (Node n m) m) {j : Fin m} : RawBdd.toVar_or w (Pointer.node j) i = ↑w[j].var

def Apply.oapply {n m n' m' : ℕ} (op : Bool → Bool → Bool) (O : OBdd n m) (U : OBdd n' m') : (s : ℕ) × { OU : OBdd (max n n') s // ∀ (I : Vector Bool (max n n')), OU.evaluate I = op (O.evaluate (Vector.cast ⋯ (I.take n))) (U.evaluate (Vector.cast ⋯ (I.take n'))) }

Equations

• Apply.oapply op O U = match Apply.apply_helper✝ op O U Apply.initial✝ ⋯ with | ⟨(state, root), ⋯⟩ => ⟨state.size, ⟨⟨{ heap := RawBdd.cook_heap state.heap ⋯, root := root.cook ⋯ }, ⋯⟩, ⋯⟩⟩