79inductive BPStep {n} (φ : CNF n) (H : XORSystem n) : BPState n → BPState n → Prop 80 | xor_push 81 {s : BPState n} 82 (X : XORConstraint n) 83 (v : Var n) 84 (b : Bool) 85 (hX : X ∈ H) 86 (hmiss : xorMissing s.assign X = some (v, b)) 87 : BPStep φ H s { assign := setVar s.assign v b }
proof body
Definition body.
88 | clause_unit 89 {s : BPState n} 90 (C : Clause n) 91 (v : Var n) 92 (b : Bool) 93 (hC : C ∈ φ.clauses) 94 (hmiss : clauseUnit s.assign C = some (v, b)) 95 : BPStep φ H s { assign := setVar s.assign v b } 96 -- Additional gate placeholders (to be refined with circuit semantics): 97 | and_one {s : BPState n} : BPStep φ H s s 98 | and_zero {s : BPState n} : BPStep φ H s s 99 | or_one {s : BPState n} : BPStep φ H s s 100 | or_zero {s : BPState n} : BPStep φ H s s 101 | not_flip {s : BPState n} : BPStep φ H s s 102 | wire_prop {s : BPState n} : BPStep φ H s s 103 104/-- Predicate: state is complete (all variables determined). -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.