@[reducible, inline]

abbrev Count.Solution {n m : ℕ} (O : OBdd n m) : Type

Equations

• Count.Solution O = { I : Vector Bool n // O.evaluate I = true }

@[instance_reducible]

instance Count.instVectorFintype {α : Type u_1} [Fintype α] {n : ℕ} : Fintype (Vector α n)

Equations

• Count.instVectorFintype = Fintype.ofEquiv (List.Vector α n) Count.my_vector_equiv_vector✝

@[instance_reducible]

instance Count.instFintypeSolution {n m : ℕ} {O : OBdd n m} : Fintype (Solution O)

Equations

• Count.instFintypeSolution = Subtype.fintype fun (I : Vector Bool n) => O.evaluate I = true

@[reducible, inline]

abbrev Count.numSolutions {n m : ℕ} (O : OBdd n m) : ℕ

Equations

• Count.numSolutions O = Fintype.card (Count.Solution O)

def Count.count {n m : ℕ} (O : OBdd n m) : ℕ

Equations

• Count.count O = (Count.count_helper✝ O ∅)[O.bdd.root]!

theorem Count.count_correct {n m : ℕ} {O : OBdd n m} : count O = numSolutions O