Theorem: bitvec_AndOrXor_2663 (Eval/bitvec_AndOrXor_2663.lean)

State before:
⊢ ∀ (a b : BitVec 64), (xor (decide (a ≤ b)) (a != b) = true) = (b ≤ a)
Tactic:
intros
State after:
a✝ b✝ : BitVec 64
⊢ (xor (decide (a✝ ≤ b✝)) (a✝ != b✝) = true) = (b✝ ≤ a✝)

State before:
a✝ b✝ : BitVec 64
⊢ (xor (decide (a✝ ≤ b✝)) (a✝ != b✝) = true) = (b✝ ≤ a✝)
Tactic:
bv_decide
State after:
no goals