Theorem: condFlipBit_mergeBitRes (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
b : Bool
p : BV a✝
⊢ (condFlipBit i c) (mergeBitRes i b p) = mergeBitRes i (xor (c p) b) p
Tactic:
rw [condFlipBit_apply_eq_mergeBitRes, getRes_mergeBitRes, getBit_mergeBitRes]
State after:
no goals