1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
\contentsline {chapter}{\numberline {1}The more\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}arithmetic Library}{3}
\contentsline {section}{\numberline {1.1}The Theory {\ptt more\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}arithmetic}}{3}
\contentsline {section}{\numberline {1.2}The Theory {\ptt ineq}}{4}
\contentsline {section}{\numberline {1.3}The Theory {\ptt zero\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}ineq}}{4}
\contentsline {section}{\numberline {1.4}The Theory {\ptt suc}}{4}
\contentsline {section}{\numberline {1.5}The Theory {\ptt pre}}{5}
\contentsline {section}{\numberline {1.6}The Theory {\ptt add}}{5}
\contentsline {section}{\numberline {1.7}The Theory {\ptt sub}}{5}
\contentsline {section}{\numberline {1.8}The Theory {\ptt mult}}{6}
\contentsline {section}{\numberline {1.9}The Theory {\ptt div\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}mod}}{6}
\contentsline {section}{\numberline {1.10}The Theory {\ptt min\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}max}}{6}
\contentsline {section}{\numberline {1.11}The Theory {\ptt odd\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}even}}{7}
\contentsline {section}{\numberline {1.12}Using the Library}{7}
\contentsline {subsection}{\numberline {1.12.1}An Example of a Session}{8}
\contentsline {subsection}{\numberline {1.12.2}The {\ptt load\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}more\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}arithmetic} Function}{9}
\contentsline {chapter}{\numberline {2}ML Functions in the more\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}arithmetic Library}{11}
\contentsline {chapter}{\numberline {3}Pre-proved Theorems}{15}
\contentsline {section}{\numberline {3.1}Theorems about Inequalities}{15}
\contentsline {section}{\numberline {3.2}Theorems about {\ptt 0}}{15}
\contentsline {section}{\numberline {3.3}Theorems about {\ptt SUC}}{16}
\contentsline {section}{\numberline {3.4}Theorems about {\ptt PRE}}{17}
\contentsline {section}{\numberline {3.5}Theorems about Addition}{17}
\contentsline {section}{\numberline {3.6}Theorems about Subtraction}{19}
\contentsline {section}{\numberline {3.7}Theorems about Multiplication and Exponential Functions}{22}
\contentsline {section}{\numberline {3.8}Theorems about Division}{22}
\contentsline {section}{\numberline {3.9}Theorems about Maximum and Minimum}{23}
\contentsline {section}{\numberline {3.10}Theorems about Odd and Even Numbers}{24}
\contentsline {chapter}{Index}{25}
|
