[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] lexigraphical ordering




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