Theorem: condFlipBit_apply_flipBit (Controlbits/BitResiduum.lean)

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

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (flipBit i) ((condFlipBit i c) q) = bif c (getRes i q) then q else (flipBit i) q
Tactic:
rcases (c (getRes i q)).dichotomy with h | h <;> rw [condFlipBit_apply, h]
State after:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ (flipBit i) (bif false then (flipBit i) q else q) = bif false then q else (flipBit i) q

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

State before:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ (flipBit i) (bif false then (flipBit i) q else q) = bif false then q else (flipBit i) q
Tactic:
simp_rw [cond_false]
State after:
no goals

State before:
case inr
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = true
⊢ (flipBit i) (bif true then (flipBit i) q else q) = bif true then q else (flipBit i) q
Tactic:
simp_rw [cond_true, flipBit_flipBit]
State after:
no goals