* Reorganized PROV-DM-CONSTRAINTS
authorJames Cheney <jcheney@inf.ed.ac.uk>
Sun, 15 Apr 2012 14:20:36 +0100
changeset 2297 ccf4ba7cd44e
parent 2296 1985dd0ec931
child 2298 edac7c971c3c
* Reorganized PROV-DM-CONSTRAINTS
model/working-copy/wd5-prov-dm-constraints-revised.html
--- a/model/working-copy/wd5-prov-dm-constraints-revised.html	Sat Apr 14 14:55:42 2012 +0100
+++ b/model/working-copy/wd5-prov-dm-constraints-revised.html	Sun Apr 15 14:20:36 2012 +0100
@@ -173,7 +173,9 @@
   constraints</i> that well-structured provenance descriptions should
   follow. These inferences and constraints are useful for readers who
   develop applications that generate provenance or reason over
-  provenance.  </p> </section>
+  provenance.
+</p>
+</section>
 
 <section id="sotd">
 <h4>PROV Family of Specifications</h4>
@@ -212,35 +214,19 @@
 
 
 
-<!--
-<div class="buttonpanel"> 
-<form action="#"><p> 
-<input id="hide-bnf" onclick="set_display_by_class('div','grammar','none'); set_display_by_id('hide-bnf','none');  set_display_by_id('show-bnf','');" type="button" value="Hide Grammar" /> 
-<input id="show-bnf" onclick="set_display_by_class('div','grammar',''); set_display_by_id('hide-bnf','');  set_display_by_id('show-bnf','none');" style="display: none" type="button"
-value="Show Grammar" /> 
-<input id="hide-examples" onclick="set_display_by_class('div','anexample','none'); set_display_by_id('hide-examples','none'); set_display_by_id('show-examples','');" type="button"
-value="Hide Examples" /> 
-<input id="show-examples" onclick="set_display_by_class('div','anexample',''); set_display_by_id('hide-examples',''); set_display_by_id('show-examples','none');" style="display: none"
-type="button" value="Show Examples" /> 
-</p> 
-</form> 
-</div>     
--->
 
     <section id="introduction"> 
       <h2>Introduction<br>
 </h2> 
 
-<p> Provenance is defined as a record that describes the people,
-institutions, entities, and activities, involved in producing,
-influencing, or delivering a piece of data or a thing.  A
-companion specification [[PROV-DM]] defines PROV-DM, a data model for
-provenance, allowing such descriptions to be expressed.  
-</p>
-
-
-
-
+<p> Provenance records describe the people, institutions,
+  entities, and activities, involved in producing, influencing, or
+  delivering a piece of data or a thing.  This document is part of a
+  specification [[PROV-DM]] that defines a data model for
+  provenance on the Web.  </p>
+
+<div class="note"> Revise list to match SOTD.  Seems redundant.
+  </div>
 <p>This specification is one of several specifications, referred to as the PROV family of specifications, defining the various aspects
 that are necessary to achieve the vision of  inter-operable exchange of provenance:</p>
 <ul>
@@ -258,7 +244,12 @@
 <li>PROV-SEM: semantics of the PROV-DM data model [[PROV-SEM]];</li>
 </ul>
 
-
+<div class="note">
+  Revise this section to match the revised document structure.
+  </div>
+
+
+  <!--
 <p>PROV-DM is essentially defined without any constraints 
 [[PROV-DM]]. This document introduces a further set of concepts useful
 for understanding the rationale for the data model, defines inferences
@@ -266,8 +257,7 @@
 
 
 <p>In [[PROV-DM]], a data model for provenance has been defined
-without introducing any constraint that this data model has to
-satisfy.   First we introduce and refine various PROV-DM concepts such as attributes, event, entity, entity, interval, accounts. Using these notions, we explore the constraints
+without introducing any constraints on provenance.  First we introduce and refine various PROV-DM concepts such as attributes, event, entity, entity, interval, accounts. Using these notions, we explore the constraints
 that the PROV-DM data model has to satisfy. </p> 
 
 <p>Several types of constraints are specified.</p>
@@ -279,37 +269,9 @@
 <li>Collection constraints are the constraints that hold for collections (<a href="#collection-constraints">Section 8</a>)</li>
 </ul>
 
-  
-
-
-<!--
-    <section id="structure-of-this-document"> 
-<h3>Structure of this Document</h3>
-
-<div class='note'>TODO</div>
-
-<p>In <a href="#prov-dm-refinement">section 2</a>, further concepts
-useful for explaining PROV-DM are introduced.</p>
-
-<p><a href="#data-model-constraints">Section 3</a></p>
-
-
-<p><a href="#definitional-constraints">Section 4</a></p>
-
-<p><a href="#account-constraints">Section 5</a>
-</p>
-
-<p><a href="#interpretation">Section 6</a></p>
-<p><a href="#structural-constraints">Section 7</a></p>
-<p><a href="#collection-constraints">Section 8</a></p>
-<p><a href="#refining-provenance-descriptions">Section 9</a> successively review refined provenance descriptions, and examine their meaning, in light of the constraints introduced in previous sections. </p>
-
-
-
-    </section> 
-
-
 -->
+
+
     <section id="conventions"> 
 <h3>Conventions</h3>
 
@@ -321,14 +283,1213 @@
       [[!RFC2119]].</p>
     </section> 
 
+
+<section id="purpose">
+
+<h3>Purpose of this document</h3>
+
+<p>
+PROV-DM specifies a data model for provenance (realizable using
+PROV-N, PROV-RDF, or PROV-XML).  However, nothing in PROV-DM part 1
+forces such provenance data to be meaningful, that is, to correspond
+to a consistent history of objects and interactions.  Furthermore,
+nothing in PROV-DM part 1 enables applications to perform standard
+inferences over provenance information.  
+</p>
+
+<p> This document specifies <em>inferences</em> over PROV-DM data that
+applications MAY employ, including definitions of some provenance
+expressions in terms of others, and also defines a class of <em>valid</em>
+PROV-DM data by specifying <em>constraints</em> that valid PROV-DM data must
+satisfy. Applications SHOULD produce valid provenance and
+MAY reject provenance that is not valid in order to increase
+the usefulness of provenance.</p>
+
+<p> This specification lists inferences and definitions together in one
+section (<a href="#inferences" class="sectionRef"></a>), and then
+considers two kinds of validity constraints (<a href="#constraints"
+class="sectionRef"></a>): <em>structural constraints</em> that
+prescribe properties of PROV-DM instances that can be checked directly
+by inspecting the syntax, and <em>event ordering</em> constraints that
+require that the records in a PROV-DM instance are consistent with a
+sensible ordering of events relating the activities, entities and
+actors involved.  In separate sections we consider additional
+constraints specific to collections and accounts (<a
+ href="#collection-constraints" class="sectionRef"></a> and <a
+ href="#account-constraints" class="sectionRef"></a>).  </p>
+
+<p>
+The specification also describes how the inferences, definitions, and constraints should be used (<a href="#compliance" class="sectionRef"></a>).  Briefly, a PROV-DM compliant application is allowed (but not required) to treat two PROV-DM instances as the same if they are equal after applying the inference rules and possibly reordering expressions, and we can define a canonical form for PROV-DM instances obtained by applying all possible inference rules.  In addition, a validating PROV-DM application is required to check that the constraints are satisfied in (the canonical form of) provenance data generated or consumed by the application.
+</p>
+
+<p>
+Finally, the specification includes a section (<a
+ href="#rationale" class="sectionRef"></a>) describing the rationale
+for the inferences and constraints in greater detail, particularly
+background on events, attributes, the the role of inference, and
+accounts. A formal mathematical model that further justifies the
+constraints and inferences is found in [[PROV-SEM]].
+</p>
+
+</section>
+<section id="audience">
+<h3> Audience </h3>
+
+<p> The audience for PROV-DM-CONSTRAINTS is the same as for PROV-DM: developers
+and users who wish to create, process, share or integrate provenance
+records on the (Semantic) Web.  Not all PROV-compliant applications
+need to check validity when processing provenance, but many
+applications could benefit from the inference rules specified here.
+Conversely, applications that create or transform provenance should
+try to produce valid provenance, to make it more useful to other
+applications.
+</p>
+
+<p>This document assumes familiarity with [[PROV-DM]].
+</p>
+</section>
+
 </section> 
 
 
-<section id='prov-dm-refinement'>
-<h2>Data Model Refinement</h2>
-
+
+
+<section id="inferences">
+<h2>Inferences and Definitions</h2>
+
+<p>
+In this section we describe <a title="inference">inferences</a> and <a title="definition">definitions</a> that MAY be used on
+  provenance data.  
+An  <dfn id="inference">inference</dfn> is a rule that can be applied
+  to PROV-DM to add new provenance expressions.  A <dfn
+  id="definition">definition</dfn> is a rule that states that a
+  provenance expression is equivalent to some other expressions; thus,
+  defined provenance expressions can be replaced by their definitions.
+</p>
+
+<p>Applications that process provenance MAY use these definitions or
+inferences.  Moreover, they SHOULD apply all applicable inferences
+before determining whether an instance of PROV-DM is <a
+ title="valid">valid</a>.  In particular, applications that generalte
+provenance SHOULD check that the generated provenance is valid even if
+some of these inferences or definitions are applied to it by another
+application.
+</p>
+
+<section>
+  <h3>Component 1: Entities and Activities</h3>
+  
+
+<p>Communication between activities is <a title="definition">defined</a> in terms
+as the existence of an underlying entity generated by one activity and used by the
+other.</p>
+
+<div class='definition' id='wasInformedBy-communication'>Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>, 
+<span class="name">wasInformedBy(a2,a1)</span>
+holds <span class='conditional'>if and only if</span>
+ there is an entity  with some identifier <span class="name">e</span> and some sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
+such that <span class="name">wasGeneratedBy(-,e,a1,-,attrs1)</span> and <span class="name">used(-,a2,e,-,attrs2)</span> hold.
+</div>
+
+
+<p>Start of <span class="name">a2</span> by activity <span
+class="name">a1</span> is <a title="definition">defined</a> as follows.</p>
+
+<div class='definition' id='wasStartedBy'>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>, 
+ <span class="name">wasStartedBy(a2,a1)</span>
+holds <span class='conditional'>if and only if</span>
+ there exist an entity with some identifier <span class="name">e</span> 
+and some attributes  <span class="name">gAttr</span> and  <span class="name">sAttr</span>,
+such that
+ <span class="name">wasGeneratedBy(-,e,a1,-,gAttr)</span> 
+ and <span class="name">wasStartedBy(-,a2,e,-,sAttr)</span> hold.
+</div>
+
+
+
+
+</section>
+
+<section >
+<h3>Component 2: Agents</h3>
+
+Attribution identifies an agent as responsible for an entity.  An
+agent can only be responsible for an entity if it was associated with
+an activity that generated the entity.  If the activity, generation
+and association events are not explicit in the description, they can
+be inferred.
+<div class='inference' id='attribution-implication'>
+<span class='conditional'>If</span>
+<span class="name">wasAttributedTo(e,ag)</span> holds for some identifiers
+<span class="name">e</span> and <span class="name">ag</span>,  
+<span class='conditional'>then</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
+<pre>
+activity(a, t1, t2, attr1)
+wasGeneratedBy(-,e, a, -)
+wasAssociatedWith(-,a, ag, -, attr2)
+</pre>
+for some sets of attribute-value pairs <span class="name">attr1</span>
+  and  <span class="name">attr2</span>, and times <span class="name">t1</span> and <span class="name">t2</span>.
+</div>
+</section>
+
+ <section> 
+<h3>Component 3: Derivations</h3>
+<section>
+<h4>Derivation</h4>
+  <p>A further inference is permitted from derivations with an explicit activity and no usage: </p>
+<div class='inference' id='derivation-use'>
+<p>Given an activity <span class="name">a</span>, entities  denoted by <span class="name">e1</span> and <span class="name">e2</span>, and  sets of attribute-value
+pairs <span class="name">dAttrs</span>, <span class="name">gAttrs</span>,
+<span class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1, a, dAttrs)</span> and <span class="name">wasGeneratedBy(e2,a,-,gAttrs)</span> hold, <span
+class='conditional'>then</span> <span class="name">used(a,e1,-,uAttrs)</span> also holds
+for some set of attribute-value pairs <span class="name">uAttrs</span>.
+</div>
+<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity in a given account
+(see <a href="#generation-uniqueness">generation-uniqueness</a>). Hence,  this activity is also the one referred to by the usage of <span class="name">e1</span>. 
+</p>
+
+
+<p>We note that the converse inference, does not hold.
+From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(a,e1,-)</span>, one cannot
+derive <span class="name">wasGeneratedBy(e2,a,-)</span> because identifier <span class="name">e1</span> may occur in usages performed by many activities, which may have not generated the entity denoted by <span class="name">e2</span>.</p>
+
+
+</section>
+<section>
+<h4>Revision</h4>
+
+<p>A revision needs to satisfy the following constraint, linking the two entities by a derivation, and stating them to be a specialization  of a third entity.</p>
+
+<div class='inference' id='wasRevision'>
+Given two identifiers <span class="name">e1</span> and <span class="name">e2</span> identifying two entities, and an identifier <span class="name">ag</span> identifying an agent,
+<span class='conditional'>if</span> <span class="name">wasRevisionOf(e2,e1,ag)</span> holds, <span class='conditional'>then</span> 
+there exists an entity with some identifier <span class="name">e</span> and some attribute-values <span class="name">eAttrs</span>, <span class="name">dAttrs</span>, such that the following 
+hold:
+<pre>
+wasDerivedFrom(e2,e1,dAttrs)
+entity(e,eAttrs)
+specializationOf(e2,e)
+specializationOf(e1,e)
+wasAttributedTo(e2,ag)
+</pre>
+</div>
+
+<p>
+<div id="optional-attributes5">In a revision of the form <span class="name">wasRevisionOf(e2,e1,-,attr)</span>, the absence of an agent means: either no agent exists, or an agent exists but it is not identified.</div>
+
+
+<p><span class="name">wasRevisionOf</span> is a strict sub-relation
+ of <span class="name">wasDerivedFrom</span> since two entities <span class="name">e2</span> and <span class="name">e1</span>
+ may satisfy <span class="name">wasDerivedFrom(e2,e1)</span> without being a variant of
+ each other.
+</p>
+</section>
+
+<section>
+<h4>Quotation</h4>
+<div class="note">
+  Motivation for quotation inference
+  </div>
+<div class='inference' id='quotation-implication'>
+<span class='conditional'>If</span>
+<span class="name">wasQuotedFrom(e2,e1,ag2,ag1,attrs)</span> holds for some identifiers
+<span class="name">e2</span>, <span class="name">e1</span>, <span class="name">ag2</span>, <span class="name">ag1</span>, 
+<span class='conditional'>then</span> the following hold:
+<pre>
+wasDerivedFrom(e2,e1)
+wasAttributedTo(e2,ag2)
+wasAttributedTo(e1,ag1)
+</pre>
+</div>
+
+<p>
+
+<div id="optional-attributes6">In a quotation of the form <span class="name">wasQuotedFrom(e2,e1,-,-,attrs)</span>, the absence of an agent means: either no agent exists, or an agent exists but it is not identified.</div>
+
+</section>
+
+
+<section id="term-traceability">
+<h3>Traceability</h3>
+
+<p>Traceability allows an entity to be transitively linked to another entity it is derived from, to an agent it is attributed to, or another agent having some responsibility, or a trigger of an activity that generated it.</p>
+
+<p>Traceability can be inferred from existing descriptions, or can be asserted stating that a dependency path exists without its individual steps being expressed. This is captured 
+by the following inference and constraint, respectively.
+
+<div class='inference' id='traceability-inference'>
+Given two identifiers <span class="name">e2</span> and  <span class="name">e1</span> for entities, 
+the following statements hold:
+
+<ol> 
+<li><span class='conditional'>If</span>  <span class="name">wasDerivedFrom(e2,e1,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span
+class="name">u1</span>, <span class='conditional'>then</span>  <span class="name">tracedTo(e2,e1)</span> also holds.</li>
+<li><span class='conditional'>If</span>  <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>then</span>  <span class="name">tracedTo(e2,e1)</span> also
+holds.</li>
+<li><span class='conditional'>If</span>  <span class="name">wasAttributedTo(e2,ag1,aAttr)</span> holds, <span class='conditional'>then</span>  <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
+<li><span class='conditional'>If</span>  <span class="name">wasAttributedTo(e2,ag2,aAttr)</span>, <span class="name">wasGeneratedBy(e2,a,gAttr)</span>,  and <span
+class="name">actedOnBehalfOf(ag2,ag1,a,rAttr)</span> hold, for some  <span class="name">a</span>, <span class="name">ag2</span>, <span class="name">ag1</span>, <span class="name">aAttr</span>,  <span class="name">gAttr</span>, and <span class="name">rAttr</span>, <span
+class='conditional'>then</span>  <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
+
+<li><span class='conditional'>If</span> <span
+class="name">wasGeneratedBy(e2,a,gAttr)</span> and <span
+class="name">wasStartedBy(a,e1,sAttr)</span> hold, for some  <span
+class="name">a</span>, <span class="name">gAttr</span> , <span
+class="name">sAttr</span>  then <span
+class="name">tracedTo(e2,e1)</span> holds.</li>
+<li><span class='conditional'>If</span>  <span class="name">tracedTo(e2,e)</span> and  <span class="name">tracedTo(e,e1)</span> hold for some  <span class="name">e</span>, <span
+class='conditional'>then</span>  <span class="name">tracedTo(e2,e1)</span> also holds.</li>
+</ol>
+</div>
+
+<p>We note that the inference rule <a
+href="#traceability-inference">traceability-inference</a> does not
+allow us to infer anything about the attributes of the related
+entities or events.
+</p>
+</section>
+
+
+</section>
+
+
+ <section> 
+<h3>Component 4: Alternate Entities</h3>
+<div class="note">TODO: There are currently no widely agreed inferences on
+  alternate or specialization.
+  </div>
+
+  The relation alternateOf is an equivalence relation: reflexive,
+  transitive and symmetric.
+  <div class='inference' id="alternate-reflexive">
+    For any entity e, we have alternateOf(e,e).
+    </div>
+
+
+       <div class='inference' id="alternate-transitive">
+    For any entities e1, e2, e3, if alternateOf(e1,e2) and
+    alternateOf(e2,e3) then alternateOf(e1,e3).
+    </div>
+   <div class='inference' id="alternate-symmetric">
+    For any entity e1, e2, if  alternateOf(e1,e2) then alternateOf(e2,e1).
+    </div>
+
+Similarly, specialization is a partial order: it is reflexive and
+    transitive.
+    <div class='inference' id="specialization-reflexive">
+    For any entity e, we have specializationOf(e,e).
+    </div>
+
+
+       <div class='inference' id="specialization-transitive">
+    For any entities e1, e2, e3, if specializationOf(e1,e2) and
+	 specializationOf(e2,e3) then specializationOf(e1,e3).
+    </div> 
+
+
+
+    If one entity specializes another, then they are also alternates:
+       <div class='inference' id="specialization-alternate">
+    For any entities e1, e2 if specializationOf(e1,e2) then alternateOf(e1,e2).
+    </div> 
+
+
+   <div class="note">TODO: Possible inferences about attributes,
+  generation, invalidation?
+  </div>
+    
+</section>
+
+</section>
+
+
+<div class="note">
+  TODO Merge material from <a href="#definitional-constraints" class="sectionRef"></a>.
+  </div>
+  
+</section> <!-- inferences -->
+
+<section id="constraints">
+<h2>Validity Constraints</h2>
+
+
+<p>
+This section defines a collection of constraints on instances of
+  PROV-DM.  An instance of PROV-DM is <dfn id="dfn-valid">valid</dfn>
+  if, after applying all possible inference and definition rules from
+  <a href="#inferences">Section 2</a>, the resulting instance
+  satisfies all of the constraints specified in this section.
+  Applications that process PROV-DM data SHOULD check that the data
+  they generate is <a title="valid">valid</a> and MAY reject input
+  provenance data that is not <a title="valid">valid</a>.
+  </p>
+
+  <p> There are two kinds of constraints:
+  <ul><li><em>uniqueness constraints</em> that say that a PROV-DM
+  instance can contain at most one expression or that multiple
+  expressions about the same objects need to have the same values (for
+  example, if we describe the same generation event twice, then the
+  two expressions should have the same times);
+    </li>
+    <li> and <em>event ordering constraints</em> that say that it
+  should be possible to arrange the 
+  events (generation, usage, invalidation, start, end) described in a
+  PROV-DM instance into a partial order that corresponds to a sensible
+  "history" (for example, an entity should not be generated after it
+  is used).
+    </li>
+    </ul>
+    
+<section id="structural-constraints">
+<h3>Uniqueness Constraints</h3>
+<div class="note">
+  TODO Merge material from <a href="#structural-constraints"
+  class="sectionRef"></a> and <a href="#definitional-constraints" class="sectionRef"></a>.
+  </div>
+
+  <p> We assume that the various identified objects of PROV-DM have
+  unique expressions describing them within a PROV-DM instance.
+  </p>
+  <div class='constraint' id='entity-unique'>
+<p>Given an entity identifier <span class="name">e</span>, there is at most one description 
+<span class="name">entity(e,attrs)</span>, where <span
+  class="name">attrs</span> is some set of attribute-values.</p>
+    </div>
+  <div class='constraint' id='activity-unique'>
+<p>Given an activity identifier <span class="name">a</span>, there is at most one description 
+<span class="name">activity(a,t1,t2,attrs)</span>, where <span
+  class="name">attrs</span> is some set of attribute-values.</p>
+    </div>
+    <div class="note">TODO: Same goes for all other objects:
+  agent, note, generation, usage, invalidation, start, end,
+  communication, start by, attribution, association, responsibility, 
+  derivation, revision, quotation.  We should find a
+  way of saying this once concisely.
+      </div>
+  
+<p>We assume that an entity has exactly one generation and
+invalidation event (either or both may, however, be left implicit).
+So, PROV-DM allows for two distinct <a>generations</a>  <span class="name">g1</span> and <span class="name">g2</span> referencing the same entity provided they occur
+<em>simultaneously</em>. 
+This implies that the two generation events are actually the same and
+caused by the same <em>activity</em>, though  provenance may contain
+several  descriptions for the same world activity. 
+</p>
+
+
+<div class='constraint' id='generation-uniqueness'>Given an entity denoted by <span class="name">e</span>, two activities denoted by <span class="name">a1</span> and <span
+class="name">a2</span>, two time instants  <span class="name">t1</span> and <span
+class="name">t2</span>, and two sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
+<span class='conditional'>if</span> <span class="name">wasGeneratedBy(id1, e, a1, t1, attrs1)</span> and <span class="name">wasGeneratedBy(id2, e, a2, t2, attrs2)</span> exist,
+<span class='conditional'>then</span> <span class="name">id1</span>=<span class="name">id2</span>, <span class="name">a1</span>=<span class="name">a2</span>, <span class="name">t1</span>=<span class="name">t2</span>  and <span class="name">attrs1</span>=<span class="name">attrs2</span>.
+</div> 
+
+<p>A generation can be used to indicate a generation time without having to specify the involved activity.  A generation time is unique, as specified by the following constraint.<p> 
+
+<div class='constraint' id='unique-generation-time'>
+Given an entity denoted by <span class="name">e</span> and 
+two time instants  <span class="name">t1</span> and <span
+class="name">t2</span>,
+<span class='conditional'>if</span> <span class="name">wasGeneratedBy(e, -, t1)</span> and <span class="name">wasGeneratedBy(e, -, t2)</span> hold, then <span class="name">t1</span>=<span class="name">t2</span>.
+</div> 
+
+<p>An <a>activity start event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity starts. It allows for an optional time attribute.  <span id="optional-attributes2">Activities also allow for an optional start time attribute.  If both are specified, they MUST be the same, as expressed by the following constraint.</span>
+</p>
+
+<div class='constraint' id='unique-startTime'>
+Given an activity <span class="name">activity(a,t1,t2,attrs1)</span> and its start <span class="name">wasStartedBy(id,a,e,t,attrs2)</span>,  then <span class="name">t</span>=<span class="name">t1</span>.
+</div> 
+
+<p>An <a>activity end event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity ends. It allows for an optional time attribute.  <span id="optional-attributes3">Activities also allow for an optional end time attribute.  If both are specified, they MUST be the same, as expressed by the following constraint.</span>
+</p>
+
+<div class='constraint' id='unique-endTime'>
+Given an activity <span class="name">activity(a,t1,t2,attrs1)</span> and its end <span class="name">wasEndedBy(id,a,e,t,attrs2)</span>,  then <span class="name">t</span>=<span class="name">t2</span>.
+</div> 
+
+
+<!--
+<div class='note'>TODO: Move this back to the place where it is first referenced.</div>
+<p>A further inference is permitted from derivations with an explicit activity and no usage: </p>
+<div class='inference' id='derivation-use'>
+<p>Given an activity <span class="name">a</span>, entities  denoted by <span class="name">e1</span> and <span class="name">e2</span>, and  sets of attribute-value
+pairs <span class="name">dAttrs</span>, <span class="name">gAttrs</span>,
+<span class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1, a, dAttrs)</span> and <span class="name">wasGeneratedBy(e2,a,-,gAttrs)</span> hold, <span
+class='conditional'>then</span> <span class="name">used(a,e1,-,uAttrs)</span> also holds
+for some set of attribute-value pairs <span class="name">uAttrs</span>.
+</div>
+<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity
+(see <a href="#generation-uniqueness">generation-uniqueness</a>). Hence,  this activity is also the one referred to by the usage of <span class="name">e1</span>. 
+</p>
+
+
+<p>We note that the converse inference, does not hold.
+From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(a,e1,-)</span>, one cannot
+derive <span class="name">wasGeneratedBy(e2,a,-)</span> because identifier <span class="name">e1</span> may occur in usages performed by many activities, which may have not generated the entity denoted by <span class="name">e2</span>.</p>
+-->
+
+
+</section> <!-- uniqueness-constraints--> 
+
+<section id="event-ordering-constraints">
+<h3>Event Ordering Constraints</h3>
+
+<p>Section <a href="#section-time-event">section-time-event</a>
+introduces a notion of <a title="instantaneous event">instantaneous event</a>
+marking changes in the world, in its activities and entities.  PROV-DM
+identifies five kinds of <a title="instantaneous event">instantaneous events</a>, namely <a>entity generation
+event</a>, <a>entity usage event</a>, <a>entity invalidation event</a>, <a>activity start event</a>
+and <a>activity end event</a>.  PROV-DM adopts Lamport's clock
+assumptions [[CLOCK]] in the form of a reflexive, transitive partial order <a>follows</a>
+(and its inverse <a>precedes</a>) between <a title="instantaneous event">instantaneous events</a>.  Furthermore,
+PROV-DM assumes the existence of a mapping from <a title="instantaneous event">instantaneous events</a> to time clocks,
+though the actual mapping is not in scope of this specification.</p>
+
+<p>Given that provenance consists of a description of past entities
+and activities, to be valid provenance descriptions MUST
+satisfy <em>ordering constraints</em> between instantaneous events, which we introduce in
+this section.  For instance, an entity can only be used after it was
+generated; hence, we say that an entity's <a title="entity generation
+event">generation event</a> precedes any of this
+entity's <a title="entity usage event">usage event</a>.  Should this
+ordering constraint be proven invalid, the associated generation and
+usage could not be credible.  The rest of this section defines
+the <dfn>temporal interpretation</dfn> of provenance descriptions as a
+set of instantaneous event ordering constraints. </p>
+
+
+<p>PROV-DM also allows for time observations to be inserted in
+specific provenance descriptions, for each of the five kinds
+of <a title="instantaneous event">instantaneous events</a> introduced in this specification.  The
+presence of a time observation for a given <a>instantaneous event</a> fixes the
+mapping of this <a>instantaneous event</a> to the timeline. The presence of time
+information in a provenance description instantiates the ordering constraint with
+that time information. It is expected that such instantiated
+constraints can help corroborate provenance information. We anticipate
+that verification algorithms could be developed, though this
+verification is outside the scope of this specification.
+</p>
+
+<p>The following figure summarizes the ordering constraints in a
+graphical manner. For each subfigure, an event time line points to the
+right. Activities are represented by rectangles, whereas entities are
+represented by circles. Usage, generation and derivation are
+represented by the corresponding edges between entities and
+activities.  The five kinds of <a title="instantaneous event">instantaneous events</a> are represented by vertical
+dotted lines (adjacent to the vertical sides of an activity's
+rectangle, or intersecting usage and generation edges).  The ordering
+constraints are represented by triangles: an occurrence of a triangle between two <a title="instantaneous event">instantaneous event</a> vertical dotted lines represents that the event denoted by the left
+line precedes the event denoted by the right line.</p>
+
+<div style="text-align: center;">
+<figure>
+<figcaption id="constraint-summary">Summary of <a title="instantaneous event">instantaneous event</a> ordering constraints</figcaption>
+<img src="images/constraints.png" alt="constraints between events" />
+</figure>
+</div>
+
+
+
+<p>The existence of an activity implies that the <a>activity start event</a> always <a>precedes</a> the corresponding <a>activity end
+event</a>.  This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (a) and  expressed by constraint <a href="#start-precedes-end">start-precedes-end</a>.</p> 
+<div class='constraint' id='start-precedes-end'> The following ordering constraint holds for any activity: the
+<a title="activity start event">start event</a> <a>precedes</a> the <a title="activity end event">end event</a>.</div> 
+
+<p> A usage and a generation for a given entity implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation
+event">generation event</a> had to precede the <a title="entity usage event">usage event</a>. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (b) and  expressed by constraint <a href="#generation-precedes-usage">generation-precedes-usage</a>.</p>
+
+<div class='constraint' id='generation-precedes-usage'>For any entity, the following ordering constraint holds: the <a title="entity generation event">generation</a> of an entity always
+<a>precedes</a> any of its <a title="entity usage event">usages</a>.
+</div>
+
+<div class="note">
+ISSUE-345: does not clearly delineate where the discussion for one constraint starts and where the next ends.
+ </div>
+
+<p>Invalidation is defined at the event at which an entity ceases to exist as such.   All usages of an entity precede its invalidation, which is captured by constraint <a href="#usage-precedes-invalidation">usage-precedes-invalidation</a> (without any explicit graphical representation).</p> 
+
+<div class='constraint' id='usage-precedes-invalidation'>For any entity, the following ordering constraint holds: any <a title="entity usage event">usage</a> of an entity always
+<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
+</div>
+
+<p>Similarly, generation of an entity precedes its invalidation. (This
+follows from other constraints if the entity is used, but we state it
+explicitly to cover the case of an entity that is generated and
+invalidated without being used.)</p>
+
+<div class='constraint' id='generation-precedes-invalidation'>For
+  any entity, the following ordering constraint holds: the <a
+  title="entity generation event">generation</a> of an entity always
+<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
+</div>
+
+<p>A usage implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity usage event">usage event</a> had to occur during the associated activity. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (c) and  expressed by constraint <a href="#usage-within-activity">usage-within-activity</a>.</p>
+
+<div class='constraint' id='usage-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
+of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>
+  <span class="name">used(a,e,attrs)</span> or <span class="name">used(a,e,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint holds:
+ the <a title="entity usage event">usage</a> of the entity  denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a> of
+activity denoted by <span class="name">a</span> and <a>follows</a> its <a title="activity start event">start</a>. 
+</div>
+
+
+
+<p>A generation implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation event">generation event</a> had to occur during the associated activity. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (d) and  expressed by constraint <a href="#generation-within-activity">generation-within-activity</a>.</p> 
+
+<div class='constraint' id='generation-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
+of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>  <span class="name">wasGeneratedBy(e,a,attrs)</span> or <span
+class="name">wasGeneratedBy(e,a,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint also holds: the <a title="entity generation
+event">generation</a> of the entity denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a>
+of activity <span class="name">a</span> and <a>follows</a> the <a title="activity start event">start</a> of <span class="name">a</span>. 
+</div> 
+
+
+
+
+<p>If there is a derivation between <span class="name">e2</span> and <span class="name">e1</span>, then 
+this means that the entity <span class="name">e1</span> had some form of influence on the entity <span class="name">e2</span>; for this to be possible, some event ordering must be satisfied.
+First, we consider derivations, where the activity and usage are known. In that case, the <a title="entity usage event">usage</a> of <span class="name">e1</span> has to precede the <a title="entity generation
+event">generation</a> of <span class="name">e2</span>.
+This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (e) and  expressed by constraint <a
+href="#derivation-usage-generation-ordering">derivation-usage-generation-ordering</a>.</p>
+
+
+<div class='constraint' id='derivation-usage-generation-ordering'>Given an activity with identifier <span class="name">a</span>,  entities with identifier <span
+class="name">e1</span> and <span class="name">e2</span>, a generation identified by <span class="name">g2</span>, and a usage identified by <span class="name">u1</span>, <span
+class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1,attrs)</span>
+ holds, <span class='conditional'>then</span>
+the following ordering constraint holds:
+the <a title="entity usage event">usage</a>
+of entity denoted by <span class="name">e1</span> <a>precedes</a> the <a title="entity generation event">generation</a> of
+the entity denoted by <span class="name">e2</span>.
+</div>
+
+<p>When the usage is unknown, a similar constraint exists, except that the constraint refers to its
+generation event, as
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (f) and  expressed by constraint <a
+href="#derivation-generation-generation-ordering">derivation-generation-generation-ordering</a>.</p>
+
+<div class='constraint' id='derivation-generation-generation-ordering'>
+Given two entities denoted by <span class="name">e1</span> and <span class="name">e2</span>, <span class='conditional'>if</span> <span
+class="name">wasDerivedFrom(e2,e1, attrs)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraint holds:
+the <a title="entity generation event">generation event</a> of the entity denoted by <span class="name">e1</span> <a>precedes</a> the <a title="entity generation event">generation event</a>
+of
+the entity  denoted by <span class="name">e2</span>.
+  </div>
+
+<p>Note that event ordering is between generations of <span class="name">e1</span>
+and <span class="name">e2</span>, as opposed to derivation where usage is known,
+which implies ordering ordering between the usage of <span class="name">e1</span> and
+generation of <span class="name">e2</span>.  </p>
+
+<p>Communication between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
+title="instantaneous event">events</a>, since some entity must have been generated by the former and used by the latter, which implies that the start event of  <span class="name">a1</span>
+cannot follow the end event of  <span class="name">a2</span>. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (g) and  expressed by constraint <a href="#wasInformedBy-ordering">wasInformedBy-ordering</a>.</p>
+
+<div class='constraint' id='wasInformedBy-ordering'>
+Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
+class="name">wasInformedBy(a2,a1)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraint holds:
+the <a title="activity start event">start event</a> of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity end event">end event</a> of
+the activity denoted by <span class="name">a2</span>.
+</div>
+
+<p>Start of <span class="name">a2</span> by activity <span class="name">a1</span> also implies ordering of <a
+title="instantaneous event">events</a>, since  <span class="name">a1</span> must have been active before   <span class="name">a2</span> started. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (h) and  expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
+
+
+<div class='constraint' id='wasStartedBy-ordering'>
+Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
+class="name">wasStartedBy(a2,a1)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraint holds: the
+<a title="activity start event">start</a> event of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity start event">start event</a> of
+the activity denoted by <span class="name">a2</span>.
+</div>
+
+
+<p>Further constraints appear in Figure <a href="#constraint-summary2">constraint-summary2</a> and are discussed below.</p>
+
+<div style="text-align: center;">
+<figure>
+<figcaption id="constraint-summary2">Summary of <a title="instantaneous event">instantaneous event</a> ordering constraints (continued)</figcaption>
+<img src="../images/constraints2.png" alt="further constraints between events" />
+</figure>
+</div>
+
+
+<p>The agent that started an activity must exist before the activity starts.
+This is
+illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (a) and  expressed by constraint <a href="#wasStartedByAgent-ordering">wasStartedByAgent-ordering</a>.</p>
+
+
+<div class='constraint' id='wasStartedByAgent-ordering'>
+Given an activity denoted by <span class="name">a</span> and an entity denoted by   <span class="name">e</span>, <span class='conditional'>if</span>  <span
+class="name">wasStartedBy(a,e)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+<a title="activity start event">start</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
+<a>precedes</a> the invalidation event of 
+the same entity.
+</div>
+
+<p> Similarly, if an agent is associated with an activity then the
+agent must exist before the activity starts and persist until the
+activity ends, as illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (b).</p>
+
+
+<div class='constraint' id='wasEndedByAgent-ordering'>
+Given an activity denoted by <span class="name">a</span> and an entity denoted by   <span class="name">e</span>, <span class='conditional'>if</span>  <span
+class="name">wasEndedBy(a,e)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+<a title="activity end event">end</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
+<a>precedes</a> the invalidation event of 
+the same entity.
+</div>
+
+
+<p>An activity that was associated with an agent must have some overlap with the agent. The agent may be generated, or may only become associated with the activity, after the activity start: so, the agent is required to exist before the activity end. Likewise, the agent may be destructed, or may terminate its association with the activity, before the activity end: hence, the agent invalidation is required to happen after the activity start.
+This is
+illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (c) and  expressed by constraint <a href="#wasAssociatedWith-ordering">wasAssociatedWith-ordering</a>.</p>
+
+
+<div class='constraint' id='wasAssociatedWith-ordering'>
+Given an activity denoted by <span class="name">a</span> and an agent denoted by   <span class="name">ag</span>, <span class='conditional'>if</span> <span
+class="name">wasAssociatedWith(a,ag)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+<a title="activity start event">start</a> event of the activity  denoted by <span class="name">a</span>
+precedes the invalidation event of 
+the agent denoted by <span class="name">ag</span>, and 
+ the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag</span>
+<a>precedes</a> the activity <a title="activity end event">end</a> event.
+</div>
+
+
+<p>An entity that was attributed to an agent must have some overlap
+with the agent. The agent is required to exist before the entity
+invalidation. Likewise, the entity generation must precede the agent destruction.
+This is
+illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (d) and  expressed by constraint <a href="#wasAttributedWith-ordering">wasAttributedWith-ordering</a>.</p>
+
+
+
+ 
+<div class='constraint' id='wasAttributedTo-ordering'>
+Given an entity denoted by <span class="name">e</span> and an agent denoted by   <span class="name">ag</span>, <span class='conditional'>if</span> <span
+class="name">wasAttributedTo(e,ag)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+<a title="entity generation event">generation</a> event of the entity  denoted by <span class="name">e</span>
+precedes the invalidation event of 
+the agent denoted by <span class="name">ag</span>, and 
+ the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag</span>
+<a>precedes</a> the entity <a title="entity invalidation event">invalidation</a> event.
+</div>
+
+<p>For responsibility, two agents need to have some overlap in their lifetime.</p>
+
+
+<div class='constraint' id='actedOnBehalfOf-ordering'>
+Given two agents <span class="name">ag1</span> and <span class="name">ag2</span>, <span class='conditional'>if</span> <span
+class="name">actedOnBehalfOf(ag2,ag1)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+<a title="entity generation event">generation</a> event of the agent  denoted by <span class="name">ag2</span>
+precedes the invalidation event of 
+agent <span class="name">ag1</span>, and 
+ the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag1</span>
+<a>precedes</a>  <a title="entity invalidation event">invalidation</a> event for <span class="name">ag2</span>.
+</div>
+
+</section> <!--event-ordering-constraints--> 
+
+</section> <!-- constraints -->
+
+<section id="collection-constraints">
+<h2>Collection Constraints</h2>
+
+<p>Membership is a convenience notation, since it can be expressed in terms of an insertion into some collection. The membership definition is formalized by constraint <a href="#membership-as-insertion">membership-as-insertion</a>.</p>
+
+<div class='definition' id='membership-as-insertion'>
+ <span class="name">memberOf(c, {(k1, v1), ...})</span> holds
+<span class='conditional'>if and only if</span> there exists a collection <span class="name">c0</span>, such that
+<span class="name">derivedByInsertionFrom(c, c0, {(k1, v1), ...})</span>.
+</div>
+
+<p>A collection may be obtained by insertion or removal, or said to satisfy the membership relation.
+To provide an interpretation of collections, PROV-DM 
+ restricts one collection to be involved in a single derivation by insertion or removal, or to one membership relation.
+PROV-DM does not provide an interpretation for descriptions that consist of two (or more) insertion, removal, membership relations that result in the same collection.</p>
+
+
+
+<p>The following constraint ensures unique derivation.</p>
+
+
+<div class='note'> The following constraint is unclear.</div>
+<div class='constraint' id='collection-unique-derivation'>
+A collection MUST NOT be derived through multiple insertions, removal,
+  or membership relations. 
+</div>
+
+<div class="anexample">
+Consider the following descriptions about three collections.
+  <pre class="codeexample">
+entity(c1, [prov:type="prov:Collection"  %% xsd:QName])
+entity(c2, [prov:type="prov:Collection"  %% xsd:QName])
+entity(c3, [prov:type="prov:Collection"  %% xsd:QName])
+
+
+derivedByInsertionFrom(c3, c1, {("k1", e1), ("k2", e2)})
+derivedByInsertionFrom(c3, c2, {("k3", e3)})
+</pre>
+<p>There is no interpretation for such descriptions since <span class="name">c3</span> is derived multiple times by insertion.</p>
+</div>
+
+
+<div class="anexample">
+<p>As a particular case, collection <span class="name">c</span> is derived multiple times from the same <span class="name">c1</span>. </p>
+<pre class="codeexample">
+derivedByInsertionFrom(id1, c, c1, {("k1", e1), ("k2", e2)})
+derivedByInsertionFrom(id2, c, c1, {("k3", e3), ("k4", e4)})
+</pre>
+<p>The interpretation of such descriptions is also unspecified. </p>
+<p>To describe the insertion of the 4 key-entity pairs, one would instead write:</p>
+<pre class="codeexample">
+derivedByInsertionFrom(id1, c, c1, {("k1", e1), ("k2", e2), ("k3", e3), ("k4", e4)})
+</pre>  
+</div>
+
+The same is true for any combination of insertions, removals, and membership relations:
+<div class="anexample">
+<p>The following descriptions</p>
+<pre class="codeexample">
+derivedByInsertionFrom(c, c1, {("k1", e1)})
+derivedByRemovalFrom(c, c2, {"k2"})
+</pre>
+have no interpretation.
+Nor have the following:
+<pre class="codeexample">
+derivedByInsertionFrom(c, c1, {("k1", e1)})
+memberOf(c, {"k2"}).
+</pre>
+</div>
+
+
+
+<section id="collection-branching">
+<h4>Collection branching</h4>
+
+It is allowed to have multiple derivations from a single root collection, as long as the resulting entities are distinct, as shown in the following example.
+
+<div class="anexample">
+<pre class="codeexample">
+entity(c0, [prov:type="prov:EmptyCollection" %% xsd:QName])    // c0 is an empty collection
+entity(c1, [prov:type="prov:Collection" %% xsd:QName])
+entity(c2, [prov:type="prov:Collection" %% xsd:QName])
+entity(c3, [prov:type="prov:Collection" %% xsd:QName])
+entity(e1)
+entity(e2)
+entity(e3)
+
+derivedByInsertionFrom(c1, c0, {("k1", e1)})      
+derivedByInsertionFrom(c2, c0, {("k2", e2)})       
+derivedByInsertionFrom(c3, c1, {("k3", e3)})       
+</pre>
+From this set of descriptions, we conclude:
+<pre class="codeexample">
+  c1 = { ("k1", e1) }
+  c2 = { ("k2", e2) }
+  c3 = { ("k1", e1), ("k3", e3)}
+</pre>
+</div>
+
+</section>
+
+  
+
+<section id="collections-and-derivation">
+
+  
+<h4>Collections and Weaker Derivation Relation</h4>
+
+<p>The state of a collection is only known to the extent that a chain of derivations starting from an empty collection can be found. Since a set of descriptions regarding a collection's evolution may be incomplete, so is the reconstructed state obtained by querying those descriptions. In general, all descriptions reflect partial knowledge regarding a sequence of data transformation events. In the particular case of collection evolution, in which some of the state changes may have been missed, the more generic  <a href="#Derivation-Relation">derivation</a> relation should be used to signal that some updates may have occurred, which cannot be expressed as insertions or removals. The following  example illustrates this.</p>
+
+
+ 
+ <div class="anexample">
+In the example, the state of <span class="name">c2</span> is only partially known because the collection is constructed from partially known other collections.
+ <pre class="codeexample">
+entity(c0, [prov:type="prov:EmptyCollection" %% xsd:QName])    // c0 is an empty collection
+entity(c1, [prov:type="prov:Collection" %% xsd:QName])    
+entity(c2, [prov:type="prov:Collection" %% xsd:QName])    
+entity(c3, [prov:type="prov:Collection" %% xsd:QName])    
+entity(e1)
+entity(e2)
+
+derivedByInsertionFrom(c1, c0, {("k1", e1)})       
+wasDerivedFrom(c2, c1)                       
+derivedByInsertionFrom(c3, c2, {("k2", e2)})       
+ </pre>
+From this set of descriptions, we conclude:
+<ul>
+<li>    <span class="name">c1 = { ("k1", e1) }</span>
+<li>    <span class="name">c2</span> is somehow derived from <span class="name">c1</span>, but the precise sequence of updates is unknown
+<li>    <span class="name">c3</span>  includes  <span class="name">("k2", e2)</span> but the earlier "gap" leaves uncertainty regarding  <span class="name">("k1", e1)</span>  (it may have been removed) or any other pair that may have been added as part of the derivation activities.
+</ul>
+ </div>
+
+</section>
+
+
+<div class='note'>
+  Do the insertion/removal derivation steps imply wasDerivedFrom,
+  wasVersionOf, alternateOf?
+  </div>
+ 
+</section> <!-- collection-constraints -->
+
+<section id="account-constraints">
+<h2>Account Constraints</h2>
+
+
+<p>PROV-DM allows for multiple descriptions of entities (and in general any identifiable object) to be expressed. </p>
+
+<div class="anexample" id="example-two-entities-one-id">
+<p>Let us consider two descriptions of a same entity, which we have taken from two different contexts. A working draft published by the <span class="name">w3:Consortium</span>:</p>
+<pre class="codeexample">
+entity(tr:WD-prov-dm-20111215, [ prov:type="pr:RecsWD" %% xsd:QName ])
+</pre>
+The second version of a document edited by some authors:
+<pre class="codeexample">
+entity(tr:WD-prov-dm-20111215, [ prov:type="document", ex:version="2" ])
+</pre>
+<p>Both descriptions are about the same entity identified  by
+<span class="name">tr:WD-prov-dm-20111215</span>, but they contain different attributes, describing the situation or partial state of the these entities according to the context in which they occur.
+</p>
+</div>
+
+
+
+<p>Two different descriptions of a same entity cannot co-exist in a same account
+ as formalized in <a href="#unique-description-in-account">unique-description-in-account</a>.</p>
+
+<div class="note">
+  TODO:
+  We should list all of the other expressions to which this applies,
+  maybe by defining the set of "object expressions" that have an
+  identity.
+  </div>
+<div class='constraint' id='unique-description-in-account'>
+<p>Given an entity identifier <span class="name">e</span>, there is at most one description 
+<span class="name">entity(e,attrs)</span> occurring in a given account, where <span class="name">attrs</span> is some set of attribute-values. Other descriptions of the same entity can exist in different accounts.</p>
+
+<p>This constraint similarly applies to all other types and relations,
+  with explicit identity.</p>
+</div>
+
+<p>
+	<div class="structural-forward">
+	  See Section <a href="#structural-constraints">structural-constraints</a> for a structural constraint on accounts
+	</div>
+
+
+<p>In some cases, there may be a requirement  for two different descriptions of a same entity to be included in a same account. To satisfy the constraint <a href="#unique-description-in-account">unique-description-in-account</a>, we can adopt a different identifier for one of them, and relate the two descriptions with the <span class="name">alternateOf</span> relation. </p>
+
+<div class="anexample" id="merge-with-rename">
+<p>We now reconsider the same two descriptions of a same entity, but we change the identifier for one of them:</p>
+<pre class="codeexample">
+entity(tr:WD-prov-dm-20111215, [ prov:type="pr:RecsWD" %% xsd:QName ])
+entity(ex:alternate-20111215, [ prov:type="document", ex:version="2" ])
+alternateOf(tr:WD-prov-dm-20111215,ex:alternate-20111215)
+</pre>
+</div>
+
+<div class="note">
+  Following text transplanted from structural constraints section.
+  </div>
+
+  <p>
+An account is said to be structurally well-formed if
+it satisfies the constraint  <a href="#generation-uniqueness">generation-uniqueness</a>. If an account is structurally well-formed, it supports the inference <a
+href="#derivation-use">derivation-use</a>.</p>
+
+<div class='note'>
+  Since we are not specifying ways to take the union of two accounts,
+  we may drop this discussion
+  </div>
+<p> Taking the union of two accounts is another account, 
+formed by the union of the descriptions they respectively contain.  We note that the resulting union may or may not invalidate some constraints:
+<ul>
+<li> Two entity descriptions with a same identifier but different sets of attributes exist in each original account may invalidate <a href="#unique-description-in-account">unique-description-in-account</a> in the union, unless some form of description merging or renaming (as per <a href="#merge-with-rename">Example</a>) occurs.
+<li> Structurally well-formed
+accounts are not
+closed under union because the
+constraint <a href="#generation-uniqueness">generation-uniqueness</a> may no
+longer be satisfied in the resulting union.  </li>
+</ul>
+<p>How to reconcile such accounts is beyond the scope of this specification.</p>
+
+
+<div class="note">
+  Material transplanted from structural well-formedness constraints section.
+  
+  This example isn't very clear, since the sub-workflow-ness isn't
+  represented in the data.  According to what was written above, we
+  should conclude that a0 and a2 are equal!
+  </div>
+<div class="anexample">
+<p>
+In the following descriptions, a workflow execution  <span class="name">a0</span> consists of two sub-workflow executions  <span class="name">a1</span> and <span class="name">a2</span>.
+Sub-workflow execution <span class="name">a2</span> generates entity <span class="name">e</span>, so does <span class="name">a0</span>.</p>
+<pre class="codeexample">
+activity(a0, [prov:type="workflow execution"])
+activity(a1, [prov:type="workflow execution"])
+activity(a2, [prov:type="workflow execution"])
+wasInformedBy(a2,a1)
+
+wasGeneratedBy(e,a0)
+wasGeneratedBy(e,a2)
+</pre>
+<p>So, we have two different <a title="generation">generations</a> for entity <span class="name">e</span>.  Such an example is permitted in PROV-DM if the two activities denoted by <span class="name">a0</span> and <span class="name">a2</span> are a single thing happening  in the world
+but described from different perspectives.</p>
+</div>
+
+<p>While this example is permitted in PROV-DM, it does not make the inter-relation between activities explicit, and  it mixes descriptions expressed from different perspectives together. 
+While this may acceptable in some specific applications, it becomes challenging for inter-operability. Indeed, PROV-DM does not offer any relation describing the structure of activities.
+  Such descriptions are said not to be structurally well-formed.</p>
+
+<p>Structurally well-formed provenance can be obtained by partitioning the generations into different accounts. This makes it clear that these generations provide alternative
+descriptions of the same real-world generation event, rather than describing two distinct generation events for the same entity. When accounts are used, the example can be encoded as follows.</p>
+
+
+<div class="anexample">
+<p>
+The same example is now revisited, with the following descriptions that are structurally well-formed. Two accounts are introduced, and there is a single generation for entity <span
+class="name">e</span> per account.</p>
+
+<p>In a first account, entitled "summary", we find:</p>
+<pre class="codeexample">
+activity(a0,t1,t2,[prov:type="workflow execution"])
+wasGeneratedBy(e,a0,-)
+</pre>
+<p>In a second account, entitled "detail", we find:</p>
+<pre class="codeexample">
+activity(a1,t1,t3,[prov:type="workflow execution"])
+activity(a2,t3,t2,[prov:type="workflow execution"])
+wasInformedBy(a2,a1)
+wasGeneratedBy(e,a2,-)
+</pre>
+</div>
+
+
+<div class='note'>Collect the discussion of uniqueness of generation
+  in one place</div>
+  
+<p>Structurally well-formed provenance satisfies some constraints, which force the structure of descriptions to be exposed by means of accounts. With these constraints satisfied, further
+inferences can be made about structurally well-formed descriptons.
+The uniqueness of generations in accounts is formulated as follows.
+</p>
+
+
+
+  
+</section> <!-- account-constraints-->
+
+
+
+
+
+
+<section id="compliance">
+<h2>Compliance with this document</h2>
+
+For the purpose of compliance, the normative sections of this document
+  are (TODO).  To be compliant:
+  <ul><li>When processing provenance obtained from another source, an
+    application MAY apply the inferences and definitions in <a
+    href="#inferences" class='sectionRef'></a>.</li>
+    <li> When producing provenance meant for other applications to
+    use, the application SHOULD produce valid provenance. </li>
+    <li>When determining whether provenance is <a>valid</a>, an
+    application MUST check that all of the
+    constraints are satisfied, even if some 
+    inferences and definitions are used.</li>
+</ul>
+  <div class="note">
+    Should we specify a way for PROV-DM instances to say whether they
+    are meant to be validated or not?
+  </div>
+  
+</section>
+
+
+  <section id='rationale' class="informative">
+<h2>Rationale for inferences and constraints</h2>
+
+
+  
 <div class='note'>TODO: Better section title/headings; move this
   material later or embed it into appropriate sections</div>
+
+    <section id='section-attributes'> 
+<h4>Entities and Attributes</h4>
+
+<p>When we talk about things in the world in natural language and even when we assign identifiers, we are often imprecise in ways that make it difficult to clearly and unambiguously report
+provenance: a resource with a URL may be understood as referring to a report available at that URL, the version of the report available there today, the report independent of where it is
+hosted over time, etc.
+However, to write precise descriptions of the provenance of things
+that change over time, we need ways of disambiguating which versions
+of things we are talking about.  
+</p>
+
+<p>
+<!--From a provenance viewpoint, it is important to identify a
+<em>partial state</em> of something, i.e. something with some aspects
+that have been fixed, so that it becomes possible to express its
+provenance, and what causes that thing, with these specific
+aspects.-->
+To describe the provenance of things that can change over
+time, PROV-DM uses the concept of <i>entities</i> with fixed
+attributes.  From a provenance viewpoint, it is important to identify
+a partial state of something, i.e. something with some aspects that
+have been fixed, so that it becomes possible to express its provenance
+(i.e. what caused the thing with these specific aspects).  An entity
+encompasses a part of a thing's history during which some of the
+attributes are fixed.  An entity can thus be thought of as a part of a
+thing with some associated partial state.
+Attribures in PROV-DM are used to fix certain aspects of entities.</p>
+
+<!--<p>Attributes in PROV-DM describe some aspects of entities.
+Indeed, we previously defined 
+entities as things one wants to provide provenance for;
+we refine this definition as follows, using attribute-values to describe entities' partial states, and linking them to the very existence of entities.</p>
+-->
+
+<p>
+An <dfn>entity</dfn> is a thing one wants to provide provenance for
+and whose situation in the world is described by some fixed
+attributes. An entity has a <dfn
+id="|dfn-characterization-interval">characterization interval</dfn>,
+or <dfn id="lifetime">lifetime</dfn>,
+defined as the period
+between its <a title="entity generation event">generation event</a>
+and its <a title="entity invalidation event">invalidation event</a>.
+An entity's attributes are established when the entity is
+created and describe the entity's situation and (partial) state
+during an entity's lifetime.</p>
+
+<p><!--An entity fixes some aspects of a thing and its situation in the
+world.-->
+A different entity (perhaps representing a different user or
+system perspective) may fix other aspects of the same thing, and its provenance
+may be different.  Different entities that are aspects of the same
+thing are called <em>alternate</em>, and the PROV-DM relations of
+specialization and alternate can be used to link such entities.</p>
+
+
+<div class="note">
+  The following statement should be put somewhere normative, ideally
+  in PROV-DM itself, to clarify the rules about optional attributes.
+  </div>
+  
+<div id="optional-attributes1">PROV-DM allows for some attributes to be optionally expressed. Unless otherwise specified, when an optional attribute is not present in a description, some value SHOULD be assumed to exist for this attribute, though it is not known which.  </div>
+
+
+
+
+<div class="anexample" id="a-report-example">
+Different users may take different perspectives on a resource with
+a URL. A provenance record might use one (or more)  different
+  entities to talk about different persectives, such as:
+<ul>
+<li>a report available at a URL: fixes the nature of the thing, i.e. a document, and its location; </li>
+<li>the version of the report available there today: fixes its version number, contents, and its date;</li>
+<li>the report independent of where it is hosted and of its content over time: fixes the nature of the thing as a conceptual artifact.</li></ul>
+The provenance of these three entities may differ, and may be along the following lines: 
+<ul>
+<li>the provenance of a report available at a URL may include: the act of publishing it and making it available at a given location, possibly under some license and access control;</li>
+<li>the provenance of the version of the report available there today may include: the authorship of the specific content, and reference to imported content;</li>
+<li>the provenance of the report independent of where it is hosted over time may include: the motivation for writing the report, the overall methodology for producing it, and the broad team
+involved in it.</li>
+</ul>
+<p>We do not assume that any entity is a better or worse description of
+reality than any other.  That is, we do not assume an absolute ground truth with
+respect to which we can judge correctness or completeness of
+descriptions.  In fact, it is possible to describe the processing that occurred for the report to be commissioned, for
+individual versions to be created, for those versions to be published at the given URL, etc., each via a different entity with attribute-value pairs that fix some aspects of the report appropriately.</p>
+</div>
+
+
+<p>Besides entities, a variety of other PROV-DM objects have
+attributes, including activity, generation, usage, start, end,
+communication, attribution, association, responsibility, and
+derivation. Each object has an associated duration interval (which may
+be a single time point), and attribute-value pairs for a given object
+are expected to be descriptions that hold for the object's duration.
+</p>
+<p>
+However, the attributes of entities have special meaning because they
+are considered to be fixed aspects
+of underlying, changing things.  This means, for example, that
+if two entities have overlapping lifetimes and they have some
+attributes in common, those attributes SHOULD match.  </p>
+<div class="note">
+  @@TODO:
+Constraints for this?
+  </div>
+</section>
+
+
+
+    <section id="representation-term-assertion-inference"> 
+<h3>Description, Assertion, and Inference</h3>
+
+<p>
+PROV-DM is a provenance data model designed to express <em>descriptions</em> of the world. 
+</p>
+
+<div class="anexample">
+A file at some point during its lifecycle, which includes multiple edits by multiple people, can be described by its type, its location in the file system, a creator, and content.  
+</div>
+
+
+<p>The data model is designed to capture activities that happened in the past, as opposed to activities
+that may or will happen. 
+However, this distinction is not formally enforced.
+Therefore, all PROV-DM descriptions SHOULD be interpreted as what has happened, as opposed to what may or will happen.</p>
+
+
+
+<p> 
+This specification does not prescribe the means by which descriptions can be arrived at; for example, descriptions can be composed on the basis of observations, reasoning, or any other means. 
+</p>
+
+
+<p>
+Sometimes, inferences about the world can be made from descriptions
+conformant to the PROV-DM data model. This
+specification defines some such inferences, allowing new descriptions
+to be inferred from existing ones. Hence, descriptions of the world
+can result either from direct assertion or from inference 
+by application of inference rules defined by this specification.
+</p>
+
+
+</section>
+
+
+
+
+
+    <section id='section-event-time'> 
+<h4>Events and Time</h4>
+
   
 <p>The PROV-DM data model is implicitly based on a notion of <dfn
   id="dfn-event">instantaneous event</dfn>s (or just <a
@@ -341,9 +1502,6 @@
 <i>validity</i> constraints indicating when provenance is self-consistent. </p>
 
 
-    <section id='section-time-event'> 
-<h4>Time and Event</h4>
-
 <p>Time is critical in the context of provenance, since it can help corroborate provenance claims. For instance, if an entity is claimed to be obtained by transforming another, then the
 latter must have existed before the former. If it is not the case, then there is something wrong with such a provenance claim. </p>
 
@@ -474,148 +1632,6 @@
 
 </section>
 
-    <section id='section-attributes'> 
-<h4>Entities and Attributes</h4>
-
-<p>When we talk about things in the world in natural language and even when we assign identifiers, we are often imprecise in ways that make it difficult to clearly and unambiguously report
-provenance: a resource with a URL may be understood as referring to a report available at that URL, the version of the report available there today, the report independent of where it is
-hosted over time, etc.
-However, to write precise descriptions of the provenance of things
-that change over time, we need ways of disambiguating which versions
-of things we are talking about.  
-</p>
-
-<p>
-<!--From a provenance viewpoint, it is important to identify a
-<em>partial state</em> of something, i.e. something with some aspects
-that have been fixed, so that it becomes possible to express its
-provenance, and what causes that thing, with these specific
-aspects.-->
-To describe the provenance of things that can change over
-time, PROV-DM uses the concept of <i>entities</i> with fixed
-attributes.  From a provenance viewpoint, it is important to identify
-a partial state of something, i.e. something with some aspects that
-have been fixed, so that it becomes possible to express its provenance
-(i.e. what caused the thing with these specific aspects).  An entity
-encompasses a part of a thing's history during which some of the
-attributes are fixed.  An entity can thus be thought of as a part of a
-thing with some associated partial state.
-Attribures in PROV-DM are used to fix certain aspects of entities.</p>
-
-<!--<p>Attributes in PROV-DM describe some aspects of entities.
-Indeed, we previously defined 
-entities as things one wants to provide provenance for;
-we refine this definition as follows, using attribute-values to describe entities' partial states, and linking them to the very existence of entities.</p>
--->
-
-<p>
-An <dfn>entity</dfn> is a thing one wants to provide provenance for
-and whose situation in the world is described by some fixed
-attributes. An entity has a <dfn
-id="|dfn-characterization-interval">characterization interval</dfn>,
-or <dfn id="lifetime">lifetime</dfn>,
-defined as the period
-between its <a title="entity generation event">generation event</a>
-and its <a title="entity invalidation event">invalidation event</a>.
-An entity's attributes are established when the entity is
-created and describe the entity's situation and (partial) state
-during an entity's lifetime.</p>
-
-<p><!--An entity fixes some aspects of a thing and its situation in the
-world.-->
-A different entity (perhaps representing a different user or
-system perspective) may fix other aspects of the same thing, and its provenance
-may be different.  Different entities that are aspects of the same
-thing are called <em>alternate</em>, and the PROV-DM relations of
-specialization and alternate can be used to link such entities.</p>
-
-
-
-
-
-
-<div class="anexample" id="a-report-example">
-Different users may take different perspectives on a resource with
-a URL. A provenance record might use one (or more)  different
-  entities to talk about different persectives, such as:
-<ul>
-<li>a report available at a URL: fixes the nature of the thing, i.e. a document, and its location; </li>
-<li>the version of the report available there today: fixes its version number, contents, and its date;</li>
-<li>the report independent of where it is hosted and of its content over time: fixes the nature of the thing as a conceptual artifact.</li></ul>
-The provenance of these three entities may differ, and may be along the following lines: 
-<ul>
-<li>the provenance of a report available at a URL may include: the act of publishing it and making it available at a given location, possibly under some license and access control;</li>
-<li>the provenance of the version of the report available there today may include: the authorship of the specific content, and reference to imported content;</li>
-<li>the provenance of the report independent of where it is hosted over time may include: the motivation for writing the report, the overall methodology for producing it, and the broad team
-involved in it.</li>
-</ul>
-<p>We do not assume that any entity is a better or worse description of
-reality than any other.  That is, we do not assume an absolute ground truth with
-respect to which we can judge correctness or completeness of
-descriptions.  In fact, it is possible to describe the processing that occurred for the report to be commissioned, for
-individual versions to be created, for those versions to be published at the given URL, etc., each via a different entity with attribute-value pairs that fix some aspects of the report appropriately.</p>
-</div>
-
-
-<p>Besides entities, a variety of other PROV-DM objects have
-attributes, including activity, generation, usage, start, end,
-communication, attribution, association, responsibility, and
-derivation. Each object has an associated duration interval (which may
-be a single time point), and attribute-value pairs for a given object
-are expected to be descriptions that hold for the object's duration.
-</p>
-<p>
-However, the attributes of entities have special meaning because they
-are considered to be fixed aspects
-of underlying, changing things.  This means, for example, that
-if two entities have overlapping lifetimes and they have some
-attributes in common, those attributes SHOULD match.  </p>
-<div class="note">
-  @@TODO:
-Constraints for this?
-  </div>
-</section>
-
-
-
-    <section id="representation-term-assertion-inference"> 
-<h3>Description, Assertion, and Inference</h3>
-
-<p>
-PROV-DM is a provenance data model designed to express <em>descriptions</em> of the world. 
-</p>
-
-<div class="anexample">
-A file at some point during its lifecycle, which includes multiple edits by multiple people, can be described by its type, its location in the file system, a creator, and content.  
-</div>
-
-
-<p>The data model is designed to capture activities that happened in the past, as opposed to activities
-that may or will happen. 
-However, this distinction is not formally enforced.
-Therefore, all PROV-DM descriptions SHOULD be interpreted as what has happened, as opposed to what may or will happen.</p>
-
-
-
-<p> 
-This specification does not prescribe the means by which descriptions can be arrived at; for example, descriptions can be composed on the basis of observations, reasoning, or any other means. 
-</p>
-
-
-<p>
-Sometimes, inferences about the world can be made from descriptions
-conformant to the PROV-DM data model. This
-specification defines some such inferences, allowing new descriptions
-to be inferred from existing ones. Hence, descriptions of the world
-can result either from direct assertion or from inference 
-by application of inference rules defined by this specification.
-</p>
-
-
-</section>
-
-
-
 
     <section  id="account-section">
       <h3>Account</h3>
@@ -666,17 +1682,13 @@
 
 
 
-<section id="definitional-constraints"> 
-
-<h2>PROV-DM Definitional Constraints and Inferences</h2>
-
-<p>In this section, we revisit the types and relations of PROV-DM that have constraints associated with their definitions.  </p>
-
-<p>
-<div id="optional-attributes1">PROV-DM allows for some attributes to be optionally expressed. Unless otherwise specified, when an optional attribute is not present in a description, some value SHOULD be assumed to exist for this attribute, though it is not known which.  </div>
-
-
-
+<section id="definitional-constraints">
+<h2>[OLD] Definitional constraints and inferences</h2>
+
+<div class="Note">
+  This material is out of date.  All constraints from it have been
+  moved to the main body.</div>
+  
 
    <section id="component1"> 
 <h3>Component 1: Entities and Activities</h3>
@@ -825,6 +1837,8 @@
 
 
 
+
+
 <p>
 A usage identifier is OPTIONAL. It MUST be present when annotating usages or when defining derivations (see
 <a href="#Derivation-Relation">Derivation</a>).</p>
@@ -1317,906 +2331,10 @@
 
 
 
-
-
-
-</section>
-
-
-
-
-<section id="account-constraints"> 
-<h3>PROV-DM Account Constraints</h3>
-
-
-<p>PROV-DM allows for multiple descriptions of entities (and in general any identifiable object) to be expressed. </p>
-
-<div class="anexample" id="example-two-entities-one-id">
-<p>Let us consider two descriptions of a same entity, which we have taken from two different contexts. A working draft published by the <span class="name">w3:Consortium</span>:</p>
-<pre class="codeexample">
-entity(tr:WD-prov-dm-20111215, [ prov:type="pr:RecsWD" %% xsd:QName ])
-</pre>
-The second version of a document edited by some authors:
-<pre class="codeexample">
-entity(tr:WD-prov-dm-20111215, [ prov:type="document", ex:version="2" ])
-</pre>
-<p>Both descriptions are about the same entity identified  by
-<span class="name">tr:WD-prov-dm-20111215</span>, but they contain different attributes, describing the situation or partial state of the these entities according to the context in which they occur.
-</p>
-</div>
-
-
-
-<p>Two different descriptions of a same entity cannot co-exist in a same account
- as formalized in <a href="#unique-description-in-account">unique-description-in-account</a>.</p>
-
-<div class="note">
-  TODO:
-  We should list all of the other expressions to which this applies,
-  maybe by defining the set of "object expressions" that have an
-  identity.
-  </div>
-<div class='constraint' id='unique-description-in-account'>
-<p>Given an entity identifier <span class="name">e</span>, there is at most one description 
-<span class="name">entity(e,attrs)</span> occurring in a given account, where <span class="name">attrs</span> is some set of attribute-values. Other descriptions of the same entity can exist in different accounts.</p>
-
-<p>This constraint similarly applies to all other types and relations,
-  with explicit identity.</p>
-</div>
-
-<p>
-	<div class="structural-forward">
-	  See Section <a href="#structural-constraints">structural-constraints</a> for a structural constraint on accounts
-	</div>
-
-
-<p>In some cases, there may be a requirement  for two different descriptions of a same entity to be included in a same account. To satisfy the constraint <a href="#unique-description-in-account">unique-description-in-account</a>, we can adopt a different identifier for one of them, and relate the two descriptions with the <span class="name">alternateOf</span> relation. </p>
-
-<div class="anexample" id="merge-with-rename">
-<p>We now reconsider the same two descriptions of a same entity, but we change the identifier for one of them:</p>
-<pre class="codeexample">
-entity(tr:WD-prov-dm-20111215, [ prov:type="pr:RecsWD" %% xsd:QName ])
-entity(ex:alternate-20111215, [ prov:type="document", ex:version="2" ])
-alternateOf(tr:WD-prov-dm-20111215,ex:alternate-20111215)
-</pre>
-</div>
-
-
-</section>
-
-
-    <section id="interpretation"> 
-<h3>PROV-DM Event Ordering Constraints</h3>
-
-<p>Section <a href="#section-time-event">section-time-event</a>
-introduces a notion of <a title="instantaneous event">instantaneous event</a>
-marking changes in the world, in its activities and entities.  PROV-DM
-identifies five kinds of <a title="instantaneous event">instantaneous events</a>, namely <a>entity generation
-event</a>, <a>entity usage event</a>, <a>entity invalidation event</a>, <a>activity start event</a>
-and <a>activity end event</a>.  PROV-DM adopts Lamport's clock
-assumptions [[CLOCK]] in the form of a reflexive, transitive partial order <a>follows</a>
-(and its inverse <a>precedes</a>) between <a title="instantaneous event">instantaneous events</a>.  Furthermore,
-PROV-DM assumes the existence of a mapping from <a title="instantaneous event">instantaneous events</a> to time clocks,
-though the actual mapping is not in scope of this specification.</p>
-
-<p>Given that provenance consists of a description of past entities
-and activities, to be valid provenance descriptions MUST
-satisfy <em>ordering constraints</em> between instantaneous events, which we introduce in
-this section.  For instance, an entity can only be used after it was
-generated; hence, we say that an entity's <a title="entity generation
-event">generation event</a> precedes any of this
-entity's <a title="entity usage event">usage event</a>.  Should this
-ordering constraint be proven invalid, the associated generation and
-usage could not be credible.  The rest of this section defines
-the <dfn>temporal interpretation</dfn> of provenance descriptions as a
-set of instantaneous event ordering constraints. </p>
-
-
-<p>PROV-DM also allows for time observations to be inserted in
-specific provenance descriptions, for each of the five kinds
-of <a title="instantaneous event">instantaneous events</a> introduced in this specification.  The
-presence of a time observation for a given <a>instantaneous event</a> fixes the
-mapping of this <a>instantaneous event</a> to the timeline. The presence of time
-information in a provenance description instantiates the ordering constraint with
-that time information. It is expected that such instantiated
-constraints can help corroborate provenance information. We anticipate
-that verification algorithms could be developed, though this
-verification is outside the scope of this specification.
-</p>
-
-<p>The following figure summarizes the ordering constraints in a
-graphical manner. For each subfigure, an event time line points to the
-right. Activities are represented by rectangles, whereas entities are
-represented by circles. Usage, generation and derivation are
-represented by the corresponding edges between entities and
-activities.  The five kinds of <a title="instantaneous event">instantaneous events</a> are represented by vertical
-dotted lines (adjacent to the vertical sides of an activity's
-rectangle, or intersecting usage and generation edges).  The ordering
-constraints are represented by triangles: an occurrence of a triangle between two <a title="instantaneous event">instantaneous event</a> vertical dotted lines represents that the event denoted by the left
-line precedes the event denoted by the right line.</p>
-
-<div style="text-align: center;">
-<figure>
-<figcaption id="constraint-summary">Summary of <a title="instantaneous event">instantaneous event</a> ordering constraints</figcaption>
-<img src="images/constraints.png" alt="constraints between events" />
-</figure>
-</div>
-
-
-
-<p>The existence of an activity implies that the <a>activity start event</a> always <a>precedes</a> the corresponding <a>activity end
-event</a>.  This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (a) and  expressed by constraint <a href="#start-precedes-end">start-precedes-end</a>.</p> 
-
-<div class='interpretation' id='start-precedes-end'> The following ordering constraint holds for any activity: the
-<a title="activity start event">start event</a> <a>precedes</a> the <a title="activity end event">end event</a>.</div> 
-
-<p> A usage and a generation for a given entity implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation
-event">generation event</a> had to precede the <a title="entity usage event">usage event</a>. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (b) and  expressed by constraint <a href="#generation-precedes-usage">generation-precedes-usage</a>.</p>
-
-<div class='interpretation' id='generation-precedes-usage'>For any entity, the following ordering constraint holds: the <a title="entity generation event">generation</a> of an entity always
-<a>precedes</a> any of its <a title="entity usage event">usages</a>.
-</div>
-
-<div class="note">
-ISSUE-345: does not clearly delineate where the discussion for one constraint starts and where the next ends.
- </div>
-
-<p>Invalidation is defined at the event at which an entity ceases to exist as such.   All usages of an entity precede its invalidation, which is captured by constraint <a href="#usage-precedes-invalidation">usage-precedes-invalidation</a> (without any explicit graphical representation).</p> 
-
-<div class='interpretation' id='usage-precedes-invalidation'>For any entity, the following ordering constraint holds: any <a title="entity usage event">usage</a> of an entity always
-<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
-</div>
-
-<p>Similarly, generation of an entity precedes its invalidation. (This
-follows from other constraints if the entity is used, but we state it
-explicitly to cover the case of an entity that is generated and
-invalidated without being used.)</p>
-
-<div class='interpretation' id='generation-precedes-invalidation'>For
-  any entity, the following ordering constraint holds: the <a
-  title="entity generation event">generation</a> of an entity always
-<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
-</div>
-
-<p>A usage implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity usage event">usage event</a> had to occur during the associated activity. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (c) and  expressed by constraint <a href="#usage-within-activity">usage-within-activity</a>.</p>
-
-<div class='interpretation' id='usage-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
-of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>
-  <span class="name">used(a,e,attrs)</span> or <span class="name">used(a,e,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint holds:
- the <a title="entity usage event">usage</a> of the entity  denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a> of
-activity denoted by <span class="name">a</span> and <a>follows</a> its <a title="activity start event">start</a>. 
-</div>
-
-
-
-<p>A generation implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation event">generation event</a> had to occur during the associated activity. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (d) and  expressed by constraint <a href="#generation-within-activity">generation-within-activity</a>.</p> 
-
-<div class='interpretation' id='generation-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
-of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>  <span class="name">wasGeneratedBy(e,a,attrs)</span> or <span
-class="name">wasGeneratedBy(e,a,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint also holds: the <a title="entity generation
-event">generation</a> of the entity denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a>
-of activity <span class="name">a</span> and <a>follows</a> the <a title="activity start event">start</a> of <span class="name">a</span>. 
-</div> 
-
-
-
-
-<p>If there is a derivation between <span class="name">e2</span> and <span class="name">e1</span>, then 
-this means that the entity <span class="name">e1</span> had some form of influence on the entity <span class="name">e2</span>; for this to be possible, some event ordering must be satisfied.
-First, we consider derivations, where the activity and usage are known. In that case, the <a title="entity usage event">usage</a> of <span class="name">e1</span> has to precede the <a title="entity generation
-event">generation</a> of <span class="name">e2</span>.
-This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (e) and  expressed by constraint <a
-href="#derivation-usage-generation-ordering">derivation-usage-generation-ordering</a>.</p>
-
-
-<div class='interpretation' id='derivation-usage-generation-ordering'>Given an activity with identifier <span class="name">a</span>,  entities with identifier <span
-class="name">e1</span> and <span class="name">e2</span>, a generation identified by <span class="name">g2</span>, and a usage identified by <span class="name">u1</span>, <span
-class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1,attrs)</span>
- holds, <span class='conditional'>then</span>
-the following ordering constraint holds:
-the <a title="entity usage event">usage</a>
-of entity denoted by <span class="name">e1</span> <a>precedes</a> the <a title="entity generation event">generation</a> of
-the entity denoted by <span class="name">e2</span>.
-</div>
-
-<p>When the usage is unknown, a similar constraint exists, except that the constraint refers to its
-generation event, as
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (f) and  expressed by constraint <a
-href="#derivation-generation-generation-ordering">derivation-generation-generation-ordering</a>.</p>
-
-<div class='interpretation' id='derivation-generation-generation-ordering'>
-Given two entities denoted by <span class="name">e1</span> and <span class="name">e2</span>, <span class='conditional'>if</span> <span
-class="name">wasDerivedFrom(e2,e1, attrs)</span>
- holds, <span class='conditional'>then</span> the following ordering constraint holds:
-the <a title="entity generation event">generation event</a> of the entity denoted by <span class="name">e1</span> <a>precedes</a> the <a title="entity generation event">generation event</a>
-of
-the entity  denoted by <span class="name">e2</span>.
-  </div>
-
-<p>Note that event ordering is between generations of <span class="name">e1</span>
-and <span class="name">e2</span>, as opposed to derivation where usage is known,
-which implies ordering ordering between the usage of <span class="name">e1</span> and
-generation of <span class="name">e2</span>.  </p>
-
-<p>Communication between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
-title="instantaneous event">events</a>, since some entity must have been generated by the former and used by the latter, which implies that the start event of  <span class="name">a1</span>
-cannot follow the end event of  <span class="name">a2</span>. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (g) and  expressed by constraint <a href="#wasInformedBy-ordering">wasInformedBy-ordering</a>.</p>
-
-<div class='interpretation' id='wasInformedBy-ordering'>
-Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
-class="name">wasInformedBy(a2,a1)</span>
- holds, <span class='conditional'>then</span> the following ordering constraint holds:
-the <a title="activity start event">start event</a> of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity end event">end event</a> of
-the activity denoted by <span class="name">a2</span>.
-</div>
-
-<p>Start of <span class="name">a2</span> by activity <span class="name">a1</span> also implies ordering of <a
-title="instantaneous event">events</a>, since  <span class="name">a1</span> must have been active before   <span class="name">a2</span> started. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (h) and  expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
-
-
-<div class='interpretation' id='wasStartedBy-ordering'>
-Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
-class="name">wasStartedBy(a2,a1)</span>
- holds, <span class='conditional'>then</span> the following ordering constraint holds: the
-<a title="activity start event">start</a> event of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity start event">start event</a> of
-the activity denoted by <span class="name">a2</span>.
-</div>
-
-
-<p>Further constraints appear in Figure <a href="#constraint-summary2">constraint-summary2</a> and are discussed below.</p>
-
-<div style="text-align: center;">
-<figure>
-<figcaption id="constraint-summary2">Summary of <a title="instantaneous event">instantaneous event</a> ordering constraints (continued)</figcaption>
-<img src="../images/constraints2.png" alt="further constraints between events" />
-</figure>
-</div>
-
-
-<p>The agent that started an activity must exist before the activity starts.
-This is
-illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (a) and  expressed by constraint <a href="#wasStartedByAgent-ordering">wasStartedByAgent-ordering</a>.</p>
-
-
-<div class='interpretation' id='wasStartedByAgent-ordering'>
-Given an activity denoted by <span class="name">a</span> and an entity denoted by   <span class="name">e</span>, <span class='conditional'>if</span>  <span
-class="name">wasStartedBy(a,e)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
-<a title="activity start event">start</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
-<a>precedes</a> the invalidation event of 
-the same entity.
-</div>
-
-<p> Similarly, if an agent is associated with an activity then the
-agent must exist before the activity starts and persist until the
-activity ends, as illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (b).</p>
-
-
-<div class='interpretation' id='wasEndedByAgent-ordering'>
-Given an activity denoted by <span class="name">a</span> and an entity denoted by   <span class="name">e</span>, <span class='conditional'>if</span>  <span
-class="name">wasEndedBy(a,e)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
-<a title="activity end event">end</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
-<a>precedes</a> the invalidation event of 
-the same entity.
-</div>
-
-
-<p>An activity that was associated with an agent must have some overlap with the agent. The agent may be generated, or may only become associated with the activity, after the activity start: so, the agent is required to exist before the activity end. Likewise, the agent may be destructed, or may terminate its association with the activity, before the activity end: hence, the agent invalidation is required to happen after the activity start.
-This is
-illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (c) and  expressed by constraint <a href="#wasAssociatedWith-ordering">wasAssociatedWith-ordering</a>.</p>
-
-
-<div class='interpretation' id='wasAssociatedWith-ordering'>
-Given an activity denoted by <span class="name">a</span> and an agent denoted by   <span class="name">ag</span>, <span class='conditional'>if</span> <span
-class="name">wasAssociatedWith(a,ag)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
-<a title="activity start event">start</a> event of the activity  denoted by <span class="name">a</span>
-precedes the invalidation event of 
-the agent denoted by <span class="name">ag</span>, and 
- the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag</span>
-<a>precedes</a> the activity <a title="activity end event">end</a> event.
-</div>
-
-
-<p>An entity that was attributed to an agent must have some overlap
-with the agent. The agent is required to exist before the entity
-invalidation. Likewise, the entity generation must precede the agent destruction.
-This is
-illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (d) and  expressed by constraint <a href="#wasAttributedWith-ordering">wasAttributedWith-ordering</a>.</p>
-
-
-
- 
-<div class='interpretation' id='wasAttributedTo-ordering'>
-Given an entity denoted by <span class="name">e</span> and an agent denoted by   <span class="name">ag</span>, <span class='conditional'>if</span> <span
-class="name">wasAttributedTo(e,ag)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
-<a title="entity generation event">generation</a> event of the entity  denoted by <span class="name">e</span>
-precedes the invalidation event of 
-the agent denoted by <span class="name">ag</span>, and 
- the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag</span>
-<a>precedes</a> the entity <a title="entity invalidation event">invalidation</a> event.
-</div>
-
-<p>For responsibility, two agents need to have some overlap in their lifetime.</p>
-
-
-<div class='interpretation' id='actedOnBehalfOf-ordering'>
-Given two agents <span class="name">ag1</span> and <span class="name">ag2</span>, <span class='conditional'>if</span> <span
-class="name">actedOnBehalfOf(ag2,ag1)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
-<a title="entity generation event">generation</a> event of the agent  denoted by <span class="name">ag2</span>
-precedes the invalidation event of 
-agent <span class="name">ag1</span>, and 
- the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag1</span>
-<a>precedes</a>  <a title="entity invalidation event">invalidation</a> event for <span class="name">ag2</span>.
-</div>
-
-<!--
-<p>Finally, two entities that are alternate of each other need to have some overlap.</p>
-
-<div class='interpretation' id='alternate-ordering'>
-Given two entities <span class="name">e1</span> and <span class="name">e2</span>, <span class='conditional'>if</span> <span
-class="name">alternate(e2,e1)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
-<a title="entity generation event">generation</a> event of the entity  denoted by <span class="name">e2</span>
-precedes the invalidation event of 
-entity <span class="name">e1</span>, and 
- the <a title="entity generation event">generation event</a> for entity denoted by <span class="name">e1</span>
-<a>precedes</a>  <a title="entity invalidation event">invalidation</a> event for <span class="name">ag2</span>.
-</div>
-
--->
-
 </section>
 
-<section id="structural-constraints"> 
-<h3>PROV-DM Structural Constraints</h3>
-
-<p><a href="#definitional-constraints">Section 3</a> provides definitional constraints for data model concepts.
-<a href="#account-constraints">Section 4</a> introduces constraints on descriptions occurring in accounts.
-<a href="#interpretation">Section 5</a> defines an interpretation of this data model, in terms of event ordering
-constraints.  
-This section introduces further constraints on the structure of PROV-DM descriptions.  Descriptions that satisfy these constraints are said to be <dfn>structurally well-formed</dfn>.  A
-benefit of structurally well-formed provenance descriptions is that further inferences can be made, because descriptions are more precise, and therefore, richer. </p>
-
-<p>We assume that an entity has exactly one generation and
-invalidation event (either or both may, however, be left implicit).
-<!--
-If there are
-multiple generation events, According to the definition of a <a>generation</a>, an entity
-becomes available after its generation event, and does not exist before this event.  From this definition,
-we conclude that PROV-DM does not allow for an entity to have two generations occurring at two different instants.
-The rationale for this constraint is as follows.
- Two distinct <a title="entity generation event">generation events</a> (by a same activity or by two distinct activities), occurring one after the other, necessarily create two distinct
-entities; otherwise, the second <a title="entity generation event">generation event</a> would have resulted in an entity that existed before its creation, which contradicts the definition of
-<a>generation</a>.--></p>
-
-<p>So, PROV-DM allows for two distinct <a>generations</a>  <span class="name">g1</span> and <span class="name">g2</span> referencing a same entity provided they occur
-<em>simultaneously</em>. 
-<!-- (This means that <span class="name">g1</span> <a>precedes</a> <span class="name">g2</span> and <span class="name">g2</span> <a>precedes</a> <span class="name">g1</span>.) -->
-  In practice, for such a simultaneous generation to occur, the generation event has to be unique and caused by a <em>single world activity</em>, though  provenance may contain
-several  descriptions for the <em>same</em> world activity. 
-</p>
-
-<div class="anexample">
-<p>
-In the following descriptions, a workflow execution  <span class="name">a0</span> consists of two sub-workflow executions  <span class="name">a1</span> and <span class="name">a2</span>.
-Sub-workflow execution <span class="name">a2</span> generates entity <span class="name">e</span>, so does <span class="name">a0</span>.</p>
-<pre class="codeexample">
-activity(a0, [prov:type="workflow execution"])
-activity(a1, [prov:type="workflow execution"])
-activity(a2, [prov:type="workflow execution"])
-wasInformedBy(a2,a1)
-
-wasGeneratedBy(e,a0)
-wasGeneratedBy(e,a2)
-</pre>
-<p>So, we have two different <a title="generation">generations</a> for entity <span class="name">e</span>.  Such an example is permitted in PROV-DM if the two activities denoted by <span class="name">a0</span> and <span class="name">a2</span> are a single thing happening  in the world
-but described from different perspectives.</p>
-</div>
-
-<p>While this example is permitted in PROV-DM, it does not make the inter-relation between activities explicit, and  it mixes descriptions expressed from different perspectives together. 
-While this may acceptable in some specific applications, it becomes challenging for inter-operability. Indeed, PROV-DM does not offer any relation describing the structure of activities.
-  Such descriptions are said not to be structurally well-formed.</p>
-
-<p>Structurally well-formed provenance can be obtained by partitioning the generations into different accounts. This makes it clear that these generations provide alternative
-descriptions of the same real-world generation event, rather than describing two distinct generation events for the same entity. When accounts are used, the example can be encoded as follows.</p>
-
-
-<div class="anexample">
-<p>
-The same example is now revisited, with the following descriptions that are structurally well-formed. Two accounts are introduced, and there is a single generation for entity <span
-class="name">e</span> per account.</p>
-
-<p>In a first account, entitled "summary", we find:</p>
-<pre class="codeexample">
-activity(a0,t1,t2,[prov:type="workflow execution"])
-wasGeneratedBy(e,a0,-)
-</pre>
-<p>In a second account, entitled "detail", we find:</p>
-<pre class="codeexample">
-activity(a1,t1,t3,[prov:type="workflow execution"])
-activity(a2,t3,t2,[prov:type="workflow execution"])
-wasInformedBy(a2,a1)
-wasGeneratedBy(e,a2,-)
-</pre>
-</div>
-
-
-<div class='note'>Collect the discussion of uniqueness of generation
-  in one place</div>
-  
-<p>Structurally well-formed provenance satisfies some constraints, which force the structure of descriptions to be exposed by means of accounts. With these constraints satisfied, further
-inferences can be made about structurally well-formed descriptons.
-The uniqueness of generations in accounts is formulated as follows.
-</p>
-
-<div class='constraint' id='generation-uniqueness'>Given an entity denoted by <span class="name">e</span>, two activities denoted by <span class="name">a1</span> and <span
-class="name">a2</span>, two time instants  <span class="name">t1</span> and <span
-class="name">t2</span>, and two sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
-<span class='conditional'>if</span> <span class="name">wasGeneratedBy(id1, e, a1, t1, attrs1)</span> and <span class="name">wasGeneratedBy(id2, e, a2, t2, attrs2)</span> exist in the scope of a given
-account,
-<span class='conditional'>then</span> <span class="name">id1</span>=<span class="name">id2</span>, <span class="name">a1</span>=<span class="name">a2</span>, <span class="name">t1</span>=<span class="name">t2</span>  and <span class="name">attrs1</span>=<span class="name">attrs2</span>.
-</div> 
-
-
-
-
-
-<div class='note'>TODO: Move this back to the place where it is first referenced.</div>
-<p>A further inference is permitted from derivations with an explicit activity and no usage: </p>
-<div class='inference' id='derivation-use'>
-<p>Given an activity <span class="name">a</span>, entities  denoted by <span class="name">e1</span> and <span class="name">e2</span>, and  sets of attribute-value
-pairs <span class="name">dAttrs</span>, <span class="name">gAttrs</span>,
-<span class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1, a, dAttrs)</span> and <span class="name">wasGeneratedBy(e2,a,-,gAttrs)</span> hold, <span
-class='conditional'>then</span> <span class="name">used(a,e1,-,uAttrs)</span> also holds
-for some set of attribute-value pairs <span class="name">uAttrs</span>.
-</div>
-<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity in a given account
-(see <a href="#generation-uniqueness">generation-uniqueness</a>). Hence,  this activity is also the one referred to by the usage of <span class="name">e1</span>. 
-</p>
-
-
-<p>We note that the converse inference, does not hold.
-From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(a,e1,-)</span>, one cannot
-derive <span class="name">wasGeneratedBy(e2,a,-)</span> because identifier <span class="name">e1</span> may occur in usages performed by many activities, which may have not generated the entity denoted by <span class="name">e2</span>.</p>
-
-
-<p>
-An account is said to be structurally well-formed if
-it satisfies the constraint  <a href="#generation-uniqueness">generation-uniqueness</a>. If an account is structurally well-formed, it supports the inference <a
-href="#derivation-use">derivation-use</a>.</p>
-
-<div class='note'>
-  Since we are not specifying ways to take the union of two accounts,
-  we may drop this discussion
-  </div>
-<p> Taking the union of two accounts is another account, 
-formed by the union of the descriptions they respectively contain.  We note that the resulting union may or may not invalidate some constraints:
-<ul>
-<li> Two entity descriptions with a same identifier but different sets of attributes exist in each original account may invalidate <a href="#unique-description-in-account">unique-description-in-account</a> in the union, unless some form of description merging or renaming (as per <a href="#merge-with-rename">Example</a>) occurs.
-<li> Structurally well-formed
-accounts are not
-closed under union because the
-constraint <a href="#generation-uniqueness">generation-uniqueness</a> may no
-longer be satisfied in the resulting union.  </li>
-</ul>
-<p>How to reconcile such accounts is beyond the scope of this specification.</p>
-
-<!--
-Indeed, let us reconsider example <a href="#account-example-1">account-example-1</a>, and let us define another account record as follows.</p>
-
-<div class="anexample">
-<pre class="codeexample">
-account(ex:acc2,
-        http://example.org/asserter2, 
-          entity(e0, [ prov:type="File", ex:path="/shared/crime.txt", ex:creator="Alice" ])
-          ...
-          activity(a1,t1,,[prov:type="createFile"])
-          ...
-          wasGeneratedBy(e0,a1,[ex:fct="create"])     
-          ... )
-</pre>
-<p>with identifier <span class="name">ex:acc2</span>, containing assertions by asserter by <span class="name">http://example.org/asserter2</span> stating that the entity represented by
-entity record identified by <span class="name">e0</span> was generated by an activity represented by activity record identified by <span class="name">a1</span> instead of <span
-class="name">a0</span> in the previous account <span class="name">ex:acc0</span>.  If accounts <span class="name">ex:acc0</span> and <span class="name">ex:acc2</span> are merged together,
-the resulting set of records violates <a href="#generation-uniqueness">generation-uniqueness</a> if the two activities <span class="name">a0</span> and <span class="name">a1</span> are
-distinct.</p>
-</div>
--->
-
-<!--
-<div class="note">
-Can the semantics characterize better what can be achieved with structurally well-formed accounts?
-</div>
-
-
-<div class="note" id="note-related-to-issue-105">
-Satya discussed the example of a sculpture, whose hand and leg are sculpted independently by two different sculptors. He suggested that the sculpture is generated by two distinct activities.
-This section explains that it is not the case.  The example can be formulated as follows.
-
-<p><a href="examples/sculpture.pn">Sculpture example in PROV-N</a></p>
-
-<p><a href="examples/sculpture.png">Sculpture example image</a></p>
-
-<p>
-We see that ex:s_3 (the sculpture in its final state) was derived from ex:l_2 (containment) which was generated by ex:a2. However, ex:s_3 is not directly generated by ex:a2.  We may want to
-consider an abbreviation for this: wasGeneratedBy*(ex:s_3,ex:a2).</p>
-</div>
-
--->
-
-</section>
-
-
-<section id="collection-constraints">
-<h3>PROV-DM Collection Constraints</h3>
-
-<p>Membership is a convenience notation, since it can be expressed in terms of an insertion into some collection. The membership definition is formalized by constraint <a href="#membership-as-insertion">membership-as-insertion</a>.</p>
-
-<div class='definition' id='membership-as-insertion'>
- <span class="name">memberOf(c, {(k1, v1), ...})</span> holds
-<span class='conditional'>if and only if</span> there exists a collection <span class="name">c0</span>, such that
-<span class="name">derivedByInsertionFrom(c, c0, {(k1, v1), ...})</span>.
-</div>
-
-<p>A collection may be obtained by insertion or removal, or said to satisfy the membership relation.
-To provide an interpretation of collections, PROV-DM 
- restricts one collection to be involved in a single derivation by insertion or removal, or to one membership relation.
-PROV-DM does not provide an interpretation for descriptions that consist of two (or more) insertion, removal, membership relations that result in the same collection.</p>
-
-
-
-<p>The following constraint ensures unique derivation.</p>
-
-
-<div class='note'> The following constraint is unclear.</div>
-<div class='constraint' id='collection-unique-derivation'>
-A collection MUST NOT be derived through multiple insertions, removal,
-  or membership relations. 
-</div>
-
-<div class="anexample">
-Consider the following descriptions about three collections.
-  <pre class="codeexample">
-entity(c1, [prov:type="prov:Collection"  %% xsd:QName])
-entity(c2, [prov:type="prov:Collection"  %% xsd:QName])
-entity(c3, [prov:type="prov:Collection"  %% xsd:QName])
-
-
-derivedByInsertionFrom(c3, c1, {("k1", e1), ("k2", e2)})
-derivedByInsertionFrom(c3, c2, {("k3", e3)})
-</pre>
-<p>There is no interpretation for such descriptions since <span class="name">c3</span> is derived multiple times by insertion.</p>
-</div>
-
-
-<div class="anexample">
-<p>As a particular case, collection <span class="name">c</span> is derived multiple times from the same <span class="name">c1</span>. </p>
-<pre class="codeexample">
-derivedByInsertionFrom(id1, c, c1, {("k1", e1), ("k2", e2)})
-derivedByInsertionFrom(id2, c, c1, {("k3", e3), ("k4", e4)})
-</pre>
-<p>The interpretation of such descriptions is also unspecified. </p>
-<p>To describe the insertion of the 4 key-entity pairs, one would instead write:</p>
-<pre class="codeexample">
-derivedByInsertionFrom(id1, c, c1, {("k1", e1), ("k2", e2), ("k3", e3), ("k4", e4)})
-</pre>  
-</div>
-
-The same is true for any combination of insertions, removals, and membership relations:
-<div class="anexample">
-<p>The following descriptions</p>
-<pre class="codeexample">
-derivedByInsertionFrom(c, c1, {("k1", e1)})
-derivedByRemovalFrom(c, c2, {"k2"})
-</pre>
-have no interpretation.
-Nor have the following:
-<pre class="codeexample">
-derivedByInsertionFrom(c, c1, {("k1", e1)})
-memberOf(c, {"k2"}).
-</pre>
-</div>
-
-
-
-<!--
-<section id="Collection-branching">
--->
-<section id="collection-branching">
-<h4>Collection branching</h4>
-
-It is allowed to have multiple derivations from a single root collection, as long as the resulting entities are distinct, as shown in the following example.
-
-<div class="anexample">
-<pre class="codeexample">
-entity(c0, [prov:type="prov:EmptyCollection" %% xsd:QName])    // c0 is an empty collection
-entity(c1, [prov:type="prov:Collection" %% xsd:QName])
-entity(c2, [prov:type="prov:Collection" %% xsd:QName])
-entity(c3, [prov:type="prov:Collection" %% xsd:QName])
-entity(e1)
-entity(e2)
-entity(e3)
-
-derivedByInsertionFrom(c1, c0, {("k1", e1)})      
-derivedByInsertionFrom(c2, c0, {("k2", e2)})       
-derivedByInsertionFrom(c3, c1, {("k3", e3)})       
-</pre>
-From this set of descriptions, we conclude:
-<pre class="codeexample">
-  c1 = { ("k1", e1) }
-  c2 = { ("k2", e2) }
-  c3 = { ("k1", e1), ("k3", e3)}
-</pre>
-</div>
-
-</section>
-
-  
-
-<section id="collections-and-derivation">
-
-  
-<h4>Collections and Weaker Derivation Relation</h4>
-
-<p>The state of a collection is only known to the extent that a chain of derivations starting from an empty collection can be found. Since a set of descriptions regarding a collection's evolution may be incomplete, so is the reconstructed state obtained by querying those descriptions. In general, all descriptions reflect partial knowledge regarding a sequence of data transformation events. In the particular case of collection evolution, in which some of the state changes may have been missed, the more generic  <a href="#Derivation-Relation">derivation</a> relation should be used to signal that some updates may have occurred, which cannot be expressed as insertions or removals. The following  example illustrates this.</p>
-
-<!--
-<div class="anexample">
-<pre class="codeexample">
-entity(c, [prov:type="prov:Collection" %% xsd:QName])    // c is a collection, possibly not empty
-entity(c1, [prov:type="prov:Collection" %% xsd:QName])    
-entity(c2, [prov:type="prov:Collection" %% xsd:QName])    
-entity(e1)
-entity(e2)
-
-derivedByInsertionFrom(c1, c,  {("k1", e1)})       
-derivedByInsertionFrom(c2, c1, {("k2", e2)})    
-</pre>
-From this set of descriptions, we conclude:
-<ul>
-<li> <span class="name">c1</span> includes <span class="name">("k1", e1)</span> but may contain additional unknown pairs
-<li> <span class="name">c2</span> includes <span class="name">("k1", e1), ("k2", e2)</span> (and possibly more pairs), where <span class="name">e2</span> is a collection with unknown state
-</pre>
- </div>
---> 
-
- 
- <div class="anexample">
-In the example, the state of <span class="name">c2</span> is only partially known because the collection is constructed from partially known other collections.
- <pre class="codeexample">
-entity(c0, [prov:type="prov:EmptyCollection" %% xsd:QName])    // c0 is an empty collection
-entity(c1, [prov:type="prov:Collection" %% xsd:QName])    
-entity(c2, [prov:type="prov:Collection" %% xsd:QName])    
-entity(c3, [prov:type="prov:Collection" %% xsd:QName])    
-entity(e1)
-entity(e2)
-
-derivedByInsertionFrom(c1, c0, {("k1", e1)})       
-wasDerivedFrom(c2, c1)                       
-derivedByInsertionFrom(c3, c2, {("k2", e2)})       
- </pre>
-From this set of descriptions, we conclude:
-<ul>
-<li>    <span class="name">c1 = { ("k1", e1) }</span>
-<li>    <span class="name">c2</span> is somehow derived from <span class="name">c1</span>, but the precise sequence of updates is unknown
-<li>    <span class="name">c3</span>  includes  <span class="name">("k2", e2)</span> but the earlier "gap" leaves uncertainty regarding  <span class="name">("k1", e1)</span>  (it may have been removed) or any other pair that may have been added as part of the derivation activities.
-</ul>
- </div>
-
-</section>
-
-
-<div class='note'>
-  Do the insertion/removal derivation steps imply wasDerivedFrom,
-  wasVersionOf, alternateOf?
-  </div>
- 
-</section>  <!-- end of collections -->
-
-
-<!--
-<section id="resource-section">
-<h2>Resources, URIs, Entities, Identifiers, and Scope</h2> 
-
-<p>This specification  introduces the  notion of an identifiable entity in the world. In PROV-DM, an entity record is a representation of such an identifiable entity. An entity record
-includes an identifier identifying this entity.  Identifiers are qualified names, which can be mapped to IRIs.  </p>
-
-<p>The term 'resource' is used in a general sense
-      for whatever might be identified by a URI [[!RFC3986]].  On the Web, a URI denotes a resource, without any expectation that the resource is accessed. </p>
-
-<p>The purpose of this section is to clarify the relationship between resource and the notions of entity and  entity record. </p>  
-
-<p>In the context of PROV-DM, a resource is just a thing in the world. One may take multiple perspectives on such a thing and its situation in the world, fixing some its aspects.</p>
-
-<p> We refer to the <a href="#a-report-example">example</a> of section <a href="#conceptualization">2.1</a> for a resource (at some URL) and three different perspectives, referred to as
-entities.  Three different entity records can be expressed for this report, which in the PROV-N sample below, are expressed within a same account.
-</p>
-
-<pre>
-container
-prefix app http://example.org/app/
-prefix cr  http://example.org/crime/
-
-   account(acc1,
-           http://example.org/asserter1,
-
-           entity(app:0, [ prov:type="Document", cr:path="http://example.org/crime.txt" ])
-           entity(app:1, [ prov:type="Document", cr:path="http://example.org/crime.txt", cr:version="2.1", cr:content="...", cr:date="2011-10-07" ])
-           entity(app:2, [ prov:type="Document", cr:author="John" ])
-        ...)
-endContainer
-</pre>
-
-<p>Each entity record contains an identifier that is unique in
-account <span class="name">acc1</span>, and therefore locally
-identifies the entity record it is contained in.  In this example,
-three identifiers were minted.</p>
-
-<p>Given that the report is a resource denoted by the URI <span class="name">http://example.org/crime.txt</span>, we could simply use this URI as the identifier of an entity. This would
-avoid us minting new URIs.  Hence, the report URI would play a double role: as a URI it denotes a resource accessible at that URI, and as an identifier in a PROV-DM record, it helps identify
-a specific characterization of this report. A given identifier occurring in an entity record must be unique within the scope of an account. Hence, below, all entities records have been given
-the same identifier but appear in the scope of different accounts, so as to satisfy  <a href="#identifiable-term-in-account">identifiable-term-in-account</a>.</p>
-
-<pre>
-container 
-prefix app http://example.org/
-prefix cr  http://example.org/crime/
-
-   account(acc2,
-           http://example.org/asserter1,
-
-           entity(app:crime.txt, [ prov:type="Document", cr:path="http://example.org/crime.txt" ])
-           ...)
-
-   account(acc3,
-           http://example.org/asserter1,
-
-           entity(app:crime.txt, [ prov:type="Document", cr:path="http://example.org/crime.txt", cr:version="2.1", cr:content="...", cr:date="2011-10-07" ])
-           ...)
-
-   account(acc4,
-           http://example.org/asserter1,
-           entity(app:crime.txt, [ prov:type="Document", cr:author="John" ])
-           ...)
-endContainer
-</pre>
-
-<p>In this case, the qualified name  <span class="name">app:crime.txt</span> maps to URI <span class="name">http://example.org/crime.txt</span> still denotes the same resource; however, the
-perspectives we take about that resource are expressed by multiple entity records, happening to all contain the same identifier but in different accounts. </p>
-
-<p> Alternatively, if we need to assert the existence of two different perspectives on the report within the same account, then alternate identifiers MUST be used, one of them being allowed
-to be the resource URI.</p>
-
-<pre>
-container 
- prefix app  http://example.org/
- prefix app2 http://example.org/app/
- prefix cr   http://example.org/crime/
-
-   account(acc5,
-           http://example.org/asserter1,
-
-           entity(app:crime.txt, [ prov:type="Document", cr:path="http://example.org/crime.txt" ])
-           entity(app2:1, [ prov:type="Document", cr:path="http://example.org/crime.txt", cr:version="2.1", cr:content="...", cr:date="2011-10-07" ])
-
-           ...)
-endContainer
-
-</pre>
-
-
-</section>                 
-
--->
-
-<!--
-<li>For use, generation, and derivation event, the first argument is the 'effect' (i.e. most recent item) and the second argument is the 'cause' (i.e. least recent item). This order is
-compatible with the temporal layout of the graphical notation.
--->
-
-<!--
-<section id="refining-provenance-descriptions">
-<h3>Refining Provenance Descriptions</h3>
-
-<div class='note'>Purely tentative</div>
-
-<p>In this section, we successively review refined provenance descriptions, and examine their meaning, in light of the constraints introduced in this specification. </p>
-
-
-<ol> 
-<li>First, let us consider a small set of three descriptions, including an entity, an agent, and an attribution relation.
-<pre>
-entity(tr:prov-dm)
-agent(w3:Consortium)
-wasAttributedTo(tr:prov-dm,w3:Consortium)
-</pre>
-<p>The entity denoted by <span class="name">tr:prov-dm</span> does not contain any attribute besides its identifier.  Without any further detail, this entity is simply the resource denoted by <span class="name">tr:prov-dm</span>, whatever its state over time. This resource has multiple versions including <span class="name">tr:WD-prov-dm-20111215</span> and <span class="name">tr:WD-prov-dm-20111018</span>.
-Likewise, the second line simply is a description for a resource denoted by <span class="name">w3:Consortium</span>, nothing less, nothing more.</p>
-<p>The third description should be interpreted as: whatever changes entity <span class="name">tr:prov-dm</span> may have gone through, it is always attributed to the <span class="name">w3:Consortium</span> agent.</p>
-</li>
-
-
-<li>Second, the descriptions are bundled up as an account with name <span class="name">ex:acc1</span>:
-<pre>
-entity(tr:prov-dm)
-agent(ex:Simon)
-wasAttributedTo(tr:prov-dm,ex:Simon)
-</pre>
-and provenance details are available for <span class="name">ex:acc1</span>, namely the generation time for the provenance. 
-<pre>
-entity(ex:acc1, [prov:type="AccountEntity"])
-wasGeneratedBy(ex:acc1,,2011-12-15T12:00:00)
-</pre>
-<div class='note'>
-What is the meaning here?  Is it any different? Are stating anything about newer version of tr:prov-dm that occur after 2011-12-15T12:00:00?
-</div>
-
-<li> A generation event for <span class="name">tr:prov-dm</span> is provided.
-<pre>
-entity(tr:prov-dm)
-agent(ex:Simon)
-wasGeneratedBy(tr:prov-dm,,2011-12-15T12:00:00)
-wasAttributedTo(tr:prov-dm,ex:Simon)
-</pre>
-<div class='note'>
-What is the meaning here?  that only the version that was created by this event is attributed to ex:Simon, but not previous ones. This means that it is not specfied whether he was an author in anterior versions.
-</div>
-
-</li>
-
-
-<li> A invalidation event for <span class="name">tr:prov-dm</span> is provided.
-<pre>
-entity(tr:prov-dm)
-agent(ex:Simon)
-wasGeneratedBy(tr:prov-dm,,2011-12-15T12:00:00)
-wasDestroyedBy(tr:prov-dm,,2012-02-02T12:00:00)
-wasAttributedTo(tr:prov-dm,ex:Simon)
-</pre>
-<div class='note'> 
-Speculative, since we have not defined the invalidation event (yet?.
-What is the meaning here?  that only the versions that existed during this <a title="characterization interval">characterization interval</a> were attributed to ex:Simon.
-</div>
-</li>
-
-</ol>
-
-</section>
-
--->
-
-<!--
-<section>
-<h3>Stuff to Keep, Maybe?</h3>
-
-
-
-
-<li id='attribute-occurrence-in-entity-record'>The attributes
-occurring in an entity record MUST be declared in the namespace
-referred to by their prefix according to
-<a href="#term-attribute">Section term-attribute</a>. Furthermore,
-for each attribute, a namespace MAY also declare the number of
-occurrences the entity may have in a list of attributes. An entity record is
-valid if the number of occurrences of any of its attributes is
-compatible with this attribute's declaration it its namespace. This
-property applies to all types of records, and is referred to
-as <a>attribute occurrence validity</a>.</li>
-
-
-</section>
--->
+
+
 
 <section class="appendix"> 
       <h2>Acknowledgements</h2>