I'm reading this paper: http://www.lsi.upc.edu/~albert/papers/handbook.ps.gz
and I can't understand a part of it. it defines an ordering on multisets (it defines a multiset over $A$ as a function $A \rightarrow N$)
and says (page 13) multisets are ordered by the smallest irreflexive, transitive relation $\succ\succ$ such that $M \cup \{s\} \succ\succ N \cup \{t_1,\ldots,t_n\} \; \mbox{if} \; M==N \land s \succ t_i \; \forall i \in 1 \ldots n$
but later it says (page 24) $\{s, t\} \succ\succ \{u, v\}$ if $\\s > u \land (s \geq v \lor t \geq v) \;\lor\; s > v \land (s \geq u \lor t \geq u) \;\lor\\ t > u \land (s \geq v \lor t \geq v) \;\lor\; t > v \land (s \geq u \lor t \geq u)$
(by page 15, $>$ and $=$ are interpreted as a given total (up to $=_c$)reduction ordering $\succ$ and congruence $=_c$ respectively)
which would seem to make $\succ\succ$ not aymmetric, but it must be asymmetric as it is transitive and irreflexive
the problem is that it could be the case that $s > u \land s = v$ which would make $\{s, t\}$ greater but also $v > t \land s = v$ which would make $\{u, v\}$ greater if we apply the rule backwards
I guess it might be the case that this rule only works because of constraints on the multisets
The way the E theorem prover computes this seems to make sense:
int LiteralCompareFun(Eqn_p lit1, Eqn_p lit2) { int cmpres; if(EqnIsPositive(lit1) && !EqnIsPositive(lit2)) { return 1; } else if(!EqnIsPositive(lit1) && EqnIsPositive(lit2)) { return -1; } cmpres = PCmp(MAX(lit1->lterm, lit1->rterm), MAX(lit2->lterm, lit2->rterm)); if(cmpres) { return cmpres; } return PCmp(MIN(lit1->lterm, lit1->rterm), MIN(lit2->lterm, lit2->rterm)); }