`peeling_iff_arborescence`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

 257  exact id
 258
 259/-- Peeling ↔ Arborescence equivalence. -/
 260theorem peeling_iff_arborescence {n}
 261  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 262  PeelingWitness inputs aRef φ H ↔ ForcedArborescence inputs aRef φ H := by
 263  unfold ForcedArborescence
 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.