Player-swapping semantics

Swapping the speakers swaps the two inputs to the run. This gives the complemented-function protocol with unchanged message and round bounds.

theorem Complexity.KarchmerWigderson.RoundProtocol.run_swapPlayers_internal {ι : Type u_1} {M : Type u_2} {d : ℕ} (P : RoundProtocol ι M d) (x y : ι → Bool) : P.swapPlayers.run x y = P.run y x

theorem Complexity.KarchmerWigderson.RoundProtocol.SolvesKW.swapPlayers_internal {ι : Type u_1} {M : Type u_2} {d : ℕ} {P : RoundProtocol ι M d} {f : (ι → Bool) → Bool} (h : P.SolvesKW f) : P.swapPlayers.SolvesKW fun (x : ι → Bool) => !f x