def Size.size {n m : ℕ} : OBdd n m → ℕ

Equations

• Size.size = List.length ∘ Collect.collect

theorem Size.isTerminal_iff_size_eq_zero {n m : ℕ} {O : OBdd n m} : size O = 0 ↔ O.isTerminal

def Size.bool_of_size_eq_zero {n m : ℕ} (O : OBdd n m) (h : size O = 0) : Bool

Equations

• Size.bool_of_size_eq_zero O h = match O_root_def : (↑O).root with | Pointer.terminal b => b | Pointer.node a => ⋯.elim

theorem Size.size_spec {n m : ℕ} {O : OBdd n m} : size O = O.size

theorem Size.size_node_le {n m : ℕ} {j : Fin m} {O : OBdd n m} {h : (↑O).root = Pointer.node j} : size O ≤ 1 + size (O.low h) + size (O.high h)

@[irreducible]

theorem Size.size_le_helper {n m : ℕ} {O : OBdd n m} : size O ≤ 2 ^ (n - ↑(↑O).var) - 1

theorem Size.size_le {n m : ℕ} {O : OBdd n m} : size O ≤ 2 ^ n - 1