Theorem: bitvec_AddSub_1152 (Eval/bitvec_AddSub_1152.lean)

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

State before:
y✝ x✝ : BitVec 1
⊢ x✝ + y✝ = x✝ ^^^ y✝
Tactic:
bv_decide
State after:
no goals