Is there any way to suggest or impose a lexigraphical ordering on PVS terms? Perhaps using strategies? I would like to apply a rule such as: set(a,set(b,x)) = set(b,set(a,x)) but only if I can establish that 'a' is somehow smaller than 'b'. I would like to avoid a logical ordering, as that seems to lead to excessive case-splitting. Dave Greve