pith. machine review for the scientific record. sign in
theorem proved term proof

arborescence_implies_peeling

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

formal statement (Lean)

 253theorem arborescence_implies_peeling {n}
 254  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 255  ForcedArborescence inputs aRef φ H → PeelingWitness inputs aRef φ H := by

proof body

Term-mode proof.

 256  unfold ForcedArborescence
 257  exact id
 258
 259/-- Peeling ↔ Arborescence equivalence. -/

depends on (12)

Lean names referenced from this declaration's body.