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

peeling_implies_arborescence

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)

 245theorem peeling_implies_arborescence {n}
 246  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 247  PeelingWitness inputs aRef φ H → ForcedArborescence inputs aRef φ H := by

proof body

Term-mode proof.

 248  unfold ForcedArborescence
 249  exact id
 250
 251/-- Arborescence ⇒ peeling (Prop-level).
 252    Trivial since ForcedArborescence is defined as PeelingWitness. -/

depends on (17)

Lean names referenced from this declaration's body.