Theorem: bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2 (Eval/bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2.lean)

State before:
⊢ ∀ (x C1 C : BitVec 64), x ^^^ C1 ||| C = (x ||| C) ^^^ C1 &&& ~~~C
Tactic:
intros
State after:
x✝ C1✝ C✝ : BitVec 64
⊢ x✝ ^^^ C1✝ ||| C✝ = (x✝ ||| C✝) ^^^ C1✝ &&& ~~~C✝

State before:
x✝ C1✝ C✝ : BitVec 64
⊢ x✝ ^^^ C1✝ ||| C✝ = (x✝ ||| C✝) ^^^ C1✝ &&& ~~~C✝
Tactic:
bv_decide
State after:
no goals