1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
\section{The Theory {\tt add}}
The theory \ml{add}\index{add, theory@{\ptt add}, theory} contains an
\adhoc\ collection of
theorems about addition. It contains no new definitions.
The theorems that have been pre-proved in this theory include but are not
restricted to the following:
\begin{hol}
\index{LESS\_EQ\_ADD1@{\ptt LESS\_EQ\_ADD1}}
\index{ADD\_SYM\_ASSOC@{\ptt ADD\_SYM\_ASSOC}}
\index{LESS\_EQ\_SPLIT@{\ptt LESS\_EQ\_SPLIT}}
\index{ADDL\_GREATER@{\ptt ADDL\_GREATER}}
\index{LESS\_ADD1@{\ptt LESS\_ADD1}}
\begin{verbatim}
LESS_EQ_ADD1 |- !p n. p <= (n + p)
ADD_SYM_ASSOC |- !a b c. a + (b + c) = b + (a + c)
LESS_EQ_SPLIT |- !m n p. (m + n) <= p ==> n <= p /\ m <= p
ADDL_GREATER |- !m n p. m < n ==> m < (p + n)
LESS_ADD1 |- !a. a < (a + 1)
\end{verbatim}\end{hol}
|
