Theorem: bitvec_AndOrXor_2617 (Eval/bitvec_AndOrXor_2617.lean)

State before:
⊢ ∀ (a b : BitVec 64), a &&& (b ^^^ -1) ^^^ (a ^^^ -1) &&& b = a ^^^ b
Tactic:
intros
State after:
a✝ b✝ : BitVec 64
⊢ a✝ &&& (b✝ ^^^ -1) ^^^ (a✝ ^^^ -1) &&& b✝ = a✝ ^^^ b✝

State before:
a✝ b✝ : BitVec 64
⊢ a✝ &&& (b✝ ^^^ -1) ^^^ (a✝ ^^^ -1) &&& b✝ = a✝ ^^^ b✝
Tactic:
bv_decide
State after:
no goals