Theorem: bitvec_AndOrXor_1247_AB__AB__AB (Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean)

State before:
⊢ ∀ (A B : BitVec 64), (A &&& B ^^^ -1) &&& (A ||| B) = A ^^^ B
Tactic:
intros
State after:
A✝ B✝ : BitVec 64
⊢ (A✝ &&& B✝ ^^^ -1) &&& (A✝ ||| B✝) = A✝ ^^^ B✝

State before:
A✝ B✝ : BitVec 64
⊢ (A✝ &&& B✝ ^^^ -1) &&& (A✝ ||| B✝) = A✝ ^^^ B✝
Tactic:
bv_decide
State after:
no goals