--- a/ontology/ProvenanceFormalModel.html	Tue Oct 11 11:18:26 2011 +0100
+++ b/ontology/ProvenanceFormalModel.html	Tue Oct 11 14:34:25 2011 -0400
@@ -1379,13 +1379,19 @@
 	  <h4>Provenance constraint on wasGeneratedBy (generation-unicity)</h4>
 	  <p>The PROV-DM describes a constraint on wasGeneratedBy that asserts that given an account, only one PE instance can be associated to an Entity instance by the property wasGeneratedBy.</p>
 	<div class='issue'>"Given an entity expression denoted by e, two process execution expressions denoted by pe1 and pe2, and two qualifiers q1 and q2, if the expressions wasGeneratedBy(e,pe1,q1) and wasGeneratedBy(e,pe2,q2) exist in the scope of a given account, then pe1=pe2 and q1=q2." This is <a href="http://www.w3.org/2011/prov/track/issues/105">ISSUE-105</a></div>
+	</section>
+	<section>
+	  <h4>Provenance constraint on Used (use-attributes)</h4>
+	  <p>A constraint is defined for the Used relation in PROV-DM, that makes it necessary for an attribute-value to be true for an Entity instance linked to a ProcessExecution instance by relation Used.    
+	  </p>
+	  <div class='issue'>"Given a process execution expression identified by pe, an entity expression identified by e, a qualifier q, and optional time t, if assertion used(pe,e,q) or used(pe,e,q,t) holds, then the existence of an attribute-value pair in the entity expression identified by e is a pre-condition for the termination of the activity represented by the process execution expression identified by pe." This is <a href="http://www.w3.org/2011/prov/track/issues/124">ISSUE-124</a></div>
 	</section>	
-<ul>    
-<li><a id="PROV:0005" href="#PROV:0005">PROV:0005</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
- assertion <b>used(pe,e,r)</b> or <b>used(pe,e,r,t)</b> holds, 
-the existence of the value of an attribute of <b>e</b>' is a pre-condition for the activity denoted by <b>pe</b> to terminate."  (<a href="../model/ProvenanceModel.html#PROV:0005">link</a>)
-</li>
-
+    <section>
+	  <h4>Provenance constraint on Used (use-pe-ordering)</h4>
+	  <p>The PROV-DM describes a constraint for Used relation, which makes it necessary for an Entity instance e (linked to a ProcessExecution instance pe by Used relation) to be "used" before pe terminates and also the "generation" of e precedes "use" of e.
+	  </p>
+	  <div class='issue'>"Given a process execution expression identified by pe, an entity expression identified by e, a qualifier q, and optional time t, if assertion used(pe,e,q) or used(pe,e,q,t) holds, then the use of the thing represented by entity expression identified by e precedes the end time contained in the process execution expression identified by pe and follows its beginning. Furthermore, the generation of the thing denoted by entity expression identified by e always precedes its use." This is <a href="http://www.w3.org/2011/prov/track/issues/124">ISSUE-124</a></div>
+	</section> 
 <li><a id="PROV:0006" href="#PROV:0006">PROV:0006</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
  assertion <b>used(pe,e,r)</b> or <b>used(pe,e,r,t)</b> holds, one can
 infer that the use of the thing denoted by <b>e</b> precedes the end