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

pc_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)

 229theorem pc_implies_peeling {n}
 230  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 231  PC inputs aRef φ H → PeelingWitness inputs aRef φ H := by

proof body

Term-mode proof.

 232  intro hPC
 233  let result := buildPeelingResult inputs aRef φ H hPC inputs (fun _ h => h)
 234  exact ⟨{
 235    vars := result.vars
 236    constrs := result.constrs
 237    nodup := result.nodup
 238    len_eq := result.len_eq
 239    cover := fun v => (result.cover v).symm
 240    step := result.step
 241  }⟩
 242
 243/-- Peeling ⇒ forced arborescence (Prop-level).
 244    Trivial since ForcedArborescence is defined as PeelingWitness. -/

used by (1)

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

depends on (17)

Lean names referenced from this declaration's body.