Theorem: bitvec_AndOrXor_2587__BAA___B__A (Eval/bitvec_AndOrXor_2587__BAA___B__A.lean)

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

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