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

Equations

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

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.bdd.root = Pointer.node j} : size O ≤ 1 + size (O.low h) + size (O.high h)

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