Theorem: bitvec_InstCombineShift__440 (Eval/bitvec_InstCombineShift__440.lean)

State before:
⊢ ∀ (Y X C C2 : BitVec 64), (Y ^^^ X >>> C &&& C2) <<< C = X &&& C2 <<< C ^^^ Y <<< C
Tactic:
intros
State after:
Y✝ X✝ C✝ C2✝ : BitVec 64
⊢ (Y✝ ^^^ X✝ >>> C✝ &&& C2✝) <<< C✝ = X✝ &&& C2✝ <<< C✝ ^^^ Y✝ <<< C✝

State before:
Y✝ X✝ C✝ C2✝ : BitVec 64
⊢ (Y✝ ^^^ X✝ >>> C✝ &&& C2✝) <<< C✝ = X✝ &&& C2✝ <<< C✝ ^^^ Y✝ <<< C✝
Tactic:
bv_decide
State after:
no goals