Simultaneous switching for finite formula collections -- definitions

These are finite, nonuniform collections indexed by Fin formulaCount; they are unrelated to uniform circuit-family generators.

noncomputable def Complexity.DNF.switchingAnyBad {formulaCount N : ℕ} (formulas : Fin formulaCount → DNF N) (queryCount : ℕ) (restriction : Restriction.On N) : Prop

At least one DNF in a finite collection has a deep switching tree.

Equations

• Complexity.DNF.switchingAnyBad formulas queryCount restriction = ∃ (index : Fin formulaCount), (formulas index).switchingBad queryCount restriction

@[implicit_reducible]

noncomputable instance Complexity.DNF.switchingAnyBadDecidable {formulaCount N : ℕ} (formulas : Fin formulaCount → DNF N) (queryCount : ℕ) : DecidablePred (switchingAnyBad formulas queryCount)

Equations

• Complexity.DNF.switchingAnyBadDecidable formulas queryCount restriction = id inferInstance

noncomputable def Complexity.DNF.consistentParts {formulaCount N : ℕ} (formulas : Fin formulaCount → DNF N) : Fin formulaCount → DNF N

Clean every DNF in a finite collection.

Equations

• Complexity.DNF.consistentParts formulas index = (formulas index).consistentPart

noncomputable def Complexity.CNF.switchingAnyBad {formulaCount N : ℕ} (formulas : Fin formulaCount → CNF N) (queryCount : ℕ) (restriction : Restriction.On N) : Prop

At least one CNF in a finite collection has a deep switching tree.

Equations

• Complexity.CNF.switchingAnyBad formulas queryCount restriction = ∃ (index : Fin formulaCount), (formulas index).switchingBad queryCount restriction

@[implicit_reducible]

noncomputable instance Complexity.CNF.switchingAnyBadDecidable {formulaCount N : ℕ} (formulas : Fin formulaCount → CNF N) (queryCount : ℕ) : DecidablePred (switchingAnyBad formulas queryCount)

Equations

• Complexity.CNF.switchingAnyBadDecidable formulas queryCount restriction = id inferInstance

noncomputable def Complexity.CNF.consistentParts {formulaCount N : ℕ} (formulas : Fin formulaCount → CNF N) : Fin formulaCount → CNF N

Clean every CNF in a finite collection.

Equations

• Complexity.CNF.consistentParts formulas index = (formulas index).consistentPart