\begin{theindex}

  \item {\ptt APPEND}, 8
  \item {\ptt append}, theory, 8
  \item {\ptt APPEND\_11}, 38
  \item {\ptt APPEND\_BUTLAST\_LAST}, 38
  \item {\ptt APPEND\_CLAUSES}, 8, 38
  \item {\ptt APPEND\_CONS}, 38
  \item {\ptt APPEND\_CONS\_EQ\_APPEND}, 38
  \item {\ptt APPEND\_CONS\_EQ\_APPEND\_SNOC},  38 
  \item {\ptt APPEND\_EL\_11}, 39
  \item {\ptt APPEND\_EL\_REVERSE\_CONS},  39 
  \item {\ptt APPEND\_FIRSTN\_LASTN}, 49
  \item {\ptt APPEND\_FIRSTN\_NTL}, 46
  \item {\ptt APPEND\_ID}, 39
  \item {\ptt APPEND\_ID\_NULL}, 39
  \item {\ptt APPEND\_IS\_NIL}, 39
  \item {\ptt APPEND\_IS\_NULL}, 8, 39
  \item {\ptt APPEND\_JOIN}, 39
  \item {\ptt APPEND\_LASTN\_LASTN}, 49
  \item {\ptt APPEND\_LENGTH\_EQ}, 39
  \item {\ptt APPEND\_NBUTLAST\_LASTN}, 14, 49
  \item {\ptt APPEND\_NBUTLAST\_NTL}, 49
  \item {\ptt APPEND\_NIL}, 39
  \item {\ptt APPEND\_SUBSEQ}, 46
  \item {\ptt APPEND\_SUBSEQ2}, 46
  \item {\ptt APPEND\_UNAPPEND\_LEFT\_ID},  12, 57 
  \item {\ptt APPEND\_UNAPPEND\_RIGHT\_ID},  57 

  \indexspace

  \item {\ptt BUTLAST}, 5, 6, 34
  \item {\ptt BUTLAST1}, 39
  \item {\ptt BUTLAST\_APPEND}, 39
  \item {\ptt BUTLAST\_CONS}, 6, 34
  \item {\ptt BUTLAST\_CONS\_NOT\_NULL}, 35
  \item {\ptt BUTLAST\_CONV}, 21
  \item {\ptt BUTLAST\_DEF}, 6, 35
  \item {\ptt BUTLAST\_EL}, 35
  \item {\ptt BUTLAST\_NIL}, 35
  \item {\ptt BUTLAST\_NULL}, 35
  \item {\ptt BUTLAST\_REVERSE\_EQ\_-} \newline 
 {\ptt REVERSE\_TL},  35 
  \item {\ptt BUTLAST\_TL}, 35
  \item {\ptt BUTLAST\_TO\_NBUTLAST}, 49

  \indexspace

  \item {\ptt CON}, 7, 37
  \item {\ptt CONS}, 4, 5
  \item {\ptt CONS\_APPEND\_CONS}, 8, 39
  \item {\ptt CONS\_LLEQ\_LEFT\_TL}, 12, 53
  \item {\ptt CONS\_LLESS\_LEFT\_APPEND\_HD},  53 
  \item {\ptt CONS\_LLESS\_LEFT\_HD}, 53
  \item {\ptt CONS\_LLESS\_LEFT\_TL}, 12, 53
  \item {\ptt CONS\_MEMBER\_LIST}, 40
  \item {\ptt CONS\_MEMBER\_LIST\_NULL}, 40
  \item {\ptt CONS\_ONE\_ONE}, 4, 33

  \indexspace

  \item {\ptt EL}, 9
  \item {\ptt el}, theory, 9
  \item {\ptt EL1}, 9, 43
  \item {\ptt EL1\_HD}, 9, 43
  \item {\ptt EL1\_SUC\_CONS}, 9, 43
  \item {\ptt EL1\_TL}, 61
  \item {\ptt EL\_0\_REVERSE}, 43
  \item {\ptt EL\_APPEND\_1}, 9, 43
  \item {\ptt EL\_APPEND\_2}, 9, 43
  \item {\ptt EL\_APPEND\_EL}, 43
  \item {\ptt EL\_BUTLAST}, 43
  \item {\ptt EL\_CONS}, 43
  \item {\ptt EL\_CONS\_SUB1}, 44
  \item {\ptt EL\_CONV}, 22
  \item {\ptt EL\_ELL}, 10, 45
  \item {\ptt EL\_FROM0}, 61
  \item {\ptt EL\_HD}, 9, 44
  \item {\ptt EL\_HD\_NTAIL}, 13, 46
  \item {\ptt EL\_LENGTH\_APPEND}, 44
  \item {\ptt EL\_MAP}, 44
  \item {\ptt EL\_MAP2}, 44
  \item {\ptt EL\_MAP\_FROM0}, 61
  \item {\ptt EL\_NBUTLAST}, 50
  \item {\ptt EL\_NTAIL\_1}, 46
  \item {\ptt EL\_REPLICATE}, 44
  \item {\ptt EL\_REVERSE}, 44
  \item {\ptt EL\_SNOC}, 44
  \item {\ptt ELL}, 9, 10, 45
  \item {\ptt ell}, theory, 9
  \item {\ptt ELL\_APPEND\_1}, 10, 45
  \item {\ptt ELL\_APPEND\_2}, 45
  \item {\ptt ELL\_CONS}, 10, 45
  \item {\ptt ELL\_CONV}, 21
  \item {\ptt ELL\_EL}, 45
  \item {\ptt ELL\_LAST}, 10, 45
  \item {\ptt ELL\_LASTN}, 49
  \item {\ptt ELL\_LENGTH\_APPEND}, 45
  \item {\ptt ELL\_MAP}, 45
  \item {\ptt ELL\_MAP2}, 45
  \item {\ptt ELL\_NBUTLAST}, 50
  \item {\ptt ELL\_SNOC}, 45
  \item {\ptt ELL\_SNOC0}, 45
  \item {\ptt ELL\_SUC\_SNOC}, 45
  \item {\ptt EQ\_LENGTH\_INDUCT\_TAC}, 23
  \item {\ptt EQ\_LENGTH\_SNOC\_INDUCT\_TAC},  24 
  \item {\ptt EVERY}, 10
  \item {\ptt EVERY\_APPEND}, 42
  \item {\ptt EVERY\_FROM0}, 61
  \item {\ptt EVERY\_LASTN}, 50
  \item {\ptt EVERY\_MAP}, 10, 42
  \item {\ptt EVERY\_SNOC}, 42
  \item {\ptt EVERY\_UPTO}, 61
  \item {\ptt EXISTS\_EL}, 44
  \item {\ptt EXISTS\_UNAPPEND\_LEFT}, 57
  \item {\ptt EXISTS\_UNAPPEND\_RIGHT}, 57

  \indexspace

  \item {\ptt FIRSTN}, 13, 46
  \item {\ptt FIRSTN\_APPEND1}, 47
  \item {\ptt FIRSTN\_FIRSTN}, 47
  \item {\ptt FIRSTN\_LENGTH\_ID}, 47
  \item {\ptt FIRSTN\_NIL}, 47
  \item {\ptt FIRSTN\_NULL}, 13, 47
  \item {\ptt FROM0}, 17, 62
  \item {\ptt FROM0\_APPEND}, 18, 62
  \item {\ptt FROM0\_PRE}, 62
  \item {\ptt FROM0\_SUB}, 62
  \item {\ptt FST\_SND\_UNZIP\_ZIP}, 17, 60

  \indexspace

  \item {\ptt general\_lists}, theory, 4

  \indexspace

  \item {\ptt HD}, 5
  \item {\ptt HD\_APPEND}, 40
  \item {\ptt HD\_APPEND\_NULL}, 8, 40
  \item {\ptt HD\_BUTLAST}, 35
  \item {\ptt HD\_ELL\_LENGTH\_CONS}, 46
  \item {\ptt HD\_ELL\_LENGTH\_SNOC}, 46
  \item {\ptt HD\_ELL\_PRE\_LENGTH}, 46
  \item {\ptt HD\_MAP}, 10, 42
  \item {\ptt HD\_SNOC}, 5, 35
  \item {\ptt HEAD\_APPEND}, 40
  \item {\ptt HEAD\_APPEND\_NULL}, 40

  \indexspace

  \item {\ptt IMP\_APPEND\_NOT\_NIL}, 40
  \item {\ptt IMP\_APPEND\_NOT\_NULL}, 40
  \item {\ptt INTERVAL}, 18, 62
  \item {\ptt ISO\_REVERSE}, 35
  \item {\ptt ITERATED}, 8, 40
  \item {\ptt ITERATED\_EMPTY}, 8, 40
  \item {\ptt ITLIST}, 10, 42
  \item {\ptt ITLIST\_MAP}, 10
  \item {\ptt ITLIST\_MAP\_EQ}, 42

  \indexspace

  \item {\ptt L\_EQ\_NIL}, 34
  \item {\ptt LAST}, 5, 6, 35
  \item {\ptt LAST1}, 40
  \item {\ptt LAST\_APPEND}, 40
  \item {\ptt LAST\_BUTLAST\_exist}, 35
  \item {\ptt LAST\_CONS}, 6, 35
  \item {\ptt LAST\_CONS\_NOT\_NULL}, 35
  \item {\ptt LAST\_CONV}, 25
  \item {\ptt LAST\_DEF}, 6, 35
  \item {\ptt LAST\_EL}, 6, 35
  \item {\ptt LAST\_EL\_LENGTH}, 44
  \item {\ptt LAST\_LASTN}, 51
  \item {\ptt LAST\_NBUTLAST\_EL}, 51
  \item {\ptt LAST\_NBUTLAST\_ELL}, 51
  \item {\ptt LAST\_REVERSE\_EQ\_HD}, 36
  \item {\ptt last\_subseq}, theory, 14
  \item {\ptt LAST\_TL}, 36
  \item {\ptt LAST\_TO\_LASTN}, 51
  \item {\ptt LASTN}, 14, 50
  \item {\ptt LASTN\_APPEND}, 50
  \item {\ptt LASTN\_APPEND2}, 50
  \item {\ptt LASTN\_CONS}, 50
  \item {\ptt LASTN\_CONV}, 24
  \item {\ptt LASTN\_LASTN}, 50
  \item {\ptt LASTN\_LENGTH\_APPEND}, 50
  \item {\ptt LASTN\_LENGTH\_ID}, 14, 50
  \item {\ptt LASTN\_MAP}, 50
  \item {\ptt LASTN\_MAP2}, 50
  \item {\ptt LASTN\_NBUTLAST}, 51
  \item {\ptt LASTN\_NBUTLAST\_APPEND}, 51
  \item {\ptt LASTN\_NBUTLAST\_TL\_SPLIT},  51 
  \item {\ptt LASTN\_NIL}, 51
  \item {\ptt LASTN\_NULL}, 51
  \item {\ptt LASTN\_NULLN}, 14
  \item {\ptt LASTN\_SUC\_SNOC}, 51
  \item {\ptt LENGTH}, 4
  \item {\ptt LENGTH1\_CONS\_HD}, 33
  \item {\ptt LENGTH\_APPEND\_EL}, 40
  \item {\ptt LENGTH\_BUTLAST}, 36
  \item {\ptt LENGTH\_CLAUSES}, 41
  \item {\ptt LENGTH\_EQ}, 4, 33
  \item {\ptt LENGTH\_EQ\_SUC\_IMP\_NOT\_-} \newline 
 {\ptt NIL},  33 
  \item {\ptt LENGTH\_EQ\_SUC\_IMP\_NOT\_-} \newline 
 {\ptt NULL},  33 
  \item {\ptt LENGTH\_FIRSTN}, 47
  \item {\ptt LENGTH\_FROM0}, 62
  \item {\ptt LENGTH\_GR\_0\_NOT\_NIL}, 33
  \item {\ptt LENGTH\_LASTN}, 51
  \item {\ptt LENGTH\_LESS\_EQ}, 33
  \item {\ptt LENGTH\_LESS\_EQ\_EQ}, 34
  \item {\ptt LENGTH\_LESS\_IMP\_NOT\_-} \newline 
 {\ptt EQ},  34 
  \item {\ptt LENGTH\_LIST\_INDUCT\_TAC},  25 
  \item {\ptt LENGTH\_NOT\_NULL}, 34
  \item {\ptt LENGTH\_NTAIL}, 47
  \item {\ptt LENGTH\_NTAIL\_LESS}, 47
  \item {\ptt LENGTH\_NULL}, 4, 34
  \item {\ptt LENGTH\_PAD\_LEFT}, 16, 59
  \item {\ptt LENGTH\_PAD\_RIGHT}, 16, 59
  \item {\ptt LENGTH\_REPLICATE}, 8, 41
  \item {\ptt LENGTH\_REVERSE}, 7
  \item {\ptt LENGTH\_ROTATE1\_LEFT}, 59
  \item {\ptt LENGTH\_ROTATE1\_RIGHT}, 59
  \item {\ptt LENGTH\_SNOC}, 36
  \item {\ptt LENGTH\_TAIL}, 7, 38
  \item {\ptt LENGTH\_TL}, 36
  \item {\ptt LENGTH\_TL\_SUB}, 34
  \item {\ptt list\_APPEND\_Axiom}, 41
  \item {\ptt list\_APPEND\_CASES}, 41
  \item {\ptt list\_APPEND\_INDUCT}, 41
  \item {\ptt LIST\_APPEND\_INDUCT\_TAC},  8, 26 
  \item {\ptt list\_APPEND\_NULL\_CASES},  41 
  \item {\ptt list\_CASES2}, 7, 38
  \item {\ptt LIST\_LENGTH\_INDUCT\_TAC},  4 
  \item {\ptt list\_NULL\_CASES}, 34
  \item {\ptt list\_NULL\_CASES2}, 7, 38
  \item {\ptt LLEQ\_LEFT}, 11, 53
  \item {\ptt LLEQ\_LEFT\_APPEND\_UNAPPEND\_LEFT},  57 
  \item {\ptt LLEQ\_LEFT\_UNAPPEND\_LEFT\_-} \newline 
 {\ptt CONS},  57 
  \item {\ptt LLEQ\_RIGHT}, 11, 53
  \item {\ptt LLEQ\_RIGHT\_APPEND\_UNAPPEND\_-} \newline 
 {\ptt RIGHT},  12, 57 
  \item {\ptt LLEQ\_RIGHT\_UNAPPEND\_RIGHT\_-} \newline 
 {\ptt SNOC},  57 
  \item {\ptt LLESS\_LEFT}, 11, 54
  \item {\ptt LLESS\_LEFT\_APPEND}, 54
  \item {\ptt LLESS\_LEFT\_APPEND\_LLEQ\_-} \newline 
 {\ptt LEFT},  54 
  \item {\ptt LLESS\_LEFT\_APPEND\_UNAPPEND\_-} \newline 
 {\ptt LEFT},  12, 57 
  \item {\ptt LLESS\_LEFT\_APPEND\_UNAPPEND\_-} \newline 
 {\ptt LEFT\_LLESS\_LEFT},  57 
  \item {\ptt LLESS\_LEFT\_CONS}, 54
  \item {\ptt LLESS\_LEFT\_CONS\_HD}, 54
  \item {\ptt LLESS\_LEFT\_CONS\_TL\_LLESS\_-} \newline 
 {\ptt LEFT},  54 
  \item {\ptt LLESS\_LEFT\_EXISTS\_APPEND},  54 
  \item {\ptt LLESS\_LEFT\_LENGTH1\_NULL},  54 
  \item {\ptt LLESS\_LEFT\_NULL}, 54
  \item {\ptt LLESS\_LEFT\_SINGLE\_NULL},  54 
  \item {\ptt LLESS\_RIGHT}, 11, 54
  \item {\ptt LLESS\_RIGHT\_APPEND}, 54
  \item {\ptt LLESS\_RIGHT\_APPEND\_LLEQ\_-} \newline 
 {\ptt RIGHT},  55 
  \item {\ptt LLESS\_RIGHT\_APPEND\_UNAPPEND\_-} \newline 
 {\ptt RIGHT},  58 
  \item {\ptt LLESS\_RIGHT\_APPEND\_UNAPPEND\_-} \newline 
 {\ptt RIGHT\_LLESS\_RIGHT},  58 
  \item {\ptt LLESS\_RIGHT\_EXISTS\_APPEND},  55 
  \item {\ptt LLESS\_RIGHT\_LENGTH1\_NULL},  55 
  \item {\ptt LLESS\_RIGHT\_NULL}, 55
  \item {\ptt LLESS\_RIGHT\_SINGLE\_NULL},  55 
  \item {\ptt LLESS\_RIGHT\_SNOC}, 55
  \item {\ptt LLESS\_RIGHT\_SNOC\_BUTLAST\_-} \newline 
 {\ptt LLESS\_RIGHT},  55 
  \item {\ptt LLESS\_RIGHT\_SNOC\_LAST}, 55
  \item {\ptt load\_more\_lists}, 19--20

  \indexspace

  \item {\ptt MAP}, 10
  \item {\ptt map}, theory, 10
  \item {\ptt MAP2\_CONV}, 27
  \item {\ptt MAP2\_EL}, 44
  \item {\ptt MAP2\_ELL}, 46
  \item {\ptt MAP2\_SNOC}, 42
  \item {\ptt MAP\_EL}, 44
  \item {\ptt MAP\_EL1\_SUC\_CONS}, 44
  \item {\ptt MAP\_ELL}, 46
  \item {\ptt MAP\_MAP\_o}, 10, 43
  \item {\ptt MAP\_SNOC}, 43
  \item {\ptt MEMBER}, 11, 55
  \item {\ptt member}, theory, 11
  \item {\ptt MEMBER\_SNOC}, 12, 55
  \item {\ptt more\_lists}, theory, 4

  \indexspace

  \item {\ptt NBUTLAST}, 14, 52
  \item {\ptt NBUTLAST\_APPEND}, 52
  \item {\ptt NBUTLAST\_APPEND1}, 52
  \item {\ptt NBUTLAST\_BUTLAST\_SYM}, 14, 52
  \item {\ptt NBUTLAST\_CONS}, 52
  \item {\ptt NBUTLAST\_CONV}, 28
  \item {\ptt NBUTLAST\_LASTN}, 52
  \item {\ptt NBUTLAST\_LASTN\_NIL}, 52
  \item {\ptt NBUTLAST\_LENGTH}, 52
  \item {\ptt NBUTLAST\_LENGTH\_APPEND}, 52
  \item {\ptt NBUTLAST\_LENGTH\_CONS}, 52
  \item {\ptt NBUTLAST\_LENGTH\_NIL}, 52
  \item {\ptt NBUTLAST\_LENGTH\_NULL}, 14, 52
  \item {\ptt NBUTLAST\_MAP}, 52
  \item {\ptt NBUTLAST\_MAP2}, 53
  \item {\ptt NBUTLAST\_NBUTLAST}, 53
  \item {\ptt NBUTLAST\_SIMP\_REC}, 53
  \item {\ptt NBUTLAST\_SUC\_SNOC}, 53
  \item {\ptt NIL\_EQ\_L}, 34
  \item {\ptt NIL\_LLEQ\_LEFT}, 55
  \item {\ptt NIL\_LLEQ\_RIGHT}, 12, 55
  \item {\ptt NIL\_NOT\_APPEND\_CONS2}, 41
  \item {\ptt NOT\_LENGTH\_EQ}, 34
  \item {\ptt NOT\_LLESS\_LEFT\_CONS\_NOT\_-} \newline 
 {\ptt NULL},  55 
  \item {\ptt NOT\_LLESS\_LEFT\_CONS\_NOT\_-} \newline 
 {\ptt TL\_LLESS\_LEFT},  56 
  \item {\ptt NOT\_LLESS\_LEFT\_NIL}, 12, 56
  \item {\ptt NOT\_LLESS\_LEFT\_NOT\_NULL},  56 
  \item {\ptt NOT\_LLESS\_LEFT\_TL}, 56
  \item {\ptt NOT\_LLESS\_RIGHT\_BUTLAST},  56 
  \item {\ptt NOT\_LLESS\_RIGHT\_NIL}, 56
  \item {\ptt NOT\_LLESS\_RIGHT\_NOT\_NULL},  56 
  \item {\ptt NOT\_LLESS\_RIGHT\_SNOC\_NOT\_-} \newline 
 {\ptt BUTLAST\_LLESS\_RIGHT},  56 
  \item {\ptt NOT\_LLESS\_RIGHT\_SNOC\_NOT\_-} \newline 
 {\ptt NULL},  56 
  \item {\ptt NOT\_NIL\_APPEND\_EL}, 41
  \item {\ptt NOT\_NIL\_LLESS\_LEFT}, 56
  \item {\ptt NOT\_NIL\_LLESS\_RIGHT}, 56
  \item {\ptt NOT\_NIL\_SNOC}, 36
  \item {\ptt NOT\_NULL\_FROM0}, 62
  \item {\ptt NOT\_NULL\_NBUTLAST}, 53
  \item {\ptt NOT\_NULL\_NTAIL}, 47
  \item {\ptt NOT\_NULL\_NTAIL\_TL}, 47
  \item {\ptt NOT\_NULL\_TAIL}, 7, 38
  \item {\ptt NOT\_SNOC\_NIL}, 36
  \item {\ptt NTAIL}, 13, 47
  \item {\ptt NTAIL\_NIL}, 47
  \item {\ptt NTAIL\_NTAIL}, 47
  \item {\ptt NTAIL\_TAIL}, 47
  \item {\ptt NTL}, 13, 47
  \item {\ptt NTL\_APPEND}, 48
  \item {\ptt NTL\_LENGTH}, 48
  \item {\ptt NTL\_LENGTH\_APPEND}, 48
  \item {\ptt NTL\_LENGTH\_NIL}, 48
  \item {\ptt NTL\_LENGTH\_NULL}, 48
  \item {\ptt NTL\_NTL}, 48
  \item {\ptt NTL\_SIMP\_REC}, 48
  \item {\ptt NTL\_TL\_SYM}, 13, 48
  \item {\ptt NULL}, 4
  \item {\ptt NULL\_EQ\_EMPTY}, 4, 34
  \item {\ptt NULL\_ITERATED}, 41
  \item {\ptt NULL\_MAP}, 43
  \item {\ptt NULL\_NOT\_APPEND\_CONS}, 41
  \item {\ptt NULL\_NTAIL}, 48
  \item {\ptt NULL\_SUBSEQ}, 48
  \item {\ptt NULL\_UNAPPEND\_LEFT}, 12, 58
  \item {\ptt NULL\_UNAPPEND\_RIGHT}, 58
  \item {\ptt num\_lists}, theory, 17

  \indexspace

  \item {\ptt ONE\_MEMBER\_LIST}, 41
  \item {\ptt ONE\_MEMBER\_LIST\_NULL}, 41

  \indexspace

  \item {\ptt PAD\_LEFT}, 15, 59
  \item {\ptt PAD\_RIGHT}, 14, 15, 59

  \indexspace

  \item {\ptt RANGE}, 17, 62
  \item {\ptt RANGE\_SHIFT}, 18, 62
  \item {\ptt RANGE\_TOP}, 18, 62
  \item {\ptt REPLICATE}, 8, 41
  \item {\ptt REVERSE}, 5, 8, 41
  \item {\ptt REVERSE\_APPEND}, 42
  \item {\ptt REVERSE\_APPEND\_EL\_CONS},  42 
  \item {\ptt REVERSE\_CLAUSES}, 7, 36
  \item {\ptt REVERSE\_DEF}, 6, 36
  \item {\ptt REVERSE\_EQ\_NIL}, 36
  \item {\ptt REVERSE\_EXISTS}, 36
  \item {\ptt REVERSE\_NULL}, 7, 36
  \item {\ptt REVERSE\_REVERSE}, 36
  \item {\ptt REVERSE\_SINGLE}, 7, 36
  \item {\ptt ROTATE1\_LEFT}, 15, 59
  \item {\ptt ROTATE1\_LEFT\_CONS}, 16, 59
  \item {\ptt ROTATE1\_LEFT\_NIL}, 59
  \item {\ptt ROTATE1\_LEFT\_ROTATE1\_RIGHT},  59 
  \item {\ptt ROTATE1\_RIGHT}, 15, 59
  \item {\ptt ROTATE1\_RIGHT\_NIL}, 16, 59
  \item {\ptt ROTATE1\_RIGHT\_ROTATE1\_LEFT},  59 
  \item {\ptt ROTATE1\_RIGHT\_SNOC}, 59
  \item {\ptt ROTATE\_LEFT}, 15, 60
  \item {\ptt ROTATE\_LEFT\_EL}, 16, 60
  \item {\ptt ROTATE\_LEFT\_ROTATE1\_LEFT},  60 
  \item {\ptt ROTATE\_LEFT\_ROTATE\_RIGHT},  60 
  \item {\ptt ROTATE\_LEFT\_SUC\_CONS}, 60
  \item {\ptt ROTATE\_RIGHT}, 15, 60
  \item {\ptt ROTATE\_RIGHT\_EL}, 60
  \item {\ptt ROTATE\_RIGHT\_ROTATE1\_RIGHT},  60 
  \item {\ptt ROTATE\_RIGHT\_ROTATE\_LEFT},  16, 60 
  \item {\ptt ROTATE\_RIGHT\_SUC\_SNOC}, 60

  \indexspace

  \item {\ptt SAME\_LENGTH\_SNOC}, 37
  \item {\ptt shift}, theory, 14
  \item {\ptt SNOC}, 5, 37
  \item {\ptt snoc}, theory, 5
  \item {\ptt SNOC\_11}, 37
  \item {\ptt SNOC\_APPEND\_CONS}, 8, 42
  \item {\ptt SNOC\_Axiom}, 5, 37
  \item {\ptt SNOC\_CASES}, 37
  \item {\ptt SNOC\_CONV}, 29
  \item {\ptt SNOC\_DEF}, 5, 37
  \item {\ptt SNOC\_EQ\_LENGTH\_EQ}, 37
  \item {\ptt SNOC\_INDUCT}, 5, 37
  \item {\ptt SNOC\_INDUCT\_TAC}, 29
  \item {\ptt SNOC\_INDUCT\_TAC}, 8
  \item {\ptt SNOC\_LLEQ\_RIGHT\_BUTLAST},  56 
  \item {\ptt SNOC\_LLESS\_RIGHT\_APPEND\_LAST},  56 
  \item {\ptt SNOC\_LLESS\_RIGHT\_BUTLAST},  12, 57 
  \item {\ptt SNOC\_LLESS\_RIGHT\_LAST}, 57
  \item {\ptt SNOC\_NOT\_NULL}, 5, 37
  \item {\ptt SNOC\_NULL\_CASES}, 37
  \item {\ptt SNOC\_ONE\_ONE}, 37
  \item {\ptt SNOC\_REVERSE\_CONS}, 37
  \item {\ptt SNOC\_INDUCT\_TAC}, 5
  \item {\ptt SPLIT\_CONV}, 30
  \item {\ptt SUBSEQ}, 13, 48
  \item {\ptt subseq}, theory, 13
  \item {\ptt SUBSEQ2}, 48
  \item {\ptt SUBSEQ\_APPEND}, 48
  \item {\ptt SUBSEQ\_APPEND2}, 49
  \item {\ptt SUBSEQ\_EMPTY\_LIST}, 49
  \item {\ptt SUBSEQ\_EQ}, 49
  \item {\ptt SUBSEQ\_EXISTS}, 49
  \item {\ptt SUBSEQ\_MAP}, 49
  \item {\ptt SUBSEQ\_SUBSEQ}, 13, 49
  \item {\ptt SUBSEQUENCE\_EXISTS}, 42
  \item {\ptt SUBSEQUENCES}, 48
  \item {\ptt SUBST\_REVERSE\_CONV}, 7, 30
  \item {\ptt SUC\_UPTO\_SUC}, 62

  \indexspace

  \item {\ptt TAIL}, 7, 38
  \item {\ptt tail}, theory, 7
  \item {\ptt TAIL\_APPEND}, 7, 38
  \item {\ptt TAIL\_MAP}, 43
  \item {\ptt TAIL\_NTAIL}, 49
  \item {\ptt TL}, 4, 5, 7
  \item {\ptt TL\_APPEND}, 42
  \item {\ptt TL\_APPEND\_NULL}, 42
  \item {\ptt TL\_MAP}, 10, 43
  \item {\ptt TL\_NIL}, 34
  \item {\ptt TL\_NULL}, 4, 34
  \item {\ptt TL\_SNOC}, 5, 37
  \item {\ptt TL\_TAIL}, 7, 38

  \indexspace

  \item {\ptt unappend}, theory, 12
  \item {\ptt UNAPPEND\_LEFT}, 12, 58
  \item {\ptt UNAPPEND\_LEFT\_CONS}, 58
  \item {\ptt UNAPPEND\_LEFT\_EQ\_NIL}, 58
  \item {\ptt UNAPPEND\_LEFT\_NIL}, 58
  \item {\ptt UNAPPEND\_LEFT\_UNAPPEND\_RIGHT},  58 
  \item {\ptt UNAPPEND\_RIGHT}, 12, 58
  \item {\ptt UNAPPEND\_RIGHT\_EQ\_NIL}, 58
  \item {\ptt UNAPPEND\_RIGHT\_NIL}, 12, 58
  \item {\ptt UNAPPEND\_RIGHT\_SNOC}, 58
  \item {\ptt UNAPPEND\_RIGHT\_UNAPPEND\_-} \newline 
 {\ptt LEFT},  58 
  \item {\ptt UNZIP\_FST}, 16, 60
  \item {\ptt UNZIP\_FST\_ZIP}, 17, 61
  \item {\ptt UNZIP\_SND}, 16, 61
  \item {\ptt UNZIP\_SND\_ZIP}, 17, 61
  \item {\ptt UPTO}, 17, 62
  \item {\ptt UPTO\_EQ\_CONS\_SUC\_UPTO},  18, 62 
  \item {\ptt UPTO\_SUC\_EQ\_APPEND\_UPTO},  62 

  \indexspace

  \item {\ptt ZIP}, 16, 17, 61
  \item {\ptt zip}, theory, 16
  \item {\ptt ZIP\_CLAUSES}, 17, 61
  \item {\ptt ZIP\_DEF}, 16, 61
  \item {\ptt ZIP\_UNZIP\_FST\_SND}, 17, 61

\end{theindex}
