Theorem: bitvec_AddSub_1309 (Eval/bitvec_AddSub_1309.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