def Choice.choice {n m : ℕ} (O : OBdd n m) : (∃ (I : Vector Bool n), O.evaluate I = true) → Vector Bool n

Equations

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

@[simp]

def Choice.choice_evaluate {n m : ℕ} {O : OBdd n m} (hr : O.Reduced) (ht : ∃ (I : Vector Bool n), O.evaluate I = true) : O.evaluate (choice O ht) = true

Equations

• ⋯ = ⋯