GT_CONV
reduceLib.GT_CONV : conv
Proves result of greater-than ordering on two numerals.
If m and n are both numerals (e.g. 0, 1, 2, 3,...) of type
:num, then GT_CONV "m > n" returns the theorem:
|- (m > n) = T
if the natural number denoted by m is greater than that denoted by
n, or
|- (m > n) = F
otherwise.
Failure
GT_CONV tm fails unless tm is of the form ``m > n``, where
m and n are numerals of type :num.
Example
> GT_CONV ``100 > 10``;
val it = |- 100 > 10 <=> T : thm
> GT_CONV ``15 > 15``;
val it = |- 15 > 15 <=> F : thm
> GT_CONV ``11 > 27``;
val it = |- 11 > 27 = F : thm