Theorem: condFlipBit_succAbove_apply (Controlbits/BitResiduum.lean)

State before:
m : ℕ
c : BV (m + 1) → Bool
q : BV (m + 1 + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ (condFlipBit (j.succAbove i) c) q =
    mergeBitRes j (getBit j q) ((condFlipBit i fun p => c (mergeBitRes (i.predAbove j) (getBit j q) p)) (getRes j q))
Tactic:
simp_rw [condFlipBit_apply, getRes_succAbove,
Bool.apply_cond (fun x => mergeBitRes j (getBit j q) x), mergeBitRes_getBit_getRes,
flipBit_succAbove]
State after:
no goals