\begin{theindex}

  \item {\ptt B\_AND\_ASSOC}, 23
  \item {\ptt B\_AND\_DEF}, 23
  \item {\ptt B\_AND\_SYM}, 24
  \item {\ptt B\_NOT}, 24
  \item {\ptt B\_NOT\_DEF}, 24
  \item {\ptt B\_OR\_ASSOC}, 24
  \item {\ptt B\_OR\_DEF}, 24
  \item {\ptt B\_OR\_SYM}, 24
  \item {\ptt B\_XOR\_ASSOC}, 24
  \item {\ptt B\_XOR\_DEF}, 24
  \item {\ptt B\_XOR\_SYM}, 24
  \item {\ptt BV}, 24

  \indexspace

  \item {\ptt define\_word\_partition}, 6
  \item {\ptt define\_word\_val}, 4
  \item {\ptt define\_wordn\_bit\_ops}, 3
  \item {\ptt define\_wordn\_type}, 4

  \indexspace

  \item {\ptt EXISTS\_wordn\_REP}, 23

  \indexspace

  \item {\ptt new\_wordn\_definition}, 6

  \indexspace

  \item {\ptt prove\_bit\_op\_thms}, 9
  \item {\ptt prove\_BITS\_one\_one}, 7
  \item {\ptt prove\_BITS\_onto}, 8
  \item {\ptt prove\_BITS\_WORD}, 8
  \item {\ptt prove\_function\_defn\_thm}, 10
  \item {\ptt prove\_LENGTH\_BITS\_thm}, 10
  \item {\ptt prove\_NWORD\_MOD}, 11
  \item {\ptt prove\_WORD\_one\_one}, 13
  \item {\ptt prove\_WORD\_onto}, 14
  \item {\ptt prove\_word\_val}, 14
  \item {\ptt prove\_wordn\_cases\_thm}, 12
  \item {\ptt prove\_wordn\_const\_cases}, 12
  \item {\ptt prove\_wordn\_induction\_thm}, 13

  \indexspace

  \item {\ptt use\_wordn}, 15

  \indexspace

  \item {\ptt VAL}, 24
  \item {\ptt VAL\_LESS}, 25
  \item {\ptt VAL\_LESS\_EQ}, 25
  \item {\ptt VAL\_ONE\_ONE}, 25
  \item {\ptt VAL\_ONTO}, 25
  \item {\ptt VAL\_ONTO\_LEMMA}, 25

  \indexspace

  \item {\ptt WORDN}, 25
  \item {\ptt WORDN\_0}, 25
  \item {\ptt wordn\_ABS\_REP}, 23
  \item {\ptt wordn\_bit\_ops}, 16
  \item {\ptt wordn\_CASES\_TAC}, 17
  \item {\ptt wordn\_CONV}, 18
  \item {\ptt wordn\_EQ\_CONV}, 19
  \item {\ptt wordn\_FN\_DEF\_THM}, 23
  \item {\ptt WORDN\_MOD}, 25
  \item {\ptt wordn\_NVAL\_CONV}, 20
  \item {\ptt wordn\_NWORD\_CONV}, 20
  \item {\ptt WORDN\_VAL}, 25
  \item {\ptt wordn\_X\_CASES\_TAC}, 21

  \indexspace

  \item {\ptt XOR\_ASSOC}, 24

\end{theindex}
