+ <div class="head2">System's Syntax and Behavior</div>
+ <div class="text">This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns text grey">domain</td><td class="snns plane grey">block</td><td class="snns text grey">leader</td><td class="snns text grey">applicator (with →θ)*</td><td class="snns text grey">reduction</td><td class="snns text grey">→ζ *</td><td class="ssns text grey">reference *</td></tr><tr><td class="snns text">{X | Γ ⊢ X : W}</td><td class="snns plane wine">typed abstraction **</td><td class="snns text wine">Γ ⊢ λW</td><td class="snns text wine">ⓐV</td><td class="snns text wine">→β</td><td class="snns text wine">no</td><td class="ssns text wine">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane magenta">typed declaration ***</td><td class="snns text magenta">Γ ⊢ pλW</td><td class="snns text magenta">no</td><td class="snns text magenta">no</td><td class="snns text magenta">no</td><td class="ssns text magenta">$p</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane prune">native type annotation *</td><td class="snns text prune">Γ ⊢ ⓣW</td><td class="snns text prune">no</td><td class="snns text prune">no</td><td class="snns text prune">yes</td><td class="ssns text prune">no</td></tr><tr><td class="snns text">{X | Γ ⊢ X = V}</td><td class="snns plane blue">local abbreviation **</td><td class="snns text blue">Γ ⊢ δV</td><td class="snns text blue">no</td><td class="snns text blue">local →δ</td><td class="snns text blue">yes</td><td class="ssns text blue">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane sky">global abbreviation ***</td><td class="snns text sky">Γ ⊢ pδV</td><td class="snns text sky">no</td><td class="snns text sky">global →δ</td><td class="snns text sky">no</td><td class="ssns text sky">$p</td></tr><tr><td class="snss text">no</td><td class="snss plane cyan">sort ****</td><td class="snss text cyan">Γ ⊢ ⋆k</td><td class="snss text cyan">no</td><td class="snss text cyan">no</td><td class="snss text cyan">no</td><td class="ssss text cyan">no</td></tr></tbody></table></div>
+ <div class="text">* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </div>
+
+ <div class="head2">Summary of the Specification</div>
+ <div class="text">Here is a numerical acount of the specification's contents
+ and its timeline.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">46</td><td class="snns plane green">lemmas</td><td class="ssnn number green">405</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">35</td><td class="snss plane yellow">defined</td><td class="sssn number yellow">49</td></tr></tbody></table></div>
+ <ul><li><span class="date">In progress.</span>
+ Context-sensitive strong normalization of simply typed terms.
+ </li></ul>
+ <ul><li><span class="date">2012 January 27.</span>
+ Support for abstract candidates of reducibility closed.
+ </li></ul>
+ <ul><li><span class="date">2011 September 21.</span>
+ Confluence of context-sensitive parallel reduction closed.
+ </li></ul>
+ <ul><li><span class="date">2011 September 6.</span>
+ Confluence of context-free parallel reduction closed.
+ </li></ul>
+ <ul><li><span class="date">2011 April 17.</span>
+ Specification started.
+ </li></ul>
+
+ <div class="head2">Logical Structure of the Specification</div>