Theorem: bitvec_AddSub_1202 (Eval/bitvec_AddSub_1202.lean)

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

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