Theorem: condFlipBit_apply_eq_mergeBitRes (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) q = mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q)
Tactic:
rw [condFlipBit_apply]
State after:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif c (getRes i q) then (flipBit i) q else q) = mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif c (getRes i q) then (flipBit i) q else q) = mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q)
Tactic:
cases (c (getRes i q))
State after:
case false
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif false then (flipBit i) q else q) = mergeBitRes i (xor false (getBit i q)) (getRes i q)

case true
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif true then (flipBit i) q else q) = mergeBitRes i (xor true (getBit i q)) (getRes i q)

State before:
case false
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif false then (flipBit i) q else q) = mergeBitRes i (xor false (getBit i q)) (getRes i q)
Tactic:
rw [cond_false, Bool.false_xor, mergeBitRes_getBit_getRes]
State after:
no goals

State before:
case true
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif true then (flipBit i) q else q) = mergeBitRes i (xor true (getBit i q)) (getRes i q)
Tactic:
rw [cond_true, Bool.true_xor, flipBit_apply]
State after:
no goals