Theorem: bitvec_AndOrXor_2607 (Eval/bitvec_AndOrXor_2607.lean)

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

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