Theorem: bitvec_AddSub_1624 (Eval/bitvec_AddSub_1624.lean)

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

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