--- a/ontology/ProvenanceFormalModel.html	Thu Oct 13 14:37:41 2011 +0100
+++ b/ontology/ProvenanceFormalModel.html	Thu Oct 13 15:17:25 2011 +0100
@@ -1414,63 +1414,129 @@
 	  </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> 
+    <section id="remaining-constraints"
+    <h4>Remaining constraints not yet adressed by PROV-O</h4>
     <ul>
-<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
+<li><a id="use-pe-ordering">use-pe-ordering</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
 of <b>pe</b> and follows the beginning of <b>pe</b>. Furthermore, we
 can infer that the generation of the thing denoted by <b>e</b> always precedes
-its use."  (<a href="../model/ProvenanceModel.html#PROV:0006">link</a>)
+its use."  (<a href="../model/ProvenanceModel.html#use-pe-ordering">definition</a>)
 </li>
 
-<li> <a id="PROV:0007" href="#PROV:0007">PROV:0007</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b>
+<li> <a id="derivation-attributes">derivation-attributes</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>wasDerivedFrom(e2,e1)</b> holds, if and only if:
  the values of some attributes
 of <b>e2</b> are partly or fully determined by the values of some
-attributes of <b>e1</b>."  (<a href="../model/ProvenanceModel.html#PROV:0007">link</a>)
+attributes of <b>e1</b>."  (<a
+href="../model/ProvenanceModel.html#derivation-attributes">definition</a>)
 </li>
 
-<li><a id="PROV:0008" href="#PROV:0008">PROV:0008</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b>
+<li><a
+id="derivation-use-generation-ordering">derivation-use-generation-ordering</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>wasDerivedFrom(e2,e1)</b> holds, then
 the use
 of characterized thing denoted by <b>e1</b> precedes the generation of
-the characterized thing denoted by <b>e2</b>."  (<a href="../model/ProvenanceModel.html#PROV:0008">link</a>)
+the characterized thing denoted by <b>e2</b>."  (<a
+href="../model/ProvenanceModel.html#derivation-use-generation-ordering">definition</a>)
 </li>
 
-<li><a id="PROV:0009" href="#PROV:0009">PROV:0009</a> "If <b>wasDerivedFrom(e2,e1)</b> holds, then there exists a process execution <b>pe</b>, and roles <b>r1</b>,<b>r2</b>,
+<li><a id="derivation-process-execution">derivation-process-execution</a> "If <b>wasDerivedFrom(e2,e1)</b> holds, then there exists a process execution <b>pe</b>, and roles <b>r1</b>,<b>r2</b>,
 such that:
-  <b>wasGeneratedBy(e2,pe,r2)</b> and <b>used(pe,e1,r1)</b>."  (<a href="../model/ProvenanceModel.html#PROV:0009">link</a>)
+  <b>wasGeneratedBy(e2,pe,r2)</b> and <b>used(pe,e1,r1)</b>."  (<a
+  href="../model/ProvenanceModel.html#derivation-process-execution">definition</a>)
 </li>
 
 
-<li><a id="PROV:0010" href="#PROV:0010">PROV:0010</a> "If <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b> holds, then <b>wasGeneratedBy(e2,pe,r2)</b> and <b>used(pe,e1,r1)</b> also hold." (<a href="../model/ProvenanceModel.html#PROV:0010">link</a>)
-</li>
-
-<li><a id="PROV:0011" href="#PROV:0011">PROV:0011</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, and role <b>r2</b>,
-if <b>wasDerivedFrom(e2,e1)</b> and <b>wasGeneratedBy(e2,pe,r2)</b> hold, then there exists a role <b>r1</b>,
-such that <b>used(pe,e1,r1)</b> also holds." (<a href="../model/ProvenanceModel.html#PROV:0011">link</a>)
-</li>
-
-<li><a id="PROV:0012" href="#PROV:0012">PROV:0012</a> "Given two entities <b>e1</b> and <b>e2</b>, if the assertion <b>isEventuallyDerivedFrom(e2,e1)</b>
- holds, then:
-generation of the characterized thing denoted by <b>e1</b> precedes the generation of
-the characterized thing denoted by <b>e2</b>." (<a href="../model/ProvenanceModel.html#PROV:0012">link</a>)
+<li><a id="derivation-events">derivation-events</a> "If
+<b>wasDerivedFrom(e2,e1,pe,r2,r1)</b> holds, then
+<b>wasGeneratedBy(e2,pe,r2)</b> and <b>used(pe,e1,r1)</b> also hold."
+(<a href="../model/ProvenanceModel.html#derivation-events">definition</a>)
 </li>
 
-<li><a id="PROV:0013" href="#PROV:0013">PROV:0013</a> "An assertion "wasComplementOf(B,A)" holds over the temporal intersection of A and B, <em>only if</em>: 
-   <ol>
-      <li> if a mapping can be established from an attribute X of B to an attribute Y of A, then the values of A and B MUST be consistent with that mapping</li>
-      <li>B has some attribute that A does not have" (<a href="../model/ProvenanceModel.html#PROV:0013">link</a>) </li>
-   </ol>
+<li> <a id='derivation-use'>derivation-use</a>
+<p>Given a process execution expression identified by <span
+class="name">pe</span>, entity expressions identified by <span
+class="name">e1</span> and <span class="name">e2</span>, and qualifier
+<span class="name">q2</span>,
+<span class='conditional'>if</span> <span
+class="name">wasDerivedFrom(e2,e1)</span> and <span
+class="name">wasGeneratedBy(e2,pe,q2)</span> hold, <span
+class='conditional'>then</span> there exists a qualifier <span
+class="name">q1</span>,
+such that <span class="name">used(pe,e1,q1)</span> also holds.
+(<a href="../model/ProvenanceModel.html#derivation-use">definition</a>)
 </li>
 
-<li><a id="PROV:0014" href="#PROV:0014">PROV:0014</a> "Given a process execution <b>pe</b> and entity <b>e</b>, <b>hadPariticipant(pe,e)</b> holds if and only if:
-   <ul> 
-      <li> <b>used(pe,e)</b> holds, or</li>
-      <li> <b>wasControlledBy(pe,e)</b> holds, or</li>
-      <li> <b>wasComplementOf(e1,e)</b> holds for some entities <b>e1</b>, and <b>hadParticipant(pe,e1)</b>  some process execution <b>pe</b>.</li>
-   </ul>
+
+<li>
+<a id='derivation-generation-generation-ordering'>derivation-generation-generation-ordering</a>
+Given two entity expressions denoted by <span class="name">e1</span> and
+<span class="name">e2</span>, <span class='conditional'>if</span> the
+expression <span class="name">wasEventuallyDerivedFrom(e2,e1)</span>
+ holds, <span class='conditional'>then</span> the
+ generation event of the characterized thing  represented by the entity
+ expression denoted by <span class="name">e1</span> precedes the
+ generation event of
+ the characterized thing represented by the entity expression denoted by
+ <span class="name">e2</span>.
+(<a
+href="../model/ProvenanceModel.html#derivation-generation-generation-ordering">definition</a>)
 </li>
+
+<li>
+<a id='derivation-linked-independent'>derivation-linked-independent</a>
+Given two entity expressions denoted by <span class="name">e1</span> and
+<span class="name">e2</span>, <span class='conditional'>if</span> the
+assertion <span class="name">wasDerivedFrom(e2,e1)</span> or <span
+class="name">wasDerivedFrom(e2,e1,pe,q12,q1)</span>
+ holds, <span class='conditional'>then</span> the
+  the expression <span
+  class="name">wasEventuallyDerivedFrom(e2,e1)</span> also holds.
+
+(<a
+href="../model/ProvenanceModel.html#derivation-linked-independent">definition</a>)
+</li>
+
+<li>
+<a
+id='wasComplementOf-necessary-cond'>wasComplementOf-necessary-cond</a>
+An assertion "wasComplementOf(B,A)" holds over the temporal intersection
+of A and B, <span class='conditional'>only if</span>:
+<ol>
+<li> if a mapping can be established from an attribute X of entity
+expression identified by B to an attribute Y of entity expression
+identified by A, then the values of A and B must be consistent with that
+mapping;</li>
+  <li>entity expression identified by B has some attribute that entity
+  expression identified by A does not have.
+  </li></ol>
+   </div>
+(<a
+href="../model/ProvenanceModel.html#wasComplementOf-necessary-cond">definition</a>)
+</li>
+
+<li>
+<a id='participation'>participation</a>
+Given two identifiers <span class="name">pe</span> and  <span
+class="name">e</span>, respectively identifying  a process execution
+expression and an entity expression, the expression <span
+class="name">hadParticipant(pe,e)</span> holds <span
+class='conditional'>if and only if</span>:
+<ul>
+<li> <span class="name">used(pe,e)</span> holds, or</li>
+<li> <span class="name">wasControlledBy(pe,e)</span> holds, or</li>
+<li><span class="name">wasComplementOf(e1,e)</span> holds for some
+entity expression identified by <span class="name">e1</span>, and
+ <span class="name">hadParticipant(pe,e1)</span> holds  some process
+ execution expression  identified by <span class="name">pe</span>.</li>
+ </ul>
+(<a
+href="../model/ProvenanceModel.html#participation">definition</a>)
+
+</li>
+
 </ul>
 
 <div class="note">The above constraints are extracted from the
@@ -1486,6 +1552,7 @@
   If a constraint is dropped, please mark it as "defunct" - don't
   delete it!
   </div>
+</section>
     </section>   	  
     </section>