Theorem: bitvec_InstCombineShift__422_1 (Eval/bitvec_InstCombineShift__422_1.lean)

State before:
⊢ ∀ (Y X C : BitVec 31), (Y + X >>> C) <<< C = Y <<< C + X &&& (-1) <<< C
Tactic:
intros
State after:
Y✝ X✝ C✝ : BitVec 31
⊢ (Y✝ + X✝ >>> C✝) <<< C✝ = Y✝ <<< C✝ + X✝ &&& (-1) <<< C✝

State before:
Y✝ X✝ C✝ : BitVec 31
⊢ (Y✝ + X✝ >>> C✝) <<< C✝ = Y✝ <<< C✝ + X✝ &&& (-1) <<< C✝
Tactic:
bv_decide
State after:
no goals