NUM_REL_CONV : term -> thm

SYNOPSIS

Performs relational operation on natural number numerals by proof.

DESCRIPTION

When applied to a term that is a relational operator application `m < n`, `m <= n`, `m > n`, `m >= n` or `m = n` applied to numerals m and n, the conversion NUM_REL_CONV will `reduce' it and return a theorem asserting its equality to `T` or `F` as appropriate.

FAILURE CONDITIONS

NUM_REL_CONV tm fails if tm is not of one of the forms specified.

EXAMPLE

  # NUM_REL_CONV `1089 < 2231`;;
  val it : thm = |- 1089 < 2231 <=> T

  # NUM_REL_CONV `1089 >= 2231`;;
  val it : thm = |- 1089 >= 2231 <=> F

Note that the immediate operands must be numerals. For deeper reduction of combinations of numerals, use NUM_REDUCE_CONV.

  # NUM_REL_CONV `2 + 2 = 4`;;
  Exception: Failure "REWRITES_CONV".

  # NUM_REDUCE_CONV `2 + 2 = 4`;;
  val it : thm = |- 2 + 2 = 4 <=> T