# Bachmair and Ganzinger, ordering of equations

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical one in the overall attempt to get to the point where equations can be applied in one direction, thereby dramatically improving the performance of automated reasoning on problems involving equality.)

If $$s \succ t \succ u$$

Let $$s\approx t$$ have the multiset representation $$\{\{s\},\{t\}\}$$

Let $$s\not\approx t$$ have the multiset representation $$\{\{s,\bot\},\{t,\bot\}\}$$ where $$\bot$$ is a new symbol such that every existing symbol is greater than $$\bot$$.

Then $$s\not\approx u \succ s\approx t$$ even though $$t \succ u$$.

... wait, how? Sure, $$s\not\approx u$$ also contains a couple of occurrences of $$\bot$$, but what of that? $$t \succ u \succ \bot$$, so the comparison should be decided by $$t$$ vs. $$u$$; $$\bot$$ should not have enough weight to tip the balance, so to speak.

What am I missing?

(I have seen later writing that gives $$s\not\approx t$$ the multiset representation $$\{\{s,s\},\{t,t\}\}$$, and I see how this solves the problem, but I don't see how it is solved in the original version.)

• Technically the $\{\{s\},\{t\}\}$ representation is a multiset of multisets representation. Might be worth noting to avoid any confusion. – Dmitri Chubarov Jan 13 at 7:58

1. Let $$M = \{s,\bot\}$$ and $$N=\{s\}$$. We have $$M\succ M$$ since $$M(\bot) > N(\bot)$$ and there does not exist $$x$$ such that $$N(x)> M(x)$$.
2. Let $$M=\{\{s,\bot\},\{u,\bot\}\}$$ and $$N=\{\{s\},\{t\}\}$$. We have $$M(\{s,\bot\})>N(\{s,\bot\})$$ and by (1) $$\{s,\bot\}\succ\{s\}$$. Therefore $$M\succ N$$.