xor_comm_cancel'
plain-language theorem explainer
The lemma establishes the Boolean identity (b ⊕ a) ⊕ b = a for exclusive-or. It is cited inside the correctness argument for recovering a missing variable value from an XOR constraint under a satisfying assignment. The proof is a one-line wrapper that exhausts the four cases on a and b then applies reflexivity.
Claim. For all Boolean values $a$ and $b$, $(b ⊕ a) ⊕ b = a$, where $⊕$ denotes exclusive-or.
background
The declaration sits inside the backpropagation module for SAT, whose local setting tracks partial assignments (none for unknown, some b for determined). It manipulates the Boolean XOR operation imported from the sibling XOR module and is independent of the CNF layer. No upstream lemmas are required; the identity is used only to simplify expressions inside later correctness statements.
proof idea
The proof is a one-line wrapper that applies the cases tactic to both a and b, then closes with reflexivity.
why it matters
It supplies the algebraic cancellation needed by the downstream theorem xorMissing_correct, which states that if a partial assignment is compatible with a satisfying assignment a and xorMissing returns some (v, b), then b equals a v. The result therefore closes the linear-algebra step (XOR over GF(2)) inside the backpropagation mechanism for partial assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.