Theorem: bitvec_AndOrXor_2581__BAB___A__B (Eval/bitvec_AndOrXor_2581__BAB___A__B.lean)

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

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