--- a/model/ProvenanceModel.html	Wed Sep 07 09:08:02 2011 +0100
+++ b/model/ProvenanceModel.html	Wed Sep 07 09:22:35 2011 +0100
@@ -646,7 +646,7 @@
 states the existence of an activity, denoted by identifier <span class="name">id</span>, with recipe link <span class="name">add-crime-in-london</span>, start time <span class="name">t+1</span>, and end time <span class="name">t+1+epsilon</span>.
 </p>
 
-<p>The mere existence of a process execution assertion entails some event ordering in the world, since the start event preceds the end event.  This expressed by constraint <a href='#start-precedes-end'>start-precedes-end</a>.</p>
+<p>The mere existence of a process execution assertion entails some event ordering in the world, since the start event preceds the end event.  This expressed by constraint <a href="'#start-precedes-end'">start-precedes-end</a>.</p>
 
 <div class='constraint' id='start-precedes-end'><a name="PIL:0001"> From the assertion of a process execution, one can infer that the
 start precedes the end of the represented activity.</a> [<a
@@ -779,25 +779,27 @@
 </p>
 
 
-<p>A reference to a given entity may appear in multiple use assertions that refer
+<p>A reference to a given entity may appear in multiple use expressions that refer
 to a given process execution, but each of those use assertions MUST have a
-distinct role.</p>
+distinct role.
+</p>
 
-
+<!-- Luc, should we write a constraint for this? It's not clear the
+constraint is formulated properly -->
 
 
 
 <div class='constraint' id='use-attributes'><a name="PIL:0005">
-Given a process execution <span class="name">pe</span>, entity <span class="name">e</span>, role <span class="name">r</span>, and optional time <span class="name">t</span>, if
+Given a process execution <span class="name">pe</span>, entity <span class="name">e</span>, role <span class="name">r</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>
  assertion <span class="name">used(pe,e,r)</span> or <span class="name">used(pe,e,r,t)</span> holds, 
-the existence of the value of an attribute of <span class="name">e</span>' is a
+<span class='conditional'>then</span> the existence of an attribute-value pair of <span class="name">e</span> is a
 pre-condition for the activity denoted by <span class="name">pe</span> to terminate.</a>
 [<a href="../ontology/ProvenanceFormalModel.html#PIL:0005">PIL:0005</a>]</div>
 
 
 
-<div class='constraint' id='use-pe-ordering'><a name="PIL:0006">Given a process execution <span class="name">pe</span>, entity <span class="name">e</span>, role <span class="name">r</span>, and optional time <span class="name">t</span>, if
- assertion <span class="name">used(pe,e,r)</span> or <span class="name">used(pe,e,r,t)</span> holds, one can
+<div class='constraint' id='use-pe-ordering'><a name="PIL:0006">Given a process execution <span class="name">pe</span>, entity <span class="name">e</span>, role <span class="name">r</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>
+ assertion <span class="name">used(pe,e,r)</span> or <span class="name">used(pe,e,r,t)</span> holds, <span class='conditional'>then</span> one can
 infer that the use of the thing denoted by <span class="name">e</span> precedes the end
 of <span class="name">pe</span> and follows the beginning of <span class="name">pe</span>. Furthermore, we
 can infer that the generation of the thing denoted by <span class="name">e</span> always precedes