Theorem: bitvec_InstCombineShift__476 (Eval/bitvec_InstCombineShift__476.lean)

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

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