Exclusive or in De Morgan synthesis #
Exclusive or of two available functions costs four De Morgan gates:
x ⊕ y = (x ∨ y) ∧ ¬(x ∧ y), sharing nothing beyond the two arguments.
Synthesis.xor_of_mem comes from Cslib.Computability.Circuit.Boolean.Synthesis at commit
2a4389b of the author's CSLib fork (branch complexitylib-integration); upstream CSLib does not
have it. This file lives in Complexitylib/Cslib/ because it extends CSLib types in their home
namespace Cslib.Circuits; its contents are candidates for upstreaming to CSLib.
theorem
Cslib.Circuits.Synthesis.xor_of_mem
{n : ℕ}
{s : Set (BooleanFunction n)}
{f g : BooleanFunction n}
(hf : f ∈ s)
(hg : g ∈ s)
:
XOR costs four gates when its two arguments are already available. The intermediate conjunction and disjunction are shared.