--- a/model/prov-constraints.html	Fri Aug 31 16:45:49 2012 +0100
+++ b/model/prov-constraints.html	Fri Aug 31 16:59:05 2012 +0100
@@ -4676,29 +4676,45 @@
        <li>Stages 2, 3, 4, and 7 have no cycles among the formulas
       involved, so they are weakly acyclic.
        </li>
-       <li>For stage 6, the following graph witnesses weak
+       <li>For stage 6, we check weak acyclicity using the algorithm
+      in       [[DBCONSTRAINTS]], namely:
+       <ul><li> Given a formula <span class="math">φ(x<sub>1</sub>,...,x<sub>n</sub>) ⇒
+      ∃y<sub>1</sub>,...,y<sub>m</sub>. ψ(x<sub>1</sub>,...,x<sub>n</sub>,y<sub>1</sub>,...,y<sub>m</sub>)<span class="math"></li>
+      <li>For every <span class="math">x</span> that occurs in  <span class="math">ψ</span>, and for every
+      occurrence of <span class="math">x</span> in <span class="math">φ</span> in position <span class="math">r.i</span>:
+      <ol><li>For every occurrence of <span class="math">x</span> in position <span class="math">s.j</span>, add
+      an edge from <span class="math">r.i</span> to <span class="math">s.j</span> (if it does
+      not already exist).  </li>
+    <li>In addition, for every existentially quantified variable <span class="math">y</span>
+      and for every occurrence of <span class="math">y</span> in <span class="math">ψ</span> in position
+      <span class="math">t.k</span>, add a special edge from <span class="math">r.i</span> to <span class="math">t.k</span> (if it does
+      not already exist).
+      </li>
+      </ol>
+      </li>
+      </ul>
+      Weak
+      acyclicity means that there is no cycle involving a special
+      edge in the resulting graph.  For the two inferences in stage 6,
+      the following dependency graph witnesses weak
       acyclicity.  The nodes <span class="name">wasGeneratedBy.i</span>,
       <span class="name">wasInformedBy.i</span>, and <span
       class="name">used.i</span> denote the <span class="math">i</span>th arguments
       of the corresponding predicates.  The solid edges are ordinary
-      edges, and the dashed edges are <em>special</em> edges.  These
-      edges are added to the graph following the rules in
-      [[DBCONSTRAINTS]].  Weak
-      acyclicity means that there is no cycle involving a special
-      edge.
-        </li>
+      edges, and the dashed edges are <em>special</em> edges.  
+       </li>
        </ul>
       </p>
        
-       <img src="weak-acyclic-6.svg" text="Graph illustrating weak acyclicity of stage 6"/>
-      </p>
-
+       <img src="weak-acyclic-6.svg" text="Graph illustrating weak
+       acyclicity of stage 6"/>
+       
       <p><b>Termination for instances with attributes.</b>
        We can translate an instance with attributes to an alternative,
        purely relational language by introducing a relation
        <span class="name">attribute(id,a,v)</span> and replacing every statement of the form
-       <span class="name">r(id;a1,...,a_n,[(k_1,v_1),...,(k_m,v_m)])</span> with
-       <span class="name">r(id;a1,...,a_n),attribute(id,k_1,v_1),...,attribute(id,k_m,v_m)</span>,
+       <span class="name">r(id;a1,...,a<sub>n</sub>,[(k<sub>1</sub>,v<sub>1</sub>),...,(k<sub>m</sub>,v<sub>m</sub>)])</span> with
+       <span class="name">r(id;a1,...,a<sub>n</sub>),attribute(id,k<sub>1</sub>,v<sub>1</sub>),...,attribute(id,k<sub>m</sub>,v<sub>m</sub>)</span>,
        and similarly for <span class="name">entity</span>, <span class="name">activity</span> and <span class="name">agent</span>
        attributes.  The inference rules can also be translated so as
        to work on these instances, and a similar argument to