@[irreducible]

def Evaluate.evaluate {n m : ℕ} (O : OBdd n m) : Vector Bool n → Bool

Equations

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

@[irreducible]

theorem Evaluate.evaluate_evaluate {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} : evaluate O = O.evaluate

theorem Evaluate.evaluate_terminal {n m : ℕ} {b : Bool} {O : OBdd n m} : (↑O).root = Pointer.terminal b → evaluate O = Function.const (Vector Bool n) b

theorem Evaluate.evaluate_node {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) : evaluate O = fun (I : Vector Bool n) => if I[(↑O).heap[j].var] = true then evaluate (O.high h) I else evaluate (O.low h) I