Theorem: condFlipBit_succ_apply (Controlbits/BitResiduum.lean)

State before:
m : ℕ
c : BV (m + 1) → Bool
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ (condFlipBit i.succ c) q =
    mergeBitRes 0 (getBit 0 q) ((condFlipBit i fun p => c (mergeBitRes 0 (getBit 0 q) p)) (getRes 0 q))
Tactic:
simp_rw [condFlipBit_apply_eq_mergeBitRes, mergeBitRes_succ, getRes_succ, getBit_succ,
getBit_mergeBitRes, getRes_mergeBitRes]
State after:
no goals