122noncomputable def extractFromPC {n : Nat} (inputs : InputSet n) (aRef : Assignment n) 123 (φ : CNF n) (H : XORSystem n) (hPC : PC inputs aRef φ H) 124 (U : Finset (Var n)) (hU : U ⊆ inputs) (hne : U.Nonempty) : 125 { p : Constraint n × Var n // 126 p.1 ∈ constraintsOf φ H ∧ 127 p.2 ∈ U ∧ 128 mentionsVar p.1 p.2 = true ∧ 129 (∀ w ∈ U, w ≠ p.2 → mentionsVar p.1 w = false) ∧ 130 determinesVar aRef p.1 p.2 } := by
proof body
Definition body.
131 have h := hPC U hU hne 132 choose K hK using h 133 choose v hv using hK.2 134 exact ⟨(K, v), hK.1, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2⟩ 135 136/-- Bundled result type for peeling construction. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.