\begin{theindex}

  \item {\ptt add}, theory, 5
  \item {\ptt ADD\_DIV\_ADD\_DIV}, 6, 22
  \item {\ptt ADD\_DIV\_SUC\_DIV}, 22
  \item {\ptt ADD\_EQ\_IMP\_SUB\_EQ}, 19
  \item {\ptt ADD\_EQ\_LESS\_EQ}, 18
  \item {\ptt ADD\_EQ\_LESS\_IMP\_LESS}, 18
  \item {\ptt ADD\_GREATER\_EQ}, 18
  \item {\ptt ADD\_LESS\_EQ\_SUB}, 19
  \item {\ptt ADD\_MONO\_LESS}, 18
  \item {\ptt ADD\_SUB\_SYM}, 5, 19
  \item {\ptt ADD\_SUC\_0}, 18
  \item {\ptt ADD\_SYM\_ASSOC}, 5, 18
  \item {\ptt ADDL\_GREATER}, 5, 17
  \item {\ptt ADDL\_GREATER\_EQ}, 17
  \item {\ptt ADDR\_GREATER}, 17
  \item {\ptt ADDR\_GREATER\_EQ}, 18

  \indexspace

  \item {\ptt DIV}, 6
  \item {\ptt DIV\_DIV\_DIV\_MULT}, 22
  \item {\ptt DIV\_ONE}, 22
  \item {\ptt div\_mod}, theory, 6

  \indexspace

  \item {\ptt EQ\_LESS\_EQ}, 4
  \item {\ptt EVEN}, 7
  \item {\ptt EVEN\_IMPL\_MULT}, 7
  \item {\ptt EVEN\_MULT}, 24
  \item {\ptt EVEN\_ODD\_0}, 7, 24
  \item {\ptt EVEN\_ODD\_PLUS\_CASES}, 24
  \item {\ptt EVEN\_ODD\_SUC}, 7, 24
  \item {\ptt EXP1}, 22

  \indexspace

  \item {\ptt GEN\_INDUCT\_RULE}, 11
  \item {\ptt GEN\_INDUCT\_TAC}, 12
  \item {\ptt GEN\_INDUCTION}, 15
  \item {\ptt GREATER\_EQ\_ANTISYM}, 15
  \item {\ptt GREATER\_EQ\_SPLIT}, 18
  \item {\ptt GREATER\_EQ\_SUB\_LESS\_TO\_ADD}, 19
  \item {\ptt GREATER\_NOT\_ZERO}, 4, 15

  \indexspace

  \item {\ptt ineq}, theory, 4

  \indexspace

  \item {\ptt LEFT\_SUB\_DISTRIB}, 6
  \item {\ptt LESS1EQ0}, 4, 16
  \item {\ptt LESS\_ADD1}, 5, 18
  \item {\ptt LESS\_ADD\_ASSOC}, 18
  \item {\ptt LESS\_DIV\_EQ\_ZERO}, 22
  \item {\ptt LESS\_EQ\_0\_EQ}, 4, 16
  \item {\ptt LESS\_EQ\_ADD1}, 5, 18
  \item {\ptt LESS\_EQ\_ADD\_SUB1}, 19
  \item {\ptt LESS\_EQ\_LESS\_EQ\_EQ}, 4, 15
  \item {\ptt LESS\_EQ\_LESS\_SUC}, 16
  \item {\ptt LESS\_EQ\_MONO\_ADD\_EQ0}, 18
  \item {\ptt LESS\_EQ\_MONO\_ADD\_EQ1}, 18
  \item {\ptt LESS\_EQ\_MONO\_DIV}, 22
  \item {\ptt LESS\_EQ\_SPLIT}, 5, 18
  \item {\ptt LESS\_EQ\_SUB\_1}, 19
  \item {\ptt LESS\_EQ\_SUB\_ADD}, 20
  \item {\ptt LESS\_IMP\_LESS\_EQ\_PRE}, 17
  \item {\ptt LESS\_IS\_NOT\_LESS\_OR\_EQ}, 15
  \item {\ptt LESS\_LESS\_EQ}, 18
  \item {\ptt LESS\_LESS\_EQ\_MONO}, 19
  \item {\ptt LESS\_LESS\_MONO}, 19
  \item {\ptt LESS\_MONO\_MULT1}, 6, 22
  \item {\ptt LESS\_MULT\_PLUS\_DIFF}, 6, 22
  \item {\ptt LESS\_PRE}, 20
  \item {\ptt LESS\_SUB\_IMP\_INV}, 20
  \item {\ptt LESS\_SUB\_IMP\_SUM\_LESS}, 20
  \item {\ptt LESS\_SUB\_TO\_ADDL\_LESS}, 20
  \item {\ptt LESS\_SUB\_TO\_ADDR\_LESS}, 20
  \item {\ptt LESS\_TRANS\_ADD}, 19
  \item {\ptt LESS\_TWICE\_IMP\_LESS\_SUB}, 20
  \item {\ptt load\_more\_arithmetic}, 9

  \indexspace

  \item {\ptt M\_LESS\_0\_LESS}, 4, 16
  \item {\ptt MAX}, 6
  \item {\ptt MAX\_0}, 7, 23
  \item {\ptt MAX\_DEF}, 6, 23
  \item {\ptt MAX\_REFL}, 7, 23
  \item {\ptt MAX\_SUC}, 23
  \item {\ptt MAX\_SYM}, 7, 23
  \item {\ptt MIN}, 6
  \item {\ptt MIN\_0}, 7, 23
  \item {\ptt MIN\_DEF}, 6, 23
  \item {\ptt min\_max}, theory, 6
  \item {\ptt MIN\_REFL}, 7, 23
  \item {\ptt MIN\_SUC}, 24
  \item {\ptt MIN\_SYM}, 7, 24
  \item {\ptt MOD}, 6
  \item {\ptt MOD\_MULT\_MOD}, 6, 23
  \item {\ptt more\_arithmetic}, theory, 3
  \item {\ptt mult}, theory, 6
  \item {\ptt MULT\_DIV}, 23
  \item {\ptt MULT\_EVEN}, 24
  \item {\ptt MULT\_ODD}, 24

  \indexspace

  \item {\ptt NOT\_0\_AND\_MORE}, 4, 16
  \item {\ptt NOT\_0\_GREATER\_EQ\_SUC}, 16
  \item {\ptt NOT\_0\_SUB}, 5, 20
  \item {\ptt NOT\_1\_TWICE}, 19
  \item {\ptt NOT\_ADD\_LESS}, 19
  \item {\ptt NOT\_EQ\_0}, 4, 16
  \item {\ptt NOT\_EQ\_LESS\_EQ}, 4, 15
  \item {\ptt NOT\_EVEN\_ODD\_SUC\_EVEN\_ODD}, 24
  \item {\ptt NOT\_FORALL\_SUC\_LESS\_EQ}, 16
  \item {\ptt NOT\_LESS\_AND\_GREATER}, 15
  \item {\ptt NOT\_LESS\_IMP\_LESS\_EQ\_ADD1}, 19
  \item {\ptt NOT\_LESS\_SUB}, 20
  \item {\ptt NOT\_MULT\_LESS\_0}, 22
  \item {\ptt NOT\_SUB\_0}, 20
  \item {\ptt NOT\_SUC\_LESS\_EQ\_0}, 4
  \item {\ptt NOT\_SUC\_LESS\_EQ\_SELF}, 4, 16
  \item {\ptt NUM\_EQ\_PLUS\_CONV}, 12
  \item {\ptt NUM\_LESS\_EQ\_PLUS\_CONV}, 13
  \item {\ptt NUM\_LESS\_PLUS\_CONV}, 13

  \indexspace

  \item {\ptt ODD}, 7
  \item {\ptt ODD\_MULT}, 24
  \item {\ptt odd\_even}, theory, 7
  \item {\ptt ONE\_LESS\_EQ\_TWO\_EXP}, 22
  \item {\ptt ONE\_LESS\_TWO\_EXP\_SUC}, 6, 22

  \indexspace

  \item {\ptt pre}, theory, 5
  \item {\ptt PRE\_ADD}, 5, 17
  \item {\ptt PRE\_K\_K}, 5, 17
  \item {\ptt PRE\_LESS}, 17
  \item {\ptt PRE\_LESS\_EQ}, 5, 17
  \item {\ptt PRE\_LESS\_LESS\_SUC}, 20
  \item {\ptt PRE\_MONO}, 5, 17
  \item {\ptt PRE\_MONO\_LESS\_EQ}, 17
  \item {\ptt PRE\_SUB\_SUC}, 20

  \indexspace

  \item {\ptt SMALLER\_SUM}, 20
  \item {\ptt sub}, theory, 5
  \item {\ptt SUB\_1\_LESS}, 20
  \item {\ptt SUB\_1\_LESS\_EQ}, 20
  \item {\ptt SUB\_ADD\_SELF}, 5, 20
  \item {\ptt SUB\_BOTH\_SIDES}, 5, 21
  \item {\ptt SUB\_EQ\_SUB\_ADD\_SUB}, 21
  \item {\ptt SUB\_GREATER\_0}, 21
  \item {\ptt SUB\_GREATER\_EQ\_ADD}, 21
  \item {\ptt SUB\_LE\_ADD}, 5, 21
  \item {\ptt SUB\_LESS\_BOTH\_SIDES}, 21
  \item {\ptt SUB\_LESS\_EQ\_SUB1}, 21
  \item {\ptt SUB\_LESS\_EQ\_SUB\_SUC}, 21
  \item {\ptt SUB\_LESS\_TO\_LESS\_ADDL}, 21
  \item {\ptt SUB\_LESS\_TO\_LESS\_ADDR}, 21
  \item {\ptt SUB\_PRE\_SUB\_1}, 21
  \item {\ptt SUB\_SUB\_ID}, 21
  \item {\ptt SUB\_SUC}, 21
  \item {\ptt SUB\_SUC\_PRE\_SUB}, 21
  \item {\ptt suc}, theory, 4
  \item {\ptt SUC\_0}, 16
  \item {\ptt SUC\_DIV\_CASES}, 23
  \item {\ptt SUC\_DIV\_SELF}, 6, 23
  \item {\ptt SUC\_GREATER\_EQ\_SUC}, 4, 16
  \item {\ptt SUC\_LESS\_EQ}, 16
  \item {\ptt SUC\_LESS\_EQ\_PRE}, 17
  \item {\ptt SUC\_LESS\_N\_LESS}, 19
  \item {\ptt SUC\_LESS\_PRE}, 17
  \item {\ptt SUC\_MAX}, 24
  \item {\ptt SUC\_MIN}, 24
  \item {\ptt SUC\_MOD}, 23
  \item {\ptt SUC\_MOD\_SELF}, 6, 23
  \item {\ptt SUC\_NOT\_0}, 4, 16
  \item {\ptt SUC\_PRE}, 5, 17
  \item {\ptt SUC\_SUB}, 21
  \item {\ptt SUM\_LESS}, 19

  \indexspace

  \item {\ptt zero\_ineq}, theory, 4
  \item {\ptt ZERO\_LESS\_TWO\_EXP}, 22

\end{theindex}
