Theorem: bitvec_AndOrXor_1253_A__AB___A__B (Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean)

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

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