--- a/model/derivation.html	Thu Aug 04 00:00:27 2011 +0100
+++ b/model/derivation.html	Thu Aug 04 08:50:33 2011 +0100
@@ -95,7 +95,7 @@
 
 <p><dfn id="dfn-Derivation">Derivation</dfn> expresses that some characterized thing is transformed from, created from, or affected by another characterized thing.  </p>
 
-<p>PIL offers two different kinds of assertions by which asserters can formulate derivations. The first one is tightly connected to the notion of process execution, whereas the second one is not. The first kind of assertion is particularly suitable for asserters who have an intimate knowledge of process executions, and offers a more precise description of derivation, whereas the second does not put such a requirement on the asserter, and allows a less precise description of derivation to be asserted. From these assertions, further derivations can be inferred by a form of transitive closure. </p>
+<p>PIL offers two different kinds of assertions by which asserters can formulate derivations. The first one is tightly connected to the notion of process execution, whereas the second one is not. The first kind of assertion is particularly suitable for asserters who have an intimate knowledge of process executions, and offers a more precise description of derivation, whereas the second does not put such a requirement on the asserter, and allows a less precise description of derivation to be asserted. From these assertions, further derivations can be inferred by transitive closure. </p>
 
 <section>
 <h4>Process Execution Linked Derivation</h4>
@@ -108,11 +108,11 @@
 <li> refers to an entity <b>e1</b>, denoting the generated characterized thing;
 <li> refers to process execution <b>pe</b>;
 <li> contains a role <b>r2</b>.
-<li> contains a role <b>r1</b>;
+<li> contains a role <b>r1</b>.
 </ul>
 This assertion expresses that the process execution <b>pe</b>, by
 using the thing denoted by <b>e1</b> with role <b>r1</b> derived the
-characterized thing denoted by entity <b>e2</b> and generated it with
+thing denoted by entity <b>e2</b> and generated it with
 role <b>r2</b>.
 </p>
 
@@ -133,20 +133,25 @@
 </p>
 
 
-<p>The compact version has the same meaning as the fully formed process-execution linked derivation, except that the process execution can be inferred to exist.
+<p>The compact version has the same meaning as the fully formed process-execution linked derivation, except that a process execution is known to exist, though it does not need to be asserted.
 This is formalized by the following inference rule, referred to as <em>process execution introduction</em>:<br/>
 <div class='inference'>
 If <b>isDerivedFrom(e2,e1)</b> holds, then there exists a process execution <b>pe</b>, and roles <b>r1</b>,<b>r2</b>,
 such that:
-  <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b>.</p>
+  <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b>.
 </div></p>
 
-<p>From an assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
+<p>If <b>e2</b> is derived from <b>e1</b>, then 
+this means that the thing represented by <b>e1</b> has an influence on the thing represented by <b>e2</b>, which is captured by a dependency between their attribute values, expressed as follows.
+From an assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>isDerivedFrom(e2,e1)</b>, the values of some attributes
 of <b>e2</b> are at least partially determined by the values of some
 attributes of <b>e1</b>.</p>
 
-<p>Given an assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
+<div class='note'>Always?</div>
+
+<p>Furthermore, there is a temporal ordering between the use of <b>e1</b> and the generation of <b>e2</b>.
+Given an assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>isDerivedFrom(e2,e1)</b>, one can infer that the use
 of characterized thing denoted by <b>e1</b> precedes the generation of
 the characterized thing denoted by <b>e2</b>.
@@ -170,6 +175,22 @@
 </pre>
 </p>
 
+<p>A further inference is permitted from the compact version, 
+<div class='inference'>
+If <b>isDerivedFrom(e2,e1)</b> and <b>isGeneratedBy(e2,pe,r2)</b> hold for some <b>e1</b>, <b>e2</b>, <b>pe</b>, <b>r2</b> then there exists a role <b>r1</b>,
+such that <b>uses(pe,e1,r1)</b> also holds.
+</div>
+This inference is justified by the fact that <b>e2</b> is generated by at most one process execution. Hence,  this process executions is also the one that uses <b>e1</b>.
+</p>
+
+
+
+<p>We note that the "symmetric" inference, does not hold.
+From <b>isDerivedFrom(e2,e1)</b> and <b>uses(pe,e1)</b>, one cannot
+derive <b>isGeneratedBy(e2,pe,r2)</b> because <b>e1</b> may be used by
+many process execution, not all of them generating <b>e2</b>.</p>
+
+
 
 </section>