Theorem: bitvec_InstCombineShift__458 (Eval/bitvec_InstCombineShift__458.lean)

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

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