----------------------------------------------------------------------
SBC_CONV                                                   (reduceLib)
----------------------------------------------------------------------
SBC_CONV : conv

SYNOPSIS
Calculates by inference the difference of two numerals.

LIBRARY
reduce

DESCRIBE
If {m} and {n} are numerals (e.g. {0}, {1}, {2}, {3},...), then
{SBC_CONV "m - n"} returns the theorem:

   |- m - n = s

where {s} is the numeral that denotes the difference of the natural
numbers denoted by {m} and {n}.

FAILURE
{SBC_CONV tm} fails unless {tm} is of the form  {"m - n"}, where {m} and
{n} are numerals.

EXAMPLE

#SBC_CONV "25 - 30";;
|- 25 - 30 = 0

#SBC_CONV "200 - 200";;
|- 200 - 200 = 0

#SBC_CONV "60 - 17";;
|- 60 - 17 = 43


----------------------------------------------------------------------