Theorem: bitvec_InstCombineShift__422_2 (Eval/bitvec_InstCombineShift__422_2.lean)

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

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