`pc_implies_forcedArborescence`

proved

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.PC
domain: Complexity
line: 267 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.PC on GitHub at line 267.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 264  exact Iff.rfl
 265
 266/-- PC ⇒ ForcedArborescence. -/
 267theorem pc_implies_forcedArborescence {n}
 268  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 269  PC inputs aRef φ H → ForcedArborescence inputs aRef φ H := by
 270  unfold ForcedArborescence
 271  exact pc_implies_peeling inputs aRef φ H
 272
 273end SAT
 274end Complexity
 275end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.