***( This file is part of the Maude 2 interpreter. Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. ) *** *** Strict total ordering on terms of a given kind. *** Version 2.3. *** fmod TERM-ORDER{X :: TRIV} is protecting EXT-BOOL . protecting CONVERSION . protecting META-LEVEL . vars E F : [X$Elt] . vars Q P : Qid . vars A B : NeTermList . vars C D : TermList . vars T U : Term . op lt : [X$Elt] [X$Elt] -> Bool . eq lt(E, F) = $lt(upTerm(E), upTerm(F)) . op $lt : TermList TermList -> Bool . eq $lt(Q, P) = string(Q) < string(P) . eq $lt(Q[A], P) = $lt(Q, P) . eq $lt(Q, P[B]) = $lt(Q, P) or-else Q == P . eq $lt(Q[A], P[B]) = if Q == P then $lt(A, B) else $lt(Q, P) fi . eq $lt(empty, B) = true . eq $lt(C, empty) = false . eq $lt((T, C), (U, D)) = if T == U then $lt(C, D) else $lt(T, U) fi . endfm