Lines Matching defs:of
3 This manual describes the use of the \ml{reduce} library, as well as discussing
4 its design. The library is intended to ease the burden of performing tedious
5 and intellectually trivial tasks of arithmetic such as proving:
12 tediousness. However, using the \ml{reduce} library, the evaluation of:
20 of certain boolean expressions. This is mainly for the sake of completeness,
21 since the same effect can be achieved by careful use of rewriting.
24 \section{The representation of numbers}
27 conversion \ml{num\_CONV} which generates the definition of any nonzero numeral
28 in terms of its predecessor, for example:
50 The following is an example of an algorithm for reducing addition expressions.
51 In fact, for reasons of efficiency, the library's \ml{ADD\_CONV} conversion is
53 general flavour of how the various arithmetic conversions are defined. Suppose
59 conjunct of the inbuilt definition \ml{ADD}:
72 where \ml{p} is the predecessor of \ml{m}, and \ml{s} the corresponding sum.
77 |- (SUC p) + n = SUC(p + n) % [2] Instance of 2nd conjunct of ADD %
122 to \ml{REDUCE\_CONV} to subterms of the theorem's conclusion
129 operator, for example \ml{ADD\_CONV} and \ml{OR\_CONV}. For more details of