module module

`IndisputableMonolith.Complexity.SAT.PC`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Complexity.SAT.Completeness module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Complexity.SAT.CNF module_import
IndisputableMonolith.Complexity.SAT.XOR module_import

declarations in this module (23)

inductive Constraint L10
def mentionsVarLit L16
def mentionsVarClause L22
def mentionsVarXOR L26
def mentionsVar L30
def satisfiesConstraint L36
def determinesVar L43
def constraintsOf L51
abbrev InputSet L55
def PC L61
structure PeelingData L74
def PeelingWitness L88
def ForcedArborescence L105
abbrev ForcedArborescenceWitness L111
def programGoal_pc_iff_arborescence L117
def extractFromPC L122
structure PeelingResult L137
def buildPeelingResult L154
theorem pc_implies_peeling L229
theorem peeling_implies_arborescence L245
theorem arborescence_implies_peeling L253
theorem peeling_iff_arborescence L260
theorem pc_implies_forcedArborescence L267