Theorem: bitvec_AddSub_1043 (Eval/bitvec_AddSub_1043.lean)

State before:
⊢ ∀ (C1 Z RHS : BitVec 64), (Z &&& C1 ^^^ C1) + 1 + RHS = RHS - (Z ||| ~~~C1)
Tactic:
intros
State after:
C1✝ Z✝ RHS✝ : BitVec 64
⊢ (Z✝ &&& C1✝ ^^^ C1✝) + 1 + RHS✝ = RHS✝ - (Z✝ ||| ~~~C1✝)

State before:
C1✝ Z✝ RHS✝ : BitVec 64
⊢ (Z✝ &&& C1✝ ^^^ C1✝) + 1 + RHS✝ = RHS✝ - (Z✝ ||| ~~~C1✝)
Tactic:
bv_decide
State after:
no goals