--- a/semantics/prov-sem.html	Thu Jan 10 14:10:41 2013 +0000
+++ b/semantics/prov-sem.html	Thu Jan 10 14:31:02 2013 +0000
@@ -1016,28 +1016,8 @@
 </section>
 </section>
 
-<section id="test">
-<h2>MathJax test</h2>
-
-\(\newcommand{\wasDerivedFrom}{\mathit{wasDerivedFrom}}\)
-\(\newcommand{\wasInformedBy}{\mathit{wasInformedBy}}\)
-\(\newcommand{\wasGeneratedBy}{\mathit{wasGeneratedBy}}\)
-\(\newcommand{\used}{\mathit{used}}\)
-\(\newcommand{\entity}{\mathit{entity}}\)
-\(\newcommand{\activity}{\mathit{activity}}\)
 
-<p>When $a \ne 0$, there are two solutions to \(ax^2 + bx + c = 0\) and they are
-</p>
-$$x = {-b \pm \sqrt{b^2-4ac} \over 2a}.$$
-
-<div class="inference" id="communication-generation-use-inference_test">
-\(\forall id,a_2,a_1,attrs.~ \wasInformedBy(id,a_2,a_1,attrs) \Longrightarrow \exists e,gen,t_1,use,t_2.~\wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge \used(use,a_2,e,t_2,[])\)</div>
-
-</section>
-
-<section id="wiki">
-<h2> Wiki stuff </h2>
-
+<section id="overview">
 <h2> Overview </h2>
 
 
@@ -1065,6 +1045,9 @@
 
 <p>One goal of the semantics is to link the procedural specification of validity and equivalence with traditional notions of logical consistency and equivalence of theories, for example in first-order logic.  A first-order axiomatization that corresponds to the formal constraints and is sound for reasoning about the models described below is in progress at the end of the document.
 </p>
+</section>
+
+<section id="basics">
 <h2> Basics </h2>
 
 
@@ -1092,6 +1075,9 @@
 
 <p>We assume a set $Attributes$ of attribute labels and a set $Values$ of possible values of attributes.
 </p>
+</section>
+
+<section id="formulas">
 <h2>Formulas </h2>
 
 <p>The following atomic formulas correspond to the statements of PROV-DM.  We assume that definitions 1-4 of PROV-CONSTRAINTS have been applied in order to expand all optional parameters; thus, we use uniform notation $r(id,a_1,\ldots,a_n)$ instead of the semicolon notation $r(id;a_1,\ldots,a_n)$.
@@ -1123,6 +1109,8 @@
 \end{array}
 $$
 
+</section>
+<section id="models">
 <h2> World Models </h2>
 
 <h3> Things </h3> 
@@ -1280,6 +1268,8 @@
 </p>
 <p><b>TODO: List the components.</b>
 </p>
+</section>
+<section id="semantics">
 <h2> Semantics </h2>
 
 <p>In what follows, let $W$ be a fixed world model with the associated sets and relations discussed in the previous section, and let $I$ be an interpretation of identifiers as objects in $W$.
@@ -1644,8 +1634,8 @@
 
 </section>
 
-<section id="infconstr">
-<h2> Inferences and Constraints </h2>
+<section id="formalizations">
+<h2> Formalizations of Inferences and Constraints </h2>
 
 <div class="inference" number="5" id="communication-generation-use-inference">$\begin{array}[t]{l}
 \forall id,a_2,a_1,attrs.~