def
definition
def or abbrev
satisfiesSystem
show as:
view Lean formalization →
formal statement (Lean)
26def satisfiesSystem {n} (a : Assignment n) (H : XORSystem n) : Prop :=
proof body
Definition body.
27 ∀ c ∈ H, satisfiesXOR a c
28
29/-! ## XOR Parity Lemmas -/
30
31/-- XOR is self-inverse: a ⊕ a = false -/
32@[simp] lemma Bool.xor_self (a : Bool) : Bool.xor a a = false := by cases a <;> rfl
33
34/-- XOR with false is identity -/
35@[simp] lemma Bool.xor_false' (a : Bool) : Bool.xor a false = a := by cases a <;> rfl
36
37/-- false XOR a = a -/
38@[simp] lemma Bool.false_xor (a : Bool) : Bool.xor false a = a := by cases a <;> rfl
39
40/-- XOR is commutative -/
41lemma Bool.xor_comm (a b : Bool) : Bool.xor a b = Bool.xor b a := by cases a <;> cases b <;> rfl
42
43/-- XOR is associative -/
44lemma Bool.xor_assoc (a b c : Bool) : Bool.xor (Bool.xor a b) c = Bool.xor a (Bool.xor b c) := by
45 cases a <;> cases b <;> cases c <;> rfl
46
47/-- XOR cancellation: (a ⊕ b) ⊕ b = a -/
48@[simp] lemma Bool.xor_xor_cancel_right (a b : Bool) : Bool.xor (Bool.xor a b) b = a := by
49 cases a <;> cases b <;> rfl
50
51/-- Parity of empty list is false -/