\begin{theindex}

  \item \back $[ {\makebox [0mm][l]{$\bot $}\,{\bot }}]$ absurdity, 
		\hyperpage{80}
  \item \back $[ \forall \mathsf{x} \colon \mathsf{y}]$ all x indeed y, 
		\hyperpage{80}
  \item \back $[ \relax [ \mathsf{x} \relax ]^{-} ]$ false test t end test, 
		\hyperpage{75}
  \item \back $[\underline{ \mathsf{x}}]$ metavar x end metavar, 
		\hyperpage{81}
  \item \back $[ \relax [ \mathsf {t} \relax ]^{\circ} ]$ raw test t end test, 
		\hyperpage{75}
  \item \back $[ \langle ^ { \ast } \mathsf{x} \,{\protect\vert} \mathsf{y} {:=}\, \mathsf{z} \rangle ]$ sub star x set y to z end sub , 
		\hyperpage{82}
  \item \back $[ \langle \mathsf{x} \,{\protect\vert} \mathsf{y} {:=}\, \mathsf{z} \rangle ]$ sub x set y to z end sub , 
		\hyperpage{82}
  \item \back $[ \relax [ \mathsf {t} \relax ]^{\cdot} ]$ test t end test, 
		\hyperpage{74}
  \item \back $[ \emptyset ]$ the empty set, \hyperpage{83}
  \item \back $[ \mathsf{x} \mathrel { : \, : } \mathsf {T}]$ tuple x end tuple, 
		\hyperpage{66}
  \item \back $[ \mathsf{x} \mathop {\char64} \mathsf{y}]$ x at y, 
		\hyperpage{86}
  \item \back $[ \mathsf{x} \wedge_c \mathsf{y}]$ x claim and y, 
		\hyperpage{73}
  \item \back $[ \mathsf{x} \in_c \mathsf{y}]$ x claim in y, 
		\hyperpage{94}
  \item \back $[ \mathsf{x} ,\linebreak [0] \mathsf{y}]$ x comma y, 
		\hyperpage{66}
  \item \back $[ \mathsf{x} \gg \mathsf{y}]$ x conclude y, 
		\hyperpage{107}
  \item \back $[ \mathsf{x} {} ^ { - } ]$ x curry minus, \hyperpage{87}
  \item \back $[ \mathsf{x} {} ^ { + } ]$ x curry plus, \hyperpage{87}
  \item \back $[ \mathsf{x} ; \mathsf{y}]$ x cut y, \hyperpage{87}
  \item \back $[ \mathsf{x} {} ^ { \ast } ]$ x dereference, 
		\hyperpage{87}
  \item \back $[ \mathsf{x} \mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \mathsf{y}]$ x endorse y, 
		\hyperpage{80}
  \item \back $[ \mathsf{x} {}^{1}]$ x first, \hyperpage{32}
  \item \back $[ \mathsf{x} \vdash \mathsf{y}]$ x infer y, 
		\hyperpage{80}
  \item \back $[ \mathsf{x} \le' \mathsf{y}]$ x less one y, 
		\hyperpage{40}
  \item \back $[ \mathsf{x} < \mathsf{y}]$ x less y, \hyperpage{39}
  \item \back $[ \mathsf{x} <' \mathsf{y}]$ x less zero y, 
		\hyperpage{40}
  \item \back $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf{y} ,\linebreak [0] \mathsf {F} )]$ x macro and y, 
		\hyperpage{69}
  \item \back $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf{y} ,\linebreak [0] \mathsf {T} )]$ x macro imply y, 
		\hyperpage{69}
  \item \back $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf {T} ,\linebreak [0] \mathsf{y} )]$ x macro or y, 
		\hyperpage{69}
  \item \back $[ \mathsf{x} \mathop{-_1} \mathsf{y}]$ x minus one y, 
		\hyperpage{40}
  \item \back $[ \mathsf{x} - \mathsf{y}]$ x minus y, \hyperpage{40}
  \item \back $[ \mathsf{x} \mathop{-_0} \mathsf{y}]$ x minus zero y, 
		\hyperpage{40}
  \item \back $[ \mathsf{x} {} ^ { \rhd }]$ x modus, \hyperpage{86}
  \item \back $[ \mathsf{x} \rhd \mathsf{y}]$ x modus ponens y, 
		\hyperpage{107}
  \item \back $[ \mathsf{x} \mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} \mathsf{y}]$ x modus probans y, 
		\hyperpage{107}
  \item \back $[ \mathsf{x} \mathop{+_1} \mathsf{y}]$ x plus one y, 
		\hyperpage{39}
  \item \back $[ \mathsf{x} + \mathsf{y}]$ x plus y, \hyperpage{39}
  \item \back $[ \mathsf{x} \mathop{+_0} \mathsf{y}]$ x plus zero y, 
		\hyperpage{39}
  \item \back $[ \mathsf{x}']$ x prime, \hyperpage{49}
  \item \back $[ \mathsf{x} \mathrel {\oplus} \mathsf{y}]$ x rule plus y, 
		\hyperpage{80}
  \item \back $[ \mathsf{x} \stackrel{s}{=} \mathsf{y}]$ x sequent equal y, 
		\hyperpage{84}
  \item \back $[ \mathsf{x} [ \mathsf{y} {\Rightarrow} \mathsf{z} ]]$ x set multi y to z end set, 
		\hyperpage{48}
  \item \back $[ \mathsf{x} [ \mathsf{y} {\rightarrow} \mathsf{z} ]]$ x set y to z end set, 
		\hyperpage{47}
  \item \back $[ \mathsf{x} \mathrel{\tilde{\wedge}} \mathsf{y}]$ x simple and y, 
		\hyperpage{73}
  \item \back $[ \mathsf{x} \in_t \mathsf{y}]$ x term in y, 
		\hyperpage{83}
  \item \back $[ \mathsf{x} \backslash \{ \mathsf{y} \}]$ x term minus y end minus, 
		\hyperpage{83}
  \item \back $[ \mathsf{x} \cup \{ \mathsf{y} \}]$ x term plus y end plus, 
		\hyperpage{83}
  \item \back $[ \mathsf{x} \stackrel{r}{=} \mathsf{y}]$ x term root equal y, 
		\hyperpage{41}
  \item \back $[ \mathsf{x} \stackrel{T}{=} \mathsf{y}]$ x term set equal y, 
		\hyperpage{83}
  \item \back $[ \mathsf{x} \subseteq_T \mathsf{y}]$ x term subset y, 
		\hyperpage{83}
  \item \back $[ \mathsf{x} \cup \mathsf{y}]$ x term union y, 
		\hyperpage{83}
  \item \back $[ \mathsf{x} \cdot \mathsf{y}]$ x times y, 
		\hyperpage{40}
  \item \back $[ \mathsf{x} \cdot_0 \mathsf{y}]$ x times zero y, 
		\hyperpage{40}

  \indexspace

  \item absurdity, \hyperpage{80}
  \item absurdity $[ {\makebox [0mm][l]{$\bot $}\,{\bot }}]$, 
		\hyperpage{80}
  \item algorithm, unification, \hyperpage{103}
  \item all x indeed y $[ \forall \mathsf{x} \colon \mathsf{y}]$, 
		\hyperpage{80}
  \item antilemma, \hyperpage{79}
  \item antilemma: $ [ \mathsf{x} \mathbf{\ antilemma\ } \mathsf{y} \colon \mathsf{z} ]$ in theory x antilemma y says z end antilemma, 
		\hyperpage{95}
  \item antirule: $ [ \mathsf{x} \mathbf{\ antirule\ } \mathsf{y} \colon \mathsf{z} ]$ in theory x antirule y says z end antirule, 
		\hyperpage{100}
  \item apply identifier $[ \mbox {\tt \char34}\mathrm {apply}\mbox {\tt \char34}]$, 
		\hyperpage{55}
  \item \back $[ \forall \mathsf{y} \colon \mathsf{z}]$ arbitrary x end line y, 
		\hyperpage{108}
  \item arbitrary x end line y $[ \forall \mathsf{x} \colon \mathsf{y}]$, 
		\hyperpage{108}
  \item array, \hyperpage{46}
  \item \back $[ array\mbox{-}\linebreak[0]add( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {a} , \mathsf {b} )]$ array add x value y index z value a level b end add, 
		\hyperpage{48}
  \item array index, \hyperpage{47}
  \item \back $[ array\mbox{-}\linebreak[0]plus( \mathsf{x} , \mathsf{y} )]$ array plus x and y end plus, 
		\hyperpage{47}
  \item \back $[ array\mbox{-}\linebreak[0]put( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {a} )]$ array put x value y array z level a end put, 
		\hyperpage{48}
  \item \back $[ array\mbox{-}\linebreak[0]remove( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ array remove x array y level z end remove, 
		\hyperpage{48}
  \item aspect, \hyperpage{12}
  \item \back $[ \mathbf{aspect}( \mathsf {a} , \mathsf {t} , \mathsf {c} )]$, 
		\hyperpage{55}
  \item \back $[ \mathbf{aspect}( \mathsf{x} , \mathsf{y} )]$ aspect x subcodex y end aspect, 
		\hyperpage{55}
  \item aspect, potentially inherited page, \hyperpage{61}
  \item aspect, pyk, \hyperpage{12}
  \item aspect, statement, \hyperpage{77}
  \item aspect, tex, \hyperpage{12}
  \item association, \hyperpage{45}
  \item association tree, \hyperpage{45}
  \item atomic, \hyperpage{46}
  \item axiom, \hyperpage{77}
  \item axiom scheme, \hyperpage{78}

  \indexspace

  \item base page, \hyperpage{7, 8}
  \item basic tagged tree operations, \hyperpage{36}
  \item because x indeed y qed $[ \mathsf{x} \gg \mathsf{y}]$, 
		\hyperpage{108}
  \item bed, page, \hyperpage{61}
  \item bibliography, \hyperpage{8}, \hyperpage{49}
  \item bibliography hook $[ \mbox {\tt \char34}\mathrm {bibliography}\mbox {\tt \char34}]$, 
		\hyperpage{52}
  \item big bracket * end bracket, \hyperpage{112}
  \item \back $[ bit( \mathsf{x} , \mathsf{y} )]$ bit x of y end bit, 
		\hyperpage{40}
  \item \back $[ bit_1( \mathsf{x} , \mathsf{y} )]$ bit one x of y end bit, 
		\hyperpage{41}
  \item body, \hyperpage{8}, \hyperpage{49}
  \item body hook $[ \mbox {\tt \char34}\mathrm {body}\mbox {\tt \char34}]$, 
		\hyperpage{52}
  \item bottom, \hyperpage{26}
  \item bracket * end bracket, \hyperpage{112}

  \indexspace

  \item C*: $[ \mathsf{x} {} ^ {{\cal C} ^ { \ast }}]$ x is metaclosed star, 
		\hyperpage{81}
  \item C: $[ \mathsf{x} {} ^ {\cal C}]$ x is metaclosed, 
		\hyperpage{81}
  \item c: \back $[ \mathsf{x} \in_c \mathsf{y}]$ x claim in y, 
		\hyperpage{94}
  \item c: \back $[ \mathsf{x} \wedge_c \mathsf{y}]$ x claim and y, 
		\hyperpage{73}
  \item cache, \hyperpage{8}, \hyperpage{50}
  \item cache hook $[ \mbox {\tt \char34}\mathrm {cache}\mbox {\tt \char34}]$, 
		\hyperpage{52}
  \item calculus, sequent, \hyperpage{75}
  \item canonical, \hyperpage{27}
  \item cardinal, \hyperpage{7}
  \item cardinal number, \hyperpage{29}
  \item cardinal tree, \hyperpage{31}
  \item \back $[ \mathbf{check}( \mathsf {t} , \mathsf {c} )]$, 
		\hyperpage{73}
  \item \back $[ \mathbf{check}_2( \mathsf {t} , \mathsf {c} , \mathsf {d} )]$, 
		\hyperpage{73}
  \item \back $[ \mathbf{check}_3( \mathsf {t} , \mathsf {c} , \mathsf {d} )]$, 
		\hyperpage{73}
  \item \back $[ \mathbf{check}^*( \mathsf {t} , \mathsf {c} )]$, 
		\hyperpage{74}
  \item \back $[ \mathbf{check}^*_2( \mathsf {t} , \mathsf {c} , \mathsf {v} )]$, 
		\hyperpage{74}
  \item checker, \hyperpage{73}
  \item \back$[ \mbox{checker}]$ checker, \hyperpage{73}
  \item circular, \hyperpage{103}
  \item claim, \hyperpage{9}, \hyperpage{72}
  \item \back $[ \mbox {\tt \char34}\mathrm {claim}\mbox {\tt \char34}]$ claim aspect, 
		\hyperpage{54}
  \item claim define x as y end define $[ [ \mathsf{x} \stackrel {claim}{=} \mathsf{y} ]]$, 
		\hyperpage{72}
  \item claim: $[ [ \mathsf{x} \stackrel {claim}{=} \mathsf{y} ]]$ claim define x as y end define, 
		\hyperpage{72}
  \item \back $[ claims( \mathsf {t} , \mathsf {c} , \mathsf {r} )]$ claims t cache c ref r end claims, 
		\hyperpage{95}
  \item \back $[ claims_2( \mathsf {t} , \mathsf {c} , \mathsf {r} )]$ claims two t cache c ref r end claims, 
		\hyperpage{95}
  \item code hook $[ \mbox {\tt \char34}\mathrm {code}\mbox {\tt \char34}]$, 
		\hyperpage{52}
  \item codex, \hyperpage{8, 9}
  \item codex hook $[ \mbox {\tt \char34}\mathrm {codex}\mbox {\tt \char34}]$, 
		\hyperpage{52}
  \item codify, \hyperpage{9}, \hyperpage{56}
  \item color*: $[ \mathsf{x} \mbox {-color}^{\ast}( \mathsf{y} )]$ x color star y end color, 
		\hyperpage{92}
  \item color: $[ \mathsf{x} \mbox {-color}( \mathsf{y} )]$ x color y end color, 
		\hyperpage{91}
  \item colored, \hyperpage{91}
  \item coloring, \hyperpage{91}
  \item \back $[ Commutativity]$ sequent commutativity, \hyperpage{102}
  \item \back $[ Commutativity_1]$ tactic commutativity, 
		\hyperpage{105}
  \item compatible, \hyperpage{28}, \hyperpage{103}
  \item computably true x end true $[ \lambda \mathsf {c} . {\cal U}^M( {\cal E}( \lceil \mathsf{x} \rceil , \mathsf {T} , \mathsf {c} ) )]$, 
		\hyperpage{87}
  \item \back $[ conclude_1 ( \mathsf{x} , \mathsf{y} )]$ conclude one x cache y end conclude, 
		\hyperpage{107}
  \item \back $[ conclude_2 ( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ conclude two x proves y cache z end conclude, 
		\hyperpage{107}
  \item \back $[ conclude_3 ( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {a} )]$ conclude three x proves y lemma z substitution a end conclude, 
		\hyperpage{107}
  \item \back $[ conclude_4 ( \mathsf{x} , \mathsf{y} )]$ conclude four x lemma y end conclude, 
		\hyperpage{108}
  \item conclusion, \hyperpage{78}, \hyperpage{83}
  \item conclusion tactic, \hyperpage{107}
  \item conjecture, \hyperpage{79}
  \item construct, page, \hyperpage{51}
  \item \back $[ Contra]$ contraexample lemma, \hyperpage{101}
  \item \back $[ \mathsf {T} \mathrel { : \, : } \mathsf {T} = \mathsf {T} \vdash {\makebox [0mm][l]{$\bot $}\,{\bot }}]$ contraexample, 
		\hyperpage{78}
  \item \back $[ Contra'']$ contraexample lemma primed, \hyperpage{96}
  \item contradiction, \hyperpage{78}
  \item correctness, \hyperpage{72}
  \item currying, \hyperpage{87}
  \item cut, \hyperpage{87}
  \item \back $[ Cut( \mathsf{x} , \mathsf{y} )]$ cut x and y end cut, 
		\hyperpage{100}

  \indexspace

  \item d: $[ \mathsf{x} {}^{d}]$ x debug, \hyperpage{41}
  \item dead character code, \hyperpage{44}
  \item decurrying, \hyperpage{87}
  \item define identifier $[ \mbox {\tt \char34}\mathrm {define}\mbox {\tt \char34}]$, 
		\hyperpage{57}
  \item definition aspect $[ \mbox {\tt \char34}\mathrm {definition}\mbox {\tt \char34}]$, 
		\hyperpage{54}
  \item definition proclamation, \hyperpage{57}
  \item definitition, \hyperpage{9}
  \item dereferencing, \hyperpage{87}
  \item diagnose, \hyperpage{8}, \hyperpage{72, 73}
  \item diagnose hook $[ \mbox {\tt \char34}\mathrm {diagnose}\mbox {\tt \char34}]$, 
		\hyperpage{53}
  \item dictionary, \hyperpage{8}, \hyperpage{49}
  \item dictionary hook $[ \mbox {\tt \char34}\mathrm {dictionary}\mbox {\tt \char34}]$, 
		\hyperpage{52}
  \item domestic definition, \hyperpage{54}

  \indexspace

  \item E: $[ \mathsf{x} {} ^ { E }]$ x is error, \hyperpage{93}
  \item eager, \hyperpage{28}
  \item endorse, \hyperpage{80}
  \item engine, parallel, \hyperpage{25}
  \item \back $[ error_{2}( \lceil \mathsf {m} \rceil , \mathsf {t} )]$ error x term y end error, 
		\hyperpage{92}
  \item \back $[ error_{2}( \mathsf {m} , \mathsf {t} )]$ error two x term y end error, 
		\hyperpage{92}
  \item example axiom $[ \mathsf {T} {}^h = \mathsf {T}]$, 
		\hyperpage{77}
  \item example axiom lemma $[ HeadNil]$, \hyperpage{100}
  \item example axiom lemma primed $[ HeadNil'']$, \hyperpage{95}
  \item example lemma $[ L_{1}]$, \hyperpage{79}
  \item example rack $[ rack]$, \hyperpage{51}
  \item example rule $[ \forall \underline{ \mathsf {a}} \colon \forall \underline{ \mathsf {b}} \colon \forall \underline{ \mathsf {c}} \colon \underline{ \mathsf {a}} =\underline{ \mathsf {b}} \vdash \underline{ \mathsf {a}} =\underline{ \mathsf {c}} \vdash \underline{ \mathsf {b}} =\underline{ \mathsf {c}}]$, 
		\hyperpage{78}
  \item example rule lemma $[ Transitivity]$, \hyperpage{101}
  \item example rule lemma primed $[ Transitivity'']$, \hyperpage{100}
  \item example scheme $[ \forall \underline{ \mathsf {a}} \colon \forall \underline{ \mathsf {b}} \colon \underline{ \mathsf {a}} \mathrel { : \, : }\underline{ \mathsf {b}} {}^h =\underline{ \mathsf {a}}]$, 
		\hyperpage{78}
  \item example scheme lemma $[ HeadPair]$, \hyperpage{101}
  \item example scheme lemma primed $[ HeadPair'']$, \hyperpage{100}
  \item example theory $[ T_E]$, \hyperpage{101}
  \item example theory primed $[ T'_{E}]$, \hyperpage{78}
  \item execute, \hyperpage{9}
  \item exists, symbol, \hyperpage{52}
  \item expander, \hyperpage{61}
  \item expansion, \hyperpage{8, 9}, \hyperpage{61}
  \item expansion hook $[ \mbox {\tt \char34}\mathrm {expansion}\mbox {\tt \char34}]$, 
		\hyperpage{52}

  \indexspace

  \item false test x end test $[ \relax [ \mathsf{x} \relax ]^{-} ]$, 
		\hyperpage{75}
  \item finite function, \hyperpage{45}
  \item first edition engine, \hyperpage{34}
  \item fit for optimization, \hyperpage{36}
  \item flush left, \hyperpage{16}
  \item \back $[ \mathbf{flush\ left\ }[ \mathsf{x} ]]$ flush left x end left, 
		\hyperpage{16}
  \item foreign definition, \hyperpage{54}
  \item free for*: \back $[ \mathsf{x} \mathrel {free\ for}^{\ast} \mathsf{y} \mathrel {in} \mathsf{z}]$ x free for star y in z , 
		\hyperpage{82}
  \item free for: $[ \mathsf{x} \mathrel {free\ for} \mathsf{y} \mathrel {in} \mathsf{z}]$ x free for y in z , 
		\hyperpage{82}
  \item free in*: $[ \mathsf{x} \mathrel {free\ in}^{\ast} \mathsf{y}]$ x free in star y , 
		\hyperpage{82}
  \item free in: $[ \mathsf{x} \mathrel {free\ in} \mathsf{y}]$ x free in y , 
		\hyperpage{82}
  \item function normal form, \hyperpage{24}
  \item function term, \hyperpage{24}

  \indexspace

  \item guard, \hyperpage{28}

  \indexspace

  \item harvesting, \hyperpage{63}
  \item \back $[ Head_{\oplus} ( \mathsf{x} )]$ head x end head, 
		\hyperpage{100}
  \item \back $[ HeadNil'']$ example axiom lemma primed, \hyperpage{95}
  \item \back $[ HeadNil]$ example axiom lemma, \hyperpage{100}
  \item \back $[ \mathsf {T} {}^h = \mathsf {T}]$ example axiom, 
		\hyperpage{77}
  \item \back $[ HeadPair'']$ example scheme lemma primed, 
		\hyperpage{100}
  \item \back $[ HeadPair]$ example scheme lemma, \hyperpage{101}
  \item \back $[ \forall \underline{ \mathsf {a}} \colon \forall \underline{ \mathsf {b}} \colon \underline{ \mathsf {a}} \mathrel { : \, : }\underline{ \mathsf {b}} {}^h =\underline{ \mathsf {a}}]$ example scheme, 
		\hyperpage{78}
  \item hide identifier $[ \mbox {\tt \char34}\mathrm {hide}\mbox {\tt \char34}]$, 
		\hyperpage{57}
  \item hook, \hyperpage{47}

  \indexspace

  \item i.e.: $[ \mathsf{x} \mathrel {i.e.} \mathsf{y}]$ x id est y, 
		\hyperpage{87}
  \item I: $[ \mathsf{x} {} ^ { I }]$ x init, \hyperpage{85}
  \item i: $[ \mathsf{x} {}^{i}]$ x id, \hyperpage{41}
  \item id, \hyperpage{31}
  \item idempotent, \hyperpage{29}
  \item identifier, \hyperpage{10}
  \item \back $[ identifier( \mathsf{x} )]$ identifier x end identifier, 
		\hyperpage{44}
  \item \back $[ identifier_{1}( \mathsf{x} , \mathsf{y} )]$ identifier one x plus id y end identifier, 
		\hyperpage{45}
  \item identifier, Logiweb, \hyperpage{44}
  \item if identifier $[ \mbox {\tt \char34}\mathrm {if}\mbox {\tt \char34}]$, 
		\hyperpage{55}
  \item if, open, \hyperpage{68}
  \item if: $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf{y} ,\linebreak [0] \mathsf{z} )]$ open if x then y else z, 
		\hyperpage{68}
  \item in theory x antilemma y says z end antilemma $ [ \mathsf{x} \mathbf{\ antilemma\ } \mathsf{y} \colon \mathsf{z} ]$, 
		\hyperpage{95}
  \item in theory x antirule y says z end antirule $ [ \mathsf{x} \mathbf{\ antirule\ } \mathsf{y} \colon \mathsf{z} ]$, 
		\hyperpage{100}
  \item in theory x lemma y says z end lemma $ [ \mathsf{x} \mathbf{\ lemma\ } \mathsf{y} \colon \mathsf{z} ]$, 
		\hyperpage{95}
  \item in theory x rule y says z end rule $ [ \mathsf{x} \mathbf{\ rule\ } \mathsf{y} \colon \mathsf{z} ]$, 
		\hyperpage{100}
  \item incompatible, \hyperpage{103}
  \item index (of array), \hyperpage{47}
  \item infer, \hyperpage{80}
  \item inference rule, \hyperpage{78}
  \item inherited page aspect, potentially, \hyperpage{61}
  \item initial macro state, \hyperpage{60}
  \item initial proof state, \hyperpage{106}
  \item \back $[ inst( \mathsf{x} , \mathsf{y} )]$ instantiate x with y end instantiate, 
		\hyperpage{102}
  \item \back $[ inst^*( \mathsf{x} , \mathsf{y} )]$ instantiate star x with y end instantiate, 
		\hyperpage{103}
  \item instance, \hyperpage{103}
  \item instantiate star x with y end instantiate $[ inst^*( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{103}
  \item instantiate x with y end instantiate $[ inst( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{102}
  \item intro * index * pyk * tex * end intro $[ intro( \mathsf{x} , \mathsf {i} , \mathsf {p} , \mathsf {t} )]$, 
		\hyperpage{70}
  \item intro * pyk * tex * end intro $[ intro( \mathsf{x} , \mathsf {p} , \mathsf {t} )]$, 
		\hyperpage{70}
  \item intro: $[ intro( \mathsf{x} , \mathsf {i} , \mathsf {p} , \mathsf {t} )]$ intro * index * pyk * tex * end intro, 
		\hyperpage{70}
  \item intro: $[ intro( \mathsf{x} , \mathsf {p} , \mathsf {t} )]$ intro * pyk * tex * end intro, 
		\hyperpage{70}
  \item introduce identifier $[ \mbox {\tt \char34}\mathrm {introduce}\mbox {\tt \char34}]$, 
		\hyperpage{57}
  \item introduction, \hyperpage{9}

  \indexspace

  \item key, \hyperpage{45}

  \indexspace

  \item \back $[ L_{1}]$ example lemma, \hyperpage{79}
  \item lambda identifier $[ \mbox {\tt \char34}\mathrm {lambda}\mbox {\tt \char34}]$, 
		\hyperpage{55}
  \item \back $[ \mathsf{x} \gg \mathsf{y}]$ because x indeed y qed, 
		\hyperpage{108}
  \item lazy, \hyperpage{29}
  \item left, flush, \hyperpage{16}
  \item lemma, \hyperpage{79}
  \item \back $ [ \mathbf{Lemma\ } \mathsf{x} \colon \mathsf{y} ]$ lemma x says y, 
		\hyperpage{95}
  \item lemma, rule, \hyperpage{88}
  \item lemma, sequent, \hyperpage{84}
  \item lemma: $ [ \mathsf{x} \mathbf{\ lemma\ } \mathsf{y} \colon \mathsf{z} ]$ in theory x lemma y says z end lemma, 
		\hyperpage{95}
  \item let, \hyperpage{69}
  \item \back $[ \mathsf{z}]$ let x abbreviate y in z, \hyperpage{65}
  \item \back $[ let_1( \lambda \mathsf{x} . \mathsf{z} , \mathsf{y} )]$ let x by y in z, 
		\hyperpage{69}
  \item \back $[ let_1( \mathsf{x} , \mathsf{y} )]$ let one x apply y end let, 
		\hyperpage{69}
  \item \back $[ let_2( \mathsf{x} , \mathsf{y} )]$ let two x apply y end let, 
		\hyperpage{69}
  \item liberal, \hyperpage{27}
  \item lifted, untagged cardinal, \hyperpage{29}
  \item \back $[ \mathsf{y} \gg \mathsf{z} ; \mathsf {a}]$ line x because y indeed z end line a, 
		\hyperpage{108}
  \item line x because y indeed z end line a $[ \mathsf{y} \gg \mathsf{z} ; \mathsf {a}]$, 
		\hyperpage{108}
  \item line x premise y end line z $[ \mathsf{y} \vdash \mathsf{z}]$, 
		\hyperpage{108}
  \item line x side condition y end line z $[ \mathsf{y} \mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \mathsf{z}]$, 
		\hyperpage{108}
  \item Lisp property list, \hyperpage{55}
  \item load, \hyperpage{8}, \hyperpage{50}
  \item \back $[ \mathsf{z}]$ locally define x as y end line z, 
		\hyperpage{108}
  \item locally define x as y end line z $[ \mathsf{z}]$, 
		\hyperpage{108}
  \item Logiweb identifier, \hyperpage{44}
  \item Logiweb sequent calculus, \hyperpage{75}

  \indexspace

  \item macro aspect, \hyperpage{59}
  \item macro aspect $[ \mbox {\tt \char34}\mathrm {macro}\mbox {\tt \char34}]$, 
		\hyperpage{54}
  \item macro definition, \hyperpage{59}
  \item macro state, \hyperpage{59}
  \item macro state, initial, \hyperpage{60}
  \item make visible x end visible $[ \mathsf{x}]$, \hyperpage{68}
  \item Map Theory, \hyperpage{76}
  \item math * end math, \hyperpage{111}
  \item mathematically equal, \hyperpage{25}
  \item message, \hyperpage{76}
  \item message aspect $[ \mbox {\tt \char34}\mathrm {message}\mbox {\tt \char34}]$, 
		\hyperpage{54}
  \item message define x as y end define $ [ \mathsf{x} \stackrel {msg}{=} \mathsf{y} ]$, 
		\hyperpage{76}
  \item message proclamation, \hyperpage{56}
  \item metavar x end metavar $[\underline{ \mathsf{x}}]$, 
		\hyperpage{81}
  \item metavariable, \hyperpage{78}
  \item metavariables, \hyperpage{81}
  \item modus, \hyperpage{86}
  \item modus ponens, \hyperpage{86}
  \item modus probans, \hyperpage{86}
  \item \makebox [-1.0\bracketwidth ]{}$[ msg]$ message, \hyperpage{76}
  \item msg: $ [ \mathsf{x} \stackrel {msg}{=} \mathsf{y} ]$ message define x as y end text end define, 
		\hyperpage{76}

  \indexspace

  \item name, tex, \hyperpage{111}
  \item natural number, \hyperpage{7}
  \item \back $[ \mathsf{x}]$ macro newline x, \hyperpage{67}
  \item \back $[ newline\ \mathsf{x}]$ newline x, \hyperpage{67}
  \item newline character, \hyperpage{109}
  \item normal form, \hyperpage{24}
  \item normalization construct, \hyperpage{30}

  \indexspace

  \item \back $[ occur( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ occur x in y substitution z end occur, 
		\hyperpage{103}
  \item \back $[ occur^*( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ occur star x in y substitution z end occur, 
		\hyperpage{103}
  \item occur star x in y substitution z end occur $[ occur^*( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{103}
  \item occur x in y substitution z end occur $[ occur( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{103}
  \item off-stage semantics, \hyperpage{34}
  \item on-stage semantics, \hyperpage{34}
  \item open if, \hyperpage{68}
  \item open if x then y else z $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf{y} ,\linebreak [0] \mathsf{z} )]$, 
		\hyperpage{68}
  \item operation over, \hyperpage{36}
  \item operation, sequent, \hyperpage{84}
  \item ordinal number, \hyperpage{29}
  \item ordinary variable, \hyperpage{78}

  \indexspace

  \item p: $[ p_0]$ proof state, \hyperpage{106}
  \item p: $[ {\cal P}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ proof expand x state y cache z end expand, 
		\hyperpage{106}
  \item p: $[ {\cal P}^*( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ proof expand list x state y cache z end expand, 
		\hyperpage{106}
  \item page aspect, potentially inherited, \hyperpage{61}
  \item page bed, \hyperpage{61}
  \item page construct, \hyperpage{10}, \hyperpage{51}
  \item parallel engine, \hyperpage{25}
  \item parameter term, \hyperpage{102}
  \item parameter term star x stack y seed z end parameter $[ parm^*( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{102}
  \item parameter term x stack y seed z end parameter $[ parm( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{102}
  \item \back $[ parm( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ parameter term x stack y seed z end parameter, 
		\hyperpage{102}
  \item \back $[ parm^*( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ parameter term star x stack y seed z end parameter, 
		\hyperpage{102}
  \item Peano tree, \hyperpage{27}
  \item perpetual, \hyperpage{24}
  \item \back $[ Plus( \mathsf{x} , \mathsf{y} )]$ plus x and y end plus, 
		\hyperpage{101}
  \item plus, rule, \hyperpage{80}
  \item ponens, modus, \hyperpage{86}
  \item post identifier $[ \mbox {\tt \char34}\mathrm {post}\mbox {\tt \char34}]$, 
		\hyperpage{57}
  \item potentially inherited page aspect, \hyperpage{61}
  \item pre identifier $[ \mbox {\tt \char34}\mathrm {pre}\mbox {\tt \char34}]$, 
		\hyperpage{57}
  \item predefined concept, \hyperpage{23}
  \item premise, \hyperpage{78}, \hyperpage{83}
  \item \back $[ \mathsf{y} \vdash \mathsf{z}]$ line x premise y end line z, 
		\hyperpage{108}
  \item priority aspect $[ \mbox {\tt \char34}\mathrm {priority}\mbox {\tt \char34}]$, 
		\hyperpage{54}
  \item priority proclamation, \hyperpage{57}
  \item \back $[ [ \mbox{base} \stackrel{ \mathrm{prio} }{\rightarrow} \mathsf{x} ]]$ priority table x end table, 
		\hyperpage{66}
  \item probans, modus, \hyperpage{86}
  \item proclaim identifier $[ \mbox {\tt \char34}\mathrm {proclaim}\mbox {\tt \char34}]$, 
		\hyperpage{57}
  \item proclamation, \hyperpage{9}
  \item proclamation construct, \hyperpage{10}
  \item \back $[ proof( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ proof x term y cache z end proof, 
		\hyperpage{94}
  \item \back $[ {<}proof{>}]$ the proof aspect, \hyperpage{95}
  \item proof $[ proof]$, \hyperpage{95}
  \item \back $[ proof_{2}( \mathsf{x} , \mathsf{y} )]$ proof two x term y end proof, 
		\hyperpage{94}
  \item proof aspect, \hyperpage{95}
  \item proof expander, \hyperpage{104}
  \item \back $ [ \mathbf{Proof\ of\ } \mathsf{x} \colon \mathsf{y} ]$ proof of x read y end proof, 
		\hyperpage{95}
  \item proof state, \hyperpage{106}
  \item proof state, initial, \hyperpage{106}
  \item proof tactic, \hyperpage{104}
  \item proof x term y cache z end proof $ proof( \mathsf{x} , \mathsf{y} , \mathsf{z} )$, 
		\hyperpage{94}
  \item proof, sequent, \hyperpage{84}
  \item property list, Lisp, \hyperpage{55}
  \item proves: $ proof( \lceil \mathsf{x} \rceil , \lceil \mathsf{y} \rceil , \mbox{base} )$ x proves y, 
		\hyperpage{93}
  \item pruning, \hyperpage{60}
  \item pure lambda calculus, \hyperpage{23}
  \item pyk, \hyperpage{162}
  \item pyk aspect, \hyperpage{12}
  \item pyk aspect $[ \mbox {\tt \char34}\mathrm {pyk}\mbox {\tt \char34}]$, 
		\hyperpage{54}

  \indexspace

  \item quote, \hyperpage{41}
  \item quote identifier $[ \mbox {\tt \char34}\mathrm {quote}\mbox {\tt \char34}]$, 
		\hyperpage{55}

  \indexspace

  \item r: $[ \mathsf{x} \stackrel{r}{=} \mathsf{y}]$ x term root equal y, 
		\hyperpage{41}
  \item r: $[ \mathsf{x} {}^{r}]$ x ref, \hyperpage{41}
  \item R: $[ \mathsf{x} {}^{R}]$ x root, \hyperpage{41}
  \item rack, \hyperpage{47}, \hyperpage{50}
  \item \back $[ rack]$ example rack, \hyperpage{51}
  \item ragged right, \hyperpage{16}, \hyperpage{67}
  \item \back $[ ragged\ right]$ ragged right, \hyperpage{67}
  \item \back $[ ragged\ right]$ ragged right expansion, \hyperpage{67}
  \item raw, \hyperpage{27}
  \item raw test x end test $[ \relax [ \mathsf{x} \relax ]^{\circ} ]$, 
		\hyperpage{75}
  \item reduction system, \hyperpage{24}
  \item reference, \hyperpage{7}, \hyperpage{10}
  \item reference cardinal, \hyperpage{31}
  \item referencing, \hyperpage{87}
  \item \back $[ Reflexivity]$ sequent reflexivity, \hyperpage{102}
  \item \back $[ Reflexivity_1]$ tactic reflexivity, \hyperpage{105}
  \item regular, \hyperpage{32}
  \item \back $[ \forall \underline{ \mathsf {a}} \colon \forall \underline{ \mathsf {b}} \colon \underline{ \mathsf {a}} \mathrel { : \, : }\underline{ \mathsf {b}} {}^h =\underline{ \mathsf {a}} \mathrel {\oplus} \forall \underline{ \mathsf {a}} \colon \forall \underline{ \mathsf {b}} \colon \forall \underline{ \mathsf {c}} \colon \underline{ \mathsf {a}} =\underline{ \mathsf {b}} \vdash \underline{ \mathsf {a}} =\underline{ \mathsf {c}} \vdash \underline{ \mathsf {b}} =\underline{ \mathsf {c}} \mathrel {\oplus} \mathsf {T} \mathrel { : \, : } \mathsf {T} = \mathsf {T} \vdash {\makebox [0mm][l]{$\bot $}\,{\bot }}]$, 
		\hyperpage{88}
  \item resolve, \hyperpage{9}
  \item retract, \hyperpage{30}
  \item retrieve, \hyperpage{9}
  \item return $[ \bot ]$, \hyperpage{26}
  \item revelation, \hyperpage{9}, \hyperpage{34}
  \item right, ragged, \hyperpage{16}, \hyperpage{67}
  \item root equivalent, \hyperpage{24}
  \item root normal form, \hyperpage{24}
  \item rule, \hyperpage{78}
  \item \back $[ rule( \mathsf{x} , \mathsf{y} )]$ rule x subcodex y end rule, 
		\hyperpage{99}
  \item \back $[ rule_1( \mathsf{x} , \mathsf{y} )]$ rule one x theory y end rule, 
		\hyperpage{99}
  \item rule lemma, \hyperpage{88}
  \item rule plus, \hyperpage{80}
  \item \back $[ Rule\ tactic]$ rule tactic, \hyperpage{99}
  \item rule, inference, \hyperpage{78}
  \item rule: $ [ \mathsf{x} \mathbf{\ rule\ } \mathsf{y} \colon \mathsf{z} ]$ in theory x rule y says z end rule, 
		\hyperpage{100}

  \indexspace

  \item s: $[ \mathsf{x} \stackrel{s}{=} \mathsf{y}]$, \hyperpage{84}
  \item S: $[ {\cal S}( \mathsf{x} , \mathsf{y} )]$ sequent eval x term y end eval, 
		\hyperpage{93}
  \item S: $[ {\cal S}^{+}( \mathsf{x} , \mathsf{y} )]$ sequent eval plus x term y end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}^{-}( \mathsf{x} , \mathsf{y} )]$ seqeval minus x term y end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}^{;}( \mathsf{x} , \mathsf{y} )]$ seqeval cut x term y end eval, 
		\hyperpage{91}
  \item S: $[ {\cal S}^{\ast}( \mathsf{x} , \mathsf{y} )]$ seqeval deref x term y end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}^{\char64}( \mathsf{x} , \mathsf{y} )]$ seqeval at x term y end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}^{\forall}( \mathsf{x} , \mathsf{y} )]$ seqeval all x term y end eval, 
		\hyperpage{91}
  \item S: $[ {\cal S}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}( \mathsf{x} , \mathsf{y} )]$ seqeval endorse x term y end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}^{\rhd}( \mathsf{x} , \mathsf{y} )]$ seqeval modus x term y end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}^{\vdash}( \mathsf{x} , \mathsf{y} )]$ seqeval infer x term y end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}^{E}( \mathsf{x} , \mathsf{y} )]$ seqeval verify x term y end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}^{i.e.}( \mathsf{x} , \mathsf{y} )]$ seqeval est x term y end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}^{I}( \mathsf{x} , \mathsf{y} )]$ seqeval init x term y end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}_{1}^{+}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ seqeval plus one x term y sequent z end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}_{1}^{-}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ seqeval minus one x term y sequent z end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}_{1}^{;}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ seqeval cut one x term y forerunner z end eval, 
		\hyperpage{91}
  \item S: $[ {\cal S}_{1}^{\ast}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ seqeval deref one x term y sequent z end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}_{1}^{\char64}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ seqeval at one x term y sequent x end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}_{1}^{\forall}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$ seqeval all one x term y variable z sequent u end eval, 
		\hyperpage{91}
  \item S: $[ {\cal S}_{1}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$ seqeval endorse one x term y side z sequent u end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}_{1}^{\rhd}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ seqeval modus one x term y sequent z end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}_{1}^{\vdash}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$ seqeval infer one x term y premise z sequent u end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}_{1}^{E}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ seqeval verify one x term y sequent z end eval, 
		\hyperpage{89}
  \item S: $[ {\cal S}_{1}^{i.e.}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$ seqeval est one x term y name z sequent u end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}_{2}^{;}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$ seqeval cut two x term y sequent u end eval, 
		\hyperpage{91}
  \item S: $[ {\cal S}_{2}^{\ast}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$ seqeval deref two x term y sequent z def u end eval, 
		\hyperpage{90}
  \item S: $[ {\cal S}_{2}^{i.e.}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} , \mathsf {v} )]$ seqeval est two x term y name z sequent u def v end eval, 
		\hyperpage{90}
  \item scheme, axiom, \hyperpage{78}
  \item self-evaluating, \hyperpage{68}
  \item semitagged, \hyperpage{33}
  \item seqeval all one x term y variable z sequent u end eval $[ {\cal S}_{1}^{\forall}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$, 
		\hyperpage{91}
  \item seqeval all x term y end eval $[ {\cal S}^{\forall}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{91}
  \item seqeval at one x term y sequent z end eval $[ {\cal S}_{1}^{\char64}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{90}
  \item seqeval at x term y end eval $[ {\cal S}^{\char64}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{90}
  \item seqeval cut one x term y forerunner z end eval $[ {\cal S}_{1}^{;}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{91}
  \item seqeval cut two x term y forerunner z sequent u end eval $[ {\cal S}_{2}^{;}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$, 
		\hyperpage{91}
  \item seqeval cut x term y end eval $[ {\cal S}^{;}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{91}
  \item seqeval deref one x term y sequent z end eval $[ {\cal S}_{1}^{\ast}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{90}
  \item seqeval deref two x term y sequent z def u end eval $[ {\cal S}_{2}^{\ast}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$, 
		\hyperpage{90}
  \item seqeval deref x term y end eval $[ {\cal S}^{\ast}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{89}
  \item seqeval endorse one x term y side z sequent u end eval $[ {\cal S}_{1}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$, 
		\hyperpage{90}
  \item seqeval endorse x term y end eval $[ {\cal S}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{90}
  \item seqeval est one x term y name z sequent u end eval $[ {\cal S}_{1}^{i.e.}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$, 
		\hyperpage{90}
  \item seqeval est two x term y name z sequent u def v end eval $[ {\cal S}_{2}^{i.e.}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} , \mathsf {v} )]$, 
		\hyperpage{90}
  \item seqeval est x term y end eval $[ {\cal S}^{i.e.}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{90}
  \item seqeval infer one x term y premise z sequent u end eval $[ {\cal S}_{1}^{\vdash}( \mathsf{x} , \mathsf{y} , \mathsf{z} , \mathsf {u} )]$, 
		\hyperpage{90}
  \item seqeval infer x term y end eval $[ {\cal S}^{\vdash}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{90}
  \item seqeval init x term y end eval $[ {\cal S}^{I}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{89}
  \item seqeval minus one x term y sequent z end eval $[ {\cal S}_{1}^{-}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{89}
  \item seqeval minus x term y end eval $[ {\cal S}^{-}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{89}
  \item seqeval modus one x term y sequent z end eval $[ {\cal S}_{1}^{\rhd}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{89}
  \item seqeval modus x term y end eval $[ {\cal S}^{\rhd}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{89}
  \item seqeval plus one x term y sequent z end eval $[ {\cal S}_{1}^{+}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{89}
  \item seqeval verify one x term y sequent z end eval $[ {\cal S}_{1}^{E}( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{89}
  \item seqeval verify x term y end eval $[ {\cal S}^{E}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{89}
  \item sequent, \hyperpage{83}
  \item sequent calculus, \hyperpage{75}
  \item sequent commutativity $[ Commutativity]$, \hyperpage{102}
  \item sequent eval plus x term y end eval $[ {\cal S}^{+}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{89}
  \item sequent eval x term y end eval $[ {\cal S}( \mathsf{x} , \mathsf{y} )]$, 
		\hyperpage{93}
  \item sequent operation, \hyperpage{84}
  \item sequent proof, \hyperpage{84}
  \item sequent reflexivity $[ Reflexivity]$, \hyperpage{102}
  \item side condition, \hyperpage{83}
  \item \back $[ \mathsf{y} \mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \mathsf{z}]$ line x side condition y end line z, 
		\hyperpage{108}
  \item singular, \hyperpage{32}
  \item stack, \hyperpage{49}
  \item statement, \hyperpage{77}, \hyperpage{79}
  \item statement $[ stmt]$, \hyperpage{77}
  \item statement aspect, \hyperpage{77}
  \item statement define x as y end define $ [ \mathsf{x} \stackrel {stmt}{=} \mathsf{y} ]$, 
		\hyperpage{77}
  \item \back $[ {<}stmt{>}]$ the statement aspect, \hyperpage{77}
  \item \makebox [-1.0\bracketwidth ]{}$[ stmt]$ statement, 
		\hyperpage{77}
  \item stmt: $ [ \mathsf{x} \stackrel {stmt}{=} \mathsf{y} ]$, 
		\hyperpage{77}
  \item strict, \hyperpage{28}, \hyperpage{35}
  \item strict variable, \hyperpage{37}
  \item sub star x set y to z end sub $[ \langle ^ { \ast } \mathsf{x} \,{\protect\vert} \mathsf{y} {:=}\, \mathsf{z} \rangle ]$, 
		\hyperpage{82}
  \item sub x set y to z end sub $[ \langle \mathsf{x} \,{\protect\vert} \mathsf{y} {:=}\, \mathsf{z} \rangle ]$, 
		\hyperpage{82}
  \item subcodex, \hyperpage{55}
  \item symbol, \hyperpage{10}
  \item symbol exists, \hyperpage{52}

  \indexspace

  \item \back $[ T_E]$ example theory, \hyperpage{101}
  \item \back $[ \lambda \mathsf {c} . {\cal U}^M( {\cal E}( \lceil \mathsf{x} \rceil , \mathsf {T} , \mathsf {c} ) )]$ computably true x end true, 
		\hyperpage{87}
  \item \back $[ T'_{E}]$ example theory primed, \hyperpage{78}
  \item t: $[ \mathsf{x} \in_t \mathsf{y}]$, \hyperpage{83}
  \item T: $[ \mathsf{x} \stackrel{T}{=} \mathsf{y}]$, \hyperpage{83}
  \item T: $[ \mathsf{x} \subseteq_T \mathsf{y}]$, \hyperpage{83}
  \item \back $[ {<}tactic{>}]$ the tactic aspect, \hyperpage{106}
  \item tactic $[ tactic]$, \hyperpage{106}
  \item tactic aspect, \hyperpage{104}
  \item tactic commutativity $[ Commutativity_1]$, \hyperpage{105}
  \item tactic define x as y end define $ [ \mathsf{x} \stackrel {tactic}{=} \mathsf{y} ]$, 
		\hyperpage{106}
  \item tactic reflexivity $[ Reflexivity_1]$, \hyperpage{105}
  \item tactic, conclusion, \hyperpage{107}
  \item tactic, proof, \hyperpage{104}
  \item tactic: $ [ \mathsf{x} \stackrel {tactic}{=} \mathsf{y} ]$, 
		\hyperpage{106}
  \item tag, \hyperpage{30}
  \item tagged cardinal, \hyperpage{30}
  \item tagged map, \hyperpage{31}
  \item tagged pair, \hyperpage{31}
  \item tagged Peano tree, \hyperpage{31}
  \item tagged tree, \hyperpage{31}
  \item \back $[ Tail_{\oplus} ( \mathsf{x} )]$ tail x end tail, 
		\hyperpage{100}
  \item term, parameter, \hyperpage{102}
  \item test x end test $[ \relax [ \mathsf{x} \relax ]^{\cdot} ]$, 
		\hyperpage{74}
  \item \back $[ \mathrm{tex}]$ tex, \hyperpage{12}
  \item tex aspect, \hyperpage{12}
  \item tex aspect $[ \mbox {\tt \char34}\mathrm {tex}\mbox {\tt \char34}]$, 
		\hyperpage{54}
  \item tex name, \hyperpage{111}
  \item texname aspect $[ \mbox {\tt \char34}\mathrm {texname}\mbox {\tt \char34}]$, 
		\hyperpage{54}
  \item the empty set $[ \emptyset ]$, \hyperpage{83}
  \item the proof aspect $[ {<}proof{>}]$, \hyperpage{95}
  \item the statement aspect $[ {<}stmt{>}]$, \hyperpage{77}
  \item the tactic aspect $[ {<}tactic{>}]$, \hyperpage{106}
  \item theory, \hyperpage{78}
  \item \back $ [ \mathbf{Theory\ } \mathsf{x} ]$ theory x end theory, 
		\hyperpage{101}
  \item \back $[ theory_2( \mathsf{x} , \mathsf{y} )]$ theory two x cache y end theory, 
		\hyperpage{101}
  \item \back $[ theory_3( \mathsf{x} , \mathsf{y} )]$ theory three x name y end theory, 
		\hyperpage{101}
  \item \back $[ theory_4( \mathsf{x} , \mathsf{y} , \mathsf{z} )]$ theory four x name var y sum z end theory, 
		\hyperpage{101}
  \item transitive bibliography, \hyperpage{50}
  \item \back $[ Transitivity'']$ example rule lemma primed, 
		\hyperpage{100}
  \item \back $[ Transitivity]$ example rule lemma, \hyperpage{101}
  \item \back $[ \forall \underline{ \mathsf {a}} \colon \forall \underline{ \mathsf {b}} \colon \forall \underline{ \mathsf {c}} \colon \underline{ \mathsf {a}} =\underline{ \mathsf {b}} \vdash \underline{ \mathsf {a}} =\underline{ \mathsf {c}} \vdash \underline{ \mathsf {b}} =\underline{ \mathsf {c}}]$ example rule, 
		\hyperpage{78}
  \item true identifier $[ \mbox {\tt \char34}\mathrm {true}\mbox {\tt \char34}]$, 
		\hyperpage{55}
  \item true term, \hyperpage{24}
  \item truth normal form, \hyperpage{24}
  \item \back $[ \mathbf {tuple}_1( \mathsf {t} ) ]$, \hyperpage{66}
  \item \back $[ \mathbf {tuple}_2( \mathsf {t} ) ]$, \hyperpage{66}
  \item tuple x end tuple $[ \mathsf{x} \mathrel { : \, : } \mathsf {T}]$, 
		\hyperpage{66}
  \item type, \hyperpage{36}

  \indexspace

  \item uncolored, \hyperpage{91}
  \item unification, \hyperpage{103}
  \item unification algorithm, \hyperpage{103}
  \item unify, \hyperpage{103}
  \item \back $[ unify( \mathsf{x} = \mathsf{y} , \mathsf{z} )]$ unify x with y substitution z end unify, 
		\hyperpage{104}
  \item \back $[ unify^*( \mathsf{x} = \mathsf{y} , \mathsf{z} )]$ unify star x with y substitution z end unify, 
		\hyperpage{104}
  \item \back $[ unify_2( \mathsf{x} = \mathsf{y} , \mathsf{z} )]$ unify two x with y substitution z end unify, 
		\hyperpage{104}
  \item unify star x with y substitution z end unify $[ unify^*( \mathsf{x} = \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{104}
  \item unify two x with y substitution z end unify $[ unify_2( \mathsf{x} = \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{104}
  \item unify x with y substitution z end unify $[ unify( \mathsf{x} = \mathsf{y} , \mathsf{z} )]$, 
		\hyperpage{104}
  \item unpack, \hyperpage{9}
  \item unpack aspect $[ \mbox {\tt \char34}\mathrm {unpack}\mbox {\tt \char34}]$, 
		\hyperpage{54}

  \indexspace

  \item \back $[ {\cal V}_1( \mathsf {c} )]$ verify one c end verify, 
		\hyperpage{96}
  \item \back $[ {\cal V}_2( \mathsf {c} , \mathsf {p} )]$ verify two c proofs p end verify, 
		\hyperpage{96}
  \item \back $[ {\cal V}_3( \mathsf {c} , \mathsf {r} , \mathsf {p} , \mathsf {d} )]$ verify three c ref r sequents p diagnose d end verify, 
		\hyperpage{97}
  \item \back $[ {\cal V}_4( \mathsf {c} , \mathsf {p} )]$ verify four c premises p end verify, 
		\hyperpage{97}
  \item \back $[ {\cal V}_5( \mathsf {c} , \mathsf {r} , \mathsf {a} , \mathsf {q} )]$ verify five c ref r array a sequents q end verify, 
		\hyperpage{98}
  \item \back $[ {\cal V}_6( \mathsf {c} , \mathsf {r} , \mathsf {p} , \mathsf {q} )]$ verify six c ref r list p sequents q end verify, 
		\hyperpage{98}
  \item \back $[ {\cal V}_7( \mathsf {c} , \mathsf {r} , \mathsf {i} , \mathsf {q} )]$ verify seven c ref r id i sequents q end verify, 
		\hyperpage{98}
  \item V: $[ \mathsf{x} {} ^ { V } ]$ x verify, \hyperpage{86}
  \item V: $[ \mathsf{x} {} ^ {\cal V}]$ x is metavar, \hyperpage{81}
  \item v: \back $[ \mathsf{x}]$ make visible x end visible, 
		\hyperpage{68}
  \item value, \hyperpage{45}
  \item value aspect, \hyperpage{25}
  \item value aspect $[ \mbox {\tt \char34}\mathrm {value}\mbox {\tt \char34}]$, 
		\hyperpage{54}
  \item value proclamation, \hyperpage{55}
  \item variable, meta, \hyperpage{78}
  \item variable, ordinary, \hyperpage{78}
  \item vector, \hyperpage{7}
  \item vector hook $[ \mbox {\tt \char34}\mathrm {vector}\mbox {\tt \char34}]$, 
		\hyperpage{51}
  \item verification, \hyperpage{86}
  \item \back $[ \mbox{verifier}]$ verifier, \hyperpage{96}
  \item verify, \hyperpage{9}
  \item verify five c ref r array a sequents q end verify $[ {\cal V}_5( \mathsf {c} , \mathsf {r} , \mathsf {a} , \mathsf {q} )]$ verify five c ref r array a sequents q end verify, 
		\hyperpage{98}
  \item verify four c premises p end verify $[ {\cal V}_4( \mathsf {c} , \mathsf {p} )]$, 
		\hyperpage{97}
  \item verify one c end verify $[ {\cal V}_1( \mathsf {c} )]$, 
		\hyperpage{96}
  \item verify seven c ref r id i sequents q end verify $[ {\cal V}_7( \mathsf {c} , \mathsf {r} , \mathsf {i} , \mathsf {q} )]$, 
		\hyperpage{98}
  \item verify six c ref r list p sequents q end verify $[ {\cal V}_6( \mathsf {c} , \mathsf {r} , \mathsf {p} , \mathsf {q} )]$, 
		\hyperpage{98}
  \item verify three c ref r sequents p diagnose d end verify $[ {\cal V}_3( \mathsf {c} , \mathsf {r} , \mathsf {p} , \mathsf {d} )]$, 
		\hyperpage{97}
  \item verify two c proofs p end verify $[ {\cal V}_2( \mathsf {c} , \mathsf {p} )]$, 
		\hyperpage{96}
  \item visibility, \hyperpage{68}

  \indexspace

  \item x at y $[ \mathsf{x} \mathop {\char64} \mathsf{y}]$, 
		\hyperpage{86}
  \item x claim and y $[ \mathsf{x} \wedge_c \mathsf{y}]$, 
		\hyperpage{73}
  \item x claim in y $[ \mathsf{x} \in_c \mathsf{y}]$, \hyperpage{94}
  \item x color star y end color $[ \mathsf{x} \mbox {-color}^{\ast}( \mathsf{y} )]$, 
		\hyperpage{92}
  \item x color y end color $[ \mathsf{x} \mbox {-color}( \mathsf{y} )]$, 
		\hyperpage{91}
  \item x comma y $[ \mathsf{x} ,\linebreak [0] \mathsf{y}]$, 
		\hyperpage{66}
  \item x curry minus $[ \mathsf{x} {} ^ { - } ]$, \hyperpage{87}
  \item x curry plus $[ \mathsf{x} {} ^ { + } ]$, \hyperpage{87}
  \item x cut y $[ \mathsf{x} ; \mathsf{y}]$, \hyperpage{87}
  \item x debug $[ \mathsf{x} {}^{d}]$, \hyperpage{41}
  \item x dereference $[ \mathsf{x} {} ^ { \ast } ]$, \hyperpage{87}
  \item x endorse y $[ \mathsf{x} \mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \mathsf{y}]$, 
		\hyperpage{80}
  \item x first $[ \mathsf{x} {}^{1}]$, \hyperpage{32}
  \item x free for star y in z $[ \mathsf{x} \mathrel {free\ for}^{\ast} \mathsf{y} \mathrel {in} \mathsf{z}]$, 
		\hyperpage{82}
  \item x free for y in z $[ \mathsf{x} \mathrel {free\ for} \mathsf{y} \mathrel {in} \mathsf{z}]$, 
		\hyperpage{82}
  \item x free in star y $[ \mathsf{x} \mathrel {free\ in}^{\ast} \mathsf{y}]$, 
		\hyperpage{82}
  \item x free in y $[ \mathsf{x} \mathrel {free\ in} \mathsf{y}]$, 
		\hyperpage{82}
  \item x id $[ \mathsf{x} {}^{i}]$, \hyperpage{41}
  \item x id est y $[ \mathsf{x} \mathrel {i.e.} \mathsf{y}]$, 
		\hyperpage{87}
  \item x infer y $[ \mathsf{x} \vdash \mathsf{y}]$, \hyperpage{80}
  \item x init $[ \mathsf{x} {} ^ { I }]$, \hyperpage{85}
  \item x is error $[ \mathsf{x} {} ^ { E }]$, \hyperpage{93}
  \item x is metaclosed $[ \mathsf{x} {} ^ {\cal C}]$, \hyperpage{81}
  \item x is metaclosed star $[ \mathsf{x} {} ^ {{\cal C} ^ { \ast }}]$, 
		\hyperpage{81}
  \item x is metavar $[ \mathsf{x} {} ^ {\cal V}]$, \hyperpage{81}
  \item x less one y $[ \mathsf{x} \le' \mathsf{y}]$, \hyperpage{40}
  \item x less y $[ \mathsf{x} < \mathsf{y}]$, \hyperpage{39}
  \item x less zero y $[ \mathsf{x} <' \mathsf{y}]$, \hyperpage{40}
  \item x macro and y $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf{y} ,\linebreak [0] \mathsf {F} )]$, 
		\hyperpage{69}
  \item x macro imply y $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf{y} ,\linebreak [0] \mathsf {T} )]$, 
		\hyperpage{69}
  \item x macro or y $[ \mathrm {If}( \mathsf{x} ,\linebreak [0] \mathsf {T} ,\linebreak [0] \mathsf{y} )]$, 
		\hyperpage{69}
  \item x minus one y $[ \mathsf{x} \mathop{-_1} \mathsf{y}]$, 
		\hyperpage{40}
  \item x minus y $[ \mathsf{x} - \mathsf{y}]$, \hyperpage{40}
  \item x minus zero y $[ \mathsf{x} \mathop{-_0} \mathsf{y}]$, 
		\hyperpage{40}
  \item x modus $[ \mathsf{x} {} ^ { \rhd }]$, \hyperpage{86}
  \item x plus one y $[ \mathsf{x} \mathop{+_1} \mathsf{y}]$, 
		\hyperpage{39}
  \item x plus y $[ \mathsf{x} + \mathsf{y}]$, \hyperpage{39}
  \item x plus zero y $[ \mathsf{x} \mathop{+_0} \mathsf{y}]$, 
		\hyperpage{39}
  \item x prime $[ \mathsf{x}']$, \hyperpage{49}
  \item x proves y: $ proof( \lceil \mathsf{x} \rceil , \lceil \mathsf{y} \rceil , \mbox{base} )$, 
		\hyperpage{93}
  \item x ref $[ \mathsf{x} {}^{r}]$, \hyperpage{41}
  \item x root $[ \mathsf{x} {}^{R}]$, \hyperpage{41}
  \item x rule plus y $[ \mathsf{x} \mathrel {\oplus} \mathsf{y}]$, 
		\hyperpage{80}
  \item x sequent equal y $[ \mathsf{x} \stackrel{s}{=} \mathsf{y}]$, 
		\hyperpage{84}
  \item x set multi y to z end set $[ \mathsf{x} [ \mathsf{y} {\Rightarrow} \mathsf{z} ]]$t, 
		\hyperpage{48}
  \item x set y to z end set $[ \mathsf{x} [ \mathsf{y} {\rightarrow} \mathsf{z} ]]$t, 
		\hyperpage{47}
  \item x simple and y $[ \mathsf{x} \mathrel{\tilde{\wedge}} \mathsf{y}]$, 
		\hyperpage{73}
  \item x term in y $[ \mathsf{x} \in_t \mathsf{y}]$, \hyperpage{83}
  \item x term minus var y end minus $[ \mathsf{x} \backslash \{ \mathsf{y} \}]$, 
		\hyperpage{83}
  \item x term plus var y end plus $[ \mathsf{x} \cup \{ \mathsf{y} \}]$, 
		\hyperpage{83}
  \item x term root equal y $[ \mathsf{x} \stackrel{r}{=} \mathsf{y}]$, 
		\hyperpage{41}
  \item x term set equal y $[ \mathsf{x} \stackrel{T}{=} \mathsf{y}]$, 
		\hyperpage{83}
  \item x term subset y $[ \mathsf{x} \subseteq_T \mathsf{y}]$, 
		\hyperpage{83}
  \item x term union y $[ \mathsf{x} \cup \mathsf{y}]$, \hyperpage{83}
  \item x times y $[ \mathsf{x} \cdot \mathsf{y}]$, \hyperpage{40}
  \item x times zero y $[ \mathsf{x} \cdot_0 \mathsf{y}]$, 
		\hyperpage{40}
  \item x verify $[ \mathsf{x} {} ^ { V } ]$, \hyperpage{86}

  \indexspace

  \item zero dimensional array, \hyperpage{47}

\end{theindex}