Theorem: bitvec_AddSub_1564 (Eval/bitvec_AddSub_1564.lean)

State before:
⊢ ∀ (x C : BitVec 64), C - (x ^^^ -1) = x + (C + 1)
Tactic:
intros
State after:
x✝ C✝ : BitVec 64
⊢ C✝ - (x✝ ^^^ -1) = x✝ + (C✝ + 1)

State before:
x✝ C✝ : BitVec 64
⊢ C✝ - (x✝ ^^^ -1) = x✝ + (C✝ + 1)
Tactic:
bv_decide
State after:
no goals