* updated prov-constraints
authorJames Cheney <jcheney@inf.ed.ac.uk>
Tue, 20 Nov 2012 15:10:55 +0000
changeset 4857 2f27ed3b7135
parent 4856 de8cda493917
child 4858 29db7fe3f266
* updated prov-constraints
model/diff-c.html
model/prov-constraints.html
--- a/model/diff-c.html	Tue Nov 20 10:06:12 2012 -0500
+++ b/model/diff-c.html	Tue Nov 20 15:10:55 2012 +0000
@@ -23,7 +23,7 @@
     
 
      
-  <style type="text/css">
+  <span class="delete">
 /*****************************************************************
  * ReSpec CSS
  * Robin Berjon (robin at berjon dot com)
@@ -486,7 +486,7 @@
 /* other */
 pre.sh_sourceCode .sh_section { color: black; font-weight: bold; }
 pre.sh_sourceCode .sh_paren { color: red; }
-pre.sh_sourceCode .sh_attribute { color: #006400; }<span class="delete">
+pre.sh_sourceCode .sh_attribute { color: #006400; }
 
 
 /* --- EDITORIAL NOTES --- */
@@ -1005,10 +1005,20 @@
 	padding: 2px;
 	border-style: solid;
 	border-color: gray;
-}</span>
-
-</style><link href="./extra.css" rel="stylesheet" type="text/css" charset="utf-8"><link href="http://www.w3.org/StyleSheets/TR/W3C-ED" rel="stylesheet" type="text/css" charset="utf-8"></head> 
-  <body style="display: inherit; "><div class="head"><p><a href="http://www.w3.org/"><img width="72" height="48" src="http://www.w3.org/Icons/w3c_home" alt="W3C"></a></p><h1 class="title" id="title">Constraints of the Provenance Data Model</h1><h2 id="subtitle"><a href="diff-c.html"><span class="insert">Changes</span></a><span class="insert"> since Last Call Working Draft  (LC)</span></h2><h2 id="w3c-editor-s-draft-01-november-2012"><acronym title="World Wide Web Consortium">W3C</acronym> <span class="delete">Working</span><span class="insert">Editor's</span> Draft <span class="delete">11 September</span><span class="insert">01 November</span> 2012</h2><dl><dt>This version:</dt><dd><span class="delete">http://www.w3.org/TR/2012/WD-prov-constraints-20120911/</span><a href="http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html"><span class="insert">http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html</span></a></dd><dt>Latest published version:</dt><dd><a href="http://www.w3.org/TR/prov-constraints/">http://www.w3.org/TR/prov-constraints/</a></dd><dt>Latest editor's draft:</dt><dd><a href="http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html">http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html</a></dd><dt>Previous version:</dt><dd><a href="http://www.w3.org/TR/2012/WD-prov-constraints-20120503/">http://www.w3.org/TR/2012/WD-prov-constraints-20120503/</a><span class="delete"> (</span><span class="delete">color-coded diffs</span><span class="delete">)</span></dd><dt>Editors:</dt><dd><a href="http://homepages.inf.ed.ac.uk/jcheney">James Cheney</a>, University of Edinburgh</dd>
+}
+
+</span>
+
+     
+     
+    
+
+    
+    
+
+     
+  <link href="http://dev.w3.org/2009/dap/ReSpec.js/css/respec.css" rel="stylesheet" type="text/css" charset="utf-8"><link href="./extra.css" rel="stylesheet" type="text/css" charset="utf-8"><link href="http://www.w3.org/StyleSheets/TR/W3C-CR" rel="stylesheet" type="text/css" charset="utf-8"></head> 
+  <body style="display: inherit;"><div class="head"><p><a href="http://www.w3.org/"><img width="72" height="48" src="http://www.w3.org/Icons/w3c_home" alt="W3C"></a></p><h1 class="title" id="title">Constraints of the Provenance Data Model</h1><h2 id="subtitle"><a href="diff-c.html"><span class="insert">Changes</span></a><span class="insert"> since Last Call Working Draft  (LC)</span></h2><h2 id="w3c-candidate-recommendation-11-december-2012"><acronym title="World Wide Web Consortium">W3C</acronym> <span class="delete">Working Draft</span><span class="insert">Candidate Recommendation</span> 11 <span class="delete">September</span><span class="insert">December</span> 2012</h2><dl><dt>This version:</dt><dd><span class="delete">http://www.w3.org/TR/2012/WD-prov-constraints-20120911/</span><a href="http://www.w3.org/TR/2012/CR-prov-constraints-20121211/"><span class="insert">http://www.w3.org/TR/2012/CR-prov-constraints-20121211/</span></a></dd><dt>Latest published version:</dt><dd><a href="http://www.w3.org/TR/prov-constraints/">http://www.w3.org/TR/prov-constraints/</a></dd><dt>Latest editor's draft:</dt><dd><a href="http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html">http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html</a></dd><dt>Previous version:</dt><dd><span class="delete">http://www.w3.org/TR/2012/WD-prov-constraints-20120503/</span><span class="delete"> (</span><span class="delete">color-coded diffs</span><span class="delete">)</span><a href="http://www.w3.org/TR/2012/WD-prov-constraints-20120911/"><span class="insert">http://www.w3.org/TR/2012/WD-prov-constraints-20120911/</span></a></dd><dt>Editors:</dt><dd><a href="http://homepages.inf.ed.ac.uk/jcheney">James Cheney</a>, University of Edinburgh</dd>
 <dd><a href="http://www.cs.ncl.ac.uk/people/Paolo.Missier">Paolo Missier</a>, Newcastle University</dd>
 <dd><a href="http://www.ecs.soton.ac.uk/~lavm/">Luc Moreau</a>, University of Southampton</dd>
 <dt>Author:</dt><dd><a href="http://users.ugent.be/~tdenies/">Tom De Nies</a>, IBBT - Ghent University</dd>
@@ -1044,49 +1054,58 @@
 instance together with zero or more bundles).</p>
 
 </div><div id="sotd" class="introductory section"><h2>Status of This Document</h2><p><em>This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current <acronym title="World Wide Web Consortium">W3C</acronym> publications and the latest revision of this technical report can be found in the <a href="http://www.w3.org/TR/"><acronym title="World Wide Web Consortium">W3C</acronym> technical reports index</a> at http://www.w3.org/TR/.</em></p>
-<h4 id="last-call">Last Call</h4>
-<p>This is the second public release of the PROV-CONSTRAINTS document. 
-This is a Last Call Working Draft. The design is not expected to change significantly, going forward, and now is the key time for external review.</p>
-
-<p>This specification identifies  <a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">features at
-risk</a> related to the at-risk Mention feature of [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-DM">PROV-DM</a></cite>]:
-<a class="rule-text" href="#mention-specialization-inference_text"><span>Inference 22 (mention-specialization-inference)</span></a> and
-<a class="rule-text" href="#unique-mention_text"><span>Constraint 31 (unique-mention)</span></a>.
-These might be removed from PROV-CONSTRAINTS.</p>
-
-<h4 id="prov-family-of-specifications">PROV Family of Specifications</h4>
+<span class="delete">Last Call</span><h4 id="prov-family-of-documents"><span class="insert">PROV Family of Documents</span></h4>
+This <span class="insert">document </span>is <span class="delete">the second public release of the PROV-CONSTRAINTS document. 
+This is</span><span class="insert">part of the PROV family of documents,</span> a <span class="delete">Last Call Working Draft. The design is not expected</span><span class="insert">set of documents defining various aspects that are necessary</span> to <span class="delete">change significantly, going forward, and now is the key time</span><span class="insert">achieve the vision of inter-operable
+interchange of provenance information in heterogeneous environments such as the Web.  These documents are:
+</span><ul>
+<li> <a href="http://www.w3.org/TR/2012/WD-prov-overview-20121211/"><span class="insert">PROV-OVERVIEW</span></a><span class="insert"> (Note), an overview of the PROV family of documents [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-OVERVIEW"><span class="insert">PROV-OVERVIEW</span></a></cite><span class="insert">];</span></li>
+<li> <a href="http://www.w3.org/TR/2012/WD-prov-primer-20121211/"><span class="insert">PROV-PRIMER</span></a><span class="insert"> (Note), a primer</span> for <span class="delete">external review.</span>
+
+<span class="delete">This specification identifies  </span><span class="delete">features at
+risk</span><span class="delete"> related</span><span class="insert">the PROV data model [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-PRIMER"><span class="insert">PROV-PRIMER</span></a></cite><span class="insert">];</span></li>
+<li> <a href="http://www.w3.org/TR/2012/CR-prov-o-20121211/"><span class="insert">PROV-O</span></a><span class="insert"> (Recommendation), the PROV ontology, an OWL2 ontology allowing the mapping of PROV</span> to <span class="delete">the at-risk Mention feature of</span><span class="insert">RDF [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-O"><span class="insert">PROV-O</span></a></cite><span class="insert">];</span></li>
+<li> <a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/"><span class="insert">PROV-DM</span></a><span class="insert"> (Recommendation), the PROV data model for provenance</span> [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-DM">PROV-DM</a></cite><span class="delete">]:
+</span><span class="delete">Inference 22 (mention-specialization-inference)</span><span class="delete"> and
+</span><span class="delete">Constraint 31 (unique-mention)</span><span class="delete">.
+These might be removed from PROV-CONSTRAINTS.</span>
+
+<span class="insert">];</span></li>
+<li> <a href="http://www.w3.org/TR/2012/CR-prov-n-20121211/"><span class="insert">PROV-N</span></a><span class="insert"> (Recommendation), a notation for provenance aimed at human consumption [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-N"><span class="insert">PROV-N</span></a></cite><span class="insert">];</span></li>
+<li> <a href="http://www.w3.org/TR/2012/CR-prov-constraints-20121211/"><span class="insert">PROV-CONSTRAINTS</span></a><span class="insert">
+(Recommendation), a set of constraints applying to the </span>PROV <span class="delete">Family of Specifications</span><span class="delete">
 This document is part of the PROV family of specifications, a set of specifications defining various aspects that are necessary to achieve the vision of inter-operable
 interchange of provenance information in heterogeneous environments such as the Web.  The specifications are:
+</span>
+ <span class="delete">PROV-DM</span><span class="delete">, the PROV </span>data model<span class="delete"> for provenance;</span>
+ <span class="delete">PROV-CONSTRAINTS</span><span class="delete">, a set of constraints applying to the PROV data model  </span>
+(this document);</li>
+<li> <span class="delete">PROV-N</span><span class="delete">, a notation</span><a href="http://www.w3.org/TR/2012/WD-prov-aq-20120619/"><span class="insert">PROV-AQ</span></a><span class="insert"> (Note), the mechanisms</span> for <span class="insert">accessing and querying </span>provenance <span class="delete">aimed at human consumption;</span><span class="insert">[</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-AQ"><span class="insert">PROV-AQ</span></a></cite><span class="insert">]; </span></li>
+<li> <span class="delete">PROV-O</span><span class="delete">,</span><a href="http://www.w3.org/TR/2012/WD-prov-xml-20121211/"><span class="insert">PROV-XML</span></a><span class="insert"> (Note),  an XML schema for</span> the PROV <span class="delete">ontology,</span><span class="insert">data model [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-XML"><span class="insert">PROV-XML</span></a></cite><span class="insert">].</span></li>
+
+</ul>
+<h4 id="how-to-read-the-prov-family-of-documentation"><span class="insert">How to read the PROV Family of Documentation</span></h4>
 <ul>
-<li> <a href="http://www.w3.org/TR/prov-dm/">PROV-DM</a>, the PROV data model for provenance;</li>
-<li> <a href="http://www.w3.org/TR/prov-constraints/">PROV-CONSTRAINTS</a>, a set of constraints applying to the PROV data model  (this document);</li>
-<li> <a href="http://www.w3.org/TR/prov-n/">PROV-N</a>, a notation for provenance aimed at human consumption;</li>
-<li> <a href="http://www.w3.org/TR/prov-o/">PROV-O</a>, the PROV ontology, an OWL2 ontology allowing the mapping of PROV to RDF;</li>
-<li> <a href="http://www.w3.org/TR/prov-aq/">PROV-AQ</a>, the mechanisms for accessing and querying provenance; </li>
-<li> <a href="http://www.w3.org/TR/prov-primer/">PROV-PRIMER</a>, a primer for the PROV data model.</li>
-</ul>
-<h4 id="how-to-read-the-prov-family-of-specifications">How to read the PROV Family of Specifications</h4>
-<ul>
-<li>The primer is the entry point to PROV offering an introduction to the provenance model.</li>
-<li>The Linked Data and Semantic Web community should focus on PROV-O
+<li><span class="insert">The primer is the entry point to PROV offering</span> an <span class="delete">OWL2 ontology allowing the mapping of PROV</span><span class="insert">introduction</span> to <span class="delete">RDF;</span>
+ <span class="delete">PROV-AQ</span><span class="delete">, the mechanisms for accessing and querying provenance; </span>
+ <span class="delete">PROV-PRIMER</span><span class="delete">, a primer for the PROV data</span><span class="insert">the provenance</span> model.</li>
+
+<span class="delete">How to read the PROV Family of Specifications</span>
+
+<li>The <span class="delete">primer is the entry point</span><span class="insert">Linked Data and Semantic Web community should focus on PROV-O defining PROV classes and properties specified in an OWL2 ontology. For further details, PROV-DM and PROV-CONSTRAINTS specify the constraints applicable</span> to <span class="delete">PROV offering an introduction to the provenance model.</span>
+<span class="delete">The Linked Data and Semantic Web community should focus on PROV-O
 defining PROV classes and properties specified in an OWL2
 ontology. For further details, PROV-DM and PROV-CONSTRAINTS specify
-the constraints applicable to the data model, and its interpretation.
-
-  
-</li>
+the constraints applicable to </span>the data model, and its interpretation.
+
+ </li>
 <li>Developers seeking to retrieve or publish provenance should focus on PROV-AQ.</li>
 <li>Readers seeking to implement other PROV serializations
-should focus on PROV-DM and PROV-CONSTRAINTS.  PROV-O and PROV-N offer 
-examples of mapping to RDF and text, respectively.</li>
-<li><span class="insert">[</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-SEM"><span class="insert">PROV-SEM</span></a></cite><span class="insert">] provides a mathematical semantics and a collection of
-axioms that provide a (non-normative, but equivalent) declarative specification, aimed
-at readers with a mathematical logic or formal background.  This can
-serve as a starting point for alternative implementations. </span></li>
+should focus on PROV-DM and PROV-CONSTRAINTS.  PROV-O and PROV-N offer examples of mapping to RDF and text, respectively.</li>
 </ul>
 
-<p>This document was published by the <a href="http://www.w3.org/2011/prov/">Provenance Working Group</a> as <span class="delete">a Last Call Working</span><span class="insert">an Editor's</span> Draft.<span class="delete"> This document is intended to become a </span><span class="delete">W3C</span><span class="delete"> Recommendation.</span> If you wish to make comments regarding this document, please send them to <a href="mailto:public-prov-comments@w3.org">public-prov-comments@w3.org</a> (<a href="mailto:public-prov-comments-request@w3.org?subject=subscribe">subscribe</a>, <a href="http://lists.w3.org/Archives/Public/public-prov-comments/">archives</a>).<span class="delete"> The Last Call period ends 10 October 2012.</span> All feedback is welcome.</p><p>Publication as <span class="delete">a Working</span><span class="insert">an Editor's</span> Draft does not imply endorsement by the <acronym title="World Wide Web Consortium">W3C</acronym> Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.<span class="delete">This is a Last Call Working Draft and thus the Working Group has determined that this document has satisfied the relevant technical requirements and is sufficiently stable to advance through the Technical Recommendation process.</span></p><p>This document was produced by a group operating under the <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/">5 February 2004 <acronym title="World Wide Web Consortium">W3C</acronym> Patent Policy</a>. <acronym title="World Wide Web Consortium">W3C</acronym> maintains a <a href="http://www.w3.org/2004/01/pp-impl/46974/status" rel="disclosure">public list of any patent disclosures</a> made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/#def-essential">Essential Claim(s)</a> must disclose the information in accordance with <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/#sec-Disclosure">section 6 of the <acronym title="World Wide Web Consortium">W3C</acronym> Patent Policy</a>.</p></div><div id="toc" class="section"><h2 class="introductory">Table of Contents</h2><ul class="toc"><li class="tocline"><a href="#introduction" class="tocxref"><span class="secno">1. </span>Introduction<br>
-</a><ul class="toc"><li class="tocline"><a href="#conventions" class="tocxref"><span class="secno">1.1 </span>Conventions</a></li><li class="tocline"><a href="#purpose" class="tocxref"><span class="secno">1.2 </span>Purpose of this document</a></li><li class="tocline"><a href="#structure-of-this-document" class="tocxref"><span class="secno">1.3 </span>Structure of this document</a></li><li class="tocline"><a href="#audience" class="tocxref"><span class="secno">1.4 </span> Audience </a></li></ul></li><li class="tocline"><a href="#rationale" class="tocxref"><span class="secno">2. </span>Rationale</a><ul class="toc"><li class="tocline"><a href="#entities--activities-and-agents" class="tocxref"><span class="secno">2.1 </span>Entities, Activities and Agents</a></li><li class="tocline"><a href="#events" class="tocxref"><span class="secno">2.2 </span>Events</a></li><li class="tocline"><a href="#typing-section" class="tocxref"><span class="secno">2.3 </span>Types</a></li><li class="tocline"><a href="#validation-process-overview-1" class="tocxref"><span class="secno">2.4 </span>Validation Process Overview</a></li><li class="tocline"><a href="#summary-of-inferences-and-constraints" class="tocxref"><span class="secno">2.5 </span>Summary of inferences and constraints</a></li></ul></li><li class="tocline"><a href="#compliance" class="tocxref"><span class="secno">3. </span>Compliance with this document</a></li><li class="tocline"><a href="#inferences" class="tocxref"><span class="secno">4. </span>Definitions and Inferences</a><ul class="toc"><li class="tocline"><a href="#optional-identifiers-and-attributes" class="tocxref"><span class="secno">4.1 </span>Optional Identifiers and Attributes</a></li><li class="tocline"><a href="#entities-and-activities" class="tocxref"><span class="secno">4.2 </span>Entities and Activities</a></li><li class="tocline"><a href="#derivations" class="tocxref"><span class="secno">4.3 </span>Derivations</a></li><li class="tocline"><a href="#agents" class="tocxref"><span class="secno">4.4 </span>Agents</a></li><li class="tocline"><a href="#alternate-and-specialized-entities" class="tocxref"><span class="secno">4.5 </span>Alternate and Specialized Entities</a></li></ul></li><li class="tocline"><a href="#constraints" class="tocxref"><span class="secno">5. </span>Constraints</a><ul class="toc"><li class="tocline"><a href="#uniqueness-constraints" class="tocxref"><span class="secno">5.1 </span>Uniqueness Constraints</a></li><li class="tocline"><a href="#event-ordering-constraints" class="tocxref"><span class="secno">5.2 </span>Event Ordering Constraints</a><ul class="toc"><li class="tocline"><a href="#activity-constraints" class="tocxref"><span class="secno">5.2.1 </span>Activity constraints</a></li><li class="tocline"><a href="#entity-constraints" class="tocxref"><span class="secno">5.2.2 </span> Entity constraints</a></li><li class="tocline"><a href="#agent-constraints" class="tocxref"><span class="secno">5.2.3 </span> Agent constraints</a></li></ul></li><li class="tocline"><a href="#type-constraints" class="tocxref"><span class="secno">5.3 </span>Type Constraints</a></li><li class="tocline"><a href="#impossibility-constraints" class="tocxref"><span class="secno">5.4 </span>Impossibility constraints</a></li></ul></li><li class="tocline"><a href="#normalization-validity-equivalence" class="tocxref"><span class="secno">6. </span>Normalization, Validity, and Equivalence</a><ul class="toc"><li class="tocline"><a href="#instance" class="tocxref"><span class="secno">6.1 </span>Instances</a></li><li class="tocline"><a href="#bundle-constraints" class="tocxref"><span class="secno">6.2 </span>Bundles and Documents</a></li></ul></li><li class="tocline"><a href="#glossary" class="tocxref"><span class="secno">7. </span>Glossary</a></li><li class="tocline"><a href="#termination" class="tocxref"><span class="secno">A. </span>Termination of normalization</a></li><li class="tocline"><a href="#changes-since-last-version" class="tocxref"><span class="secno"><span class="insert">B. </span></span><span class="insert">Changes since last version</span></a></li><li class="tocline"><a href="#acknowledgements" class="tocxref"><span class="secno"><span class="delete">B.</span><span class="insert">C.</span> </span>Acknowledgements</a></li><li class="tocline"><a href="#references" class="tocxref"><span class="secno"><span class="delete">C.</span><span class="insert">D.</span> </span>References</a><ul class="toc"><li class="tocline"><a href="#normative-references" class="tocxref"><span class="secno"><span class="delete">C.1</span><span class="insert">D.1</span> </span>Normative references</a></li><li class="tocline"><a href="#informative-references" class="tocxref"><span class="secno"><span class="delete">C.2</span><span class="insert">D.2</span> </span>Informative references</a></li></ul></li></ul></div>
+<p>This document was published by the <a href="http://www.w3.org/2011/prov/">Provenance Working Group</a> as a <span class="delete">Last Call Working Draft.</span><span class="insert">Candidate Recommendation.</span> This document is intended to become a <acronym title="World Wide Web Consortium">W3C</acronym> Recommendation. If you wish to make comments regarding this document, please send them to <a href="mailto:public-prov-comments@w3.org">public-prov-comments@w3.org</a> (<a href="mailto:public-prov-comments-request@w3.org?subject=subscribe">subscribe</a>, <a href="http://lists.w3.org/Archives/Public/public-prov-comments/">archives</a>). <span class="delete">The Last Call period ends 10 October</span><acronym title="World Wide Web Consortium"><span class="insert">W3C</span></acronym><span class="insert"> publishes a Candidate Recommendation to indicate that the document is believed to be stable and to encourage implementation by the developer community. This Candidate Recommendation is expected to advance to Proposed Recommendation no earlier than 31 January</span> 2012. All feedback is welcome.</p><p>Publication as a <span class="delete">Working Draft</span><span class="insert">Candidate Recommendation</span> does not imply endorsement by the <acronym title="World Wide Web Consortium">W3C</acronym> Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.<span class="delete">This is a Last Call Working Draft and thus the Working Group has determined that this document has satisfied the relevant technical requirements and is sufficiently stable to advance through the Technical Recommendation process.</span></p><p>This document was produced by a group operating under the <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/">5 February 2004 <acronym title="World Wide Web Consortium">W3C</acronym> Patent Policy</a>. <acronym title="World Wide Web Consortium">W3C</acronym> maintains a <a href="http://www.w3.org/2004/01/pp-impl/46974/status" rel="disclosure">public list of any patent disclosures</a> made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/#def-essential">Essential Claim(s)</a> must disclose the information in accordance with <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/#sec-Disclosure">section 6 of the <acronym title="World Wide Web Consortium">W3C</acronym> Patent Policy</a>.</p></div><div id="toc" class="section"><h2 class="introductory">Table of Contents</h2><ul class="toc"><li class="tocline"><a href="#introduction" class="tocxref"><span class="secno">1. </span>Introduction<br>
+</a><ul class="toc"><li class="tocline"><a href="#conventions" class="tocxref"><span class="secno">1.1 </span>Conventions</a></li><li class="tocline"><a href="#purpose" class="tocxref"><span class="secno">1.2 </span>Purpose of this document</a></li><li class="tocline"><a href="#structure-of-this-document" class="tocxref"><span class="secno">1.3 </span>Structure of this document</a></li><li class="tocline"><a href="#audience" class="tocxref"><span class="secno">1.4 </span> Audience </a></li></ul></li><li class="tocline"><a href="#rationale" class="tocxref"><span class="secno">2. </span>Rationale</a><ul class="toc"><li class="tocline"><a href="#entities--activities-and-agents" class="tocxref"><span class="secno">2.1 </span>Entities, Activities and Agents</a></li><li class="tocline"><a href="#events" class="tocxref"><span class="secno">2.2 </span>Events</a></li><li class="tocline"><a href="#typing-section" class="tocxref"><span class="secno">2.3 </span>Types</a></li><li class="tocline"><a href="#validation-process-overview-1" class="tocxref"><span class="secno">2.4 </span>Validation Process Overview</a></li><li class="tocline"><a href="#summary-of-inferences-and-constraints" class="tocxref"><span class="secno">2.5 </span>Summary of inferences and constraints</a></li></ul></li><li class="tocline"><a href="#compliance" class="tocxref"><span class="secno">3. </span>Compliance with this document</a></li><li class="tocline"><a href="#concepts" class="tocxref"><span class="secno"><span class="insert">4. </span></span><span class="insert">Basic concepts</span></a></li><li class="tocline"><a href="#inferences" class="tocxref"><span class="secno"><span class="delete">4.</span><span class="insert">5.</span> </span>Definitions and Inferences</a><ul class="toc"><li class="tocline"><a href="#optional-identifiers-and-attributes" class="tocxref"><span class="secno"><span class="delete">4.1</span><span class="insert">5.1</span> </span>Optional Identifiers and Attributes</a></li><li class="tocline"><a href="#entities-and-activities" class="tocxref"><span class="secno"><span class="delete">4.2</span><span class="insert">5.2</span> </span>Entities and Activities</a></li><li class="tocline"><a href="#derivations" class="tocxref"><span class="secno"><span class="delete">4.3</span><span class="insert">5.3</span> </span>Derivations</a></li><li class="tocline"><a href="#agents" class="tocxref"><span class="secno"><span class="delete">4.4</span><span class="insert">5.4</span> </span>Agents</a></li><li class="tocline"><a href="#alternate-and-specialized-entities" class="tocxref"><span class="secno"><span class="delete">4.5</span><span class="insert">5.5</span> </span>Alternate and Specialized Entities</a></li></ul></li><li class="tocline"><a href="#constraints" class="tocxref"><span class="secno"><span class="delete">5.</span><span class="insert">6.</span> </span>Constraints</a><ul class="toc"><li class="tocline"><a href="#uniqueness-constraints" class="tocxref"><span class="secno"><span class="delete">5.1</span><span class="insert">6.1</span> </span>Uniqueness Constraints</a></li><li class="tocline"><a href="#event-ordering-constraints" class="tocxref"><span class="secno"><span class="delete">5.2</span><span class="insert">6.2</span> </span>Event Ordering Constraints</a><ul class="toc"><li class="tocline"><a href="#activity-constraints" class="tocxref"><span class="secno"><span class="delete">5.2.1</span><span class="insert">6.2.1</span> </span>Activity constraints</a></li><li class="tocline"><a href="#entity-constraints" class="tocxref"><span class="secno"><span class="delete">5.2.2</span><span class="insert">6.2.2</span> </span> Entity constraints</a></li><li class="tocline"><a href="#agent-constraints" class="tocxref"><span class="secno"><span class="delete">5.2.3</span><span class="insert">6.2.3</span> </span> Agent constraints</a></li></ul></li><li class="tocline"><a href="#type-constraints" class="tocxref"><span class="secno"><span class="delete">5.3</span><span class="insert">6.3</span> </span>Type Constraints</a></li><li class="tocline"><a href="#impossibility-constraints" class="tocxref"><span class="secno"><span class="delete">5.4</span><span class="insert">6.4</span> </span>Impossibility constraints</a></li></ul></li><li class="tocline"><a href="#normalization-validity-equivalence" class="tocxref"><span class="secno"><span class="delete">6.</span><span class="insert">7.</span> </span>Normalization, Validity, and Equivalence</a><ul class="toc"><li class="tocline"><a href="#instance" class="tocxref"><span class="secno"><span class="delete">6.1</span><span class="insert">7.1</span> </span>Instances</a></li><li class="tocline"><a href="#bundle-constraints" class="tocxref"><span class="secno"><span class="delete">6.2</span><span class="insert">7.2</span> </span>Bundles and Documents</a></li></ul></li><li class="tocline"><a href="#glossary" class="tocxref"><span class="secno"><span class="delete">7.</span><span class="insert">8.</span> </span>Glossary</a></li><li class="tocline"><a href="#termination" class="tocxref"><span class="secno">A. </span>Termination of normalization</a></li><li class="tocline"><a href="#changes-since-last-version" class="tocxref"><span class="secno"><span class="insert">B. </span></span><span class="insert">Changes since last version</span></a></li><li class="tocline"><a href="#acknowledgements" class="tocxref"><span class="secno"><span class="delete">B.</span><span class="insert">C.</span> </span>Acknowledgements</a></li><li class="tocline"><a href="#references" class="tocxref"><span class="secno"><span class="delete">C.</span><span class="insert">D.</span> </span>References</a><ul class="toc"><li class="tocline"><a href="#normative-references" class="tocxref"><span class="secno"><span class="delete">C.1</span><span class="insert">D.1</span> </span>Normative references</a></li><li class="tocline"><a href="#informative-references" class="tocxref"><span class="secno"><span class="delete">C.2</span><span class="insert">D.2</span> </span>Informative references</a></li></ul></li></ul></div>
 
 
 
@@ -1101,7 +1120,7 @@
 Provenance is a record that describes the people, institutions, entities, and activities involved in producing, influencing, or delivering a piece of data or a thing.
 This document complements
   the PROV-DM specification [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-DM">PROV-DM</a></cite>] that defines a data model for
-  provenance on the Web.  </p>
+  provenance on the Web.  <span class="insert"> This document defines a form of validation for provenance. </span></p>
 
 
 
@@ -1131,23 +1150,23 @@
 
 <p>The PROV Data Model, PROV-DM, is a conceptual data model for provenance, which is
 realizable using different representations such as PROV-N and PROV-O.
-A PROV <dfn id="dfn-document">document</dfn> is a set of PROV statements,
-together with zero or more <a>bundles</a>, or named sets of
-statements.  For
+A PROV <a><span class="insert">instance</span></a><span class="insert"> is a set of PROV statements.
+A PROV </span><a>document</a> is <span class="delete">a set of PROV statements,
+</span><span class="insert">an instance 
+</span>together with zero or more <a>bundles</a>, or named <span class="delete">sets of
+statements.</span><span class="insert">instances.</span>  For
 example, a PROV document could be a .provn document, the result
-of a query, a triple store containing PROV statements in RDF, etc.
-A PROV <dfn id="dfn-instance">instance</dfn> is a set of PROV statements.
+of a query, a triple store containing PROV statements in RDF, etc.<span class="delete">
+A PROV </span><span class="delete">instance</span><span class="delete"> is a set of PROV statements.</span>
 The
 PROV-DM specification [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-DM">PROV-DM</a></cite>] imposes minimal requirements upon
 PROV instances. A <a href="#dfn-valid" class="internalDFN">valid</a> PROV instance corresponds to a
 consistent history of objects and interactions to which logical
 reasoning can be safely applied. <span class="delete">By default, </span>PROV instances need not
-be <a href="#dfn-valid" class="internalDFN">valid</a>.  
-</p>
-<p><span class="insert">
+be <a href="#dfn-valid" class="internalDFN">valid</a>.  <span class="insert">
 The term </span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert"> is chosen by analogy with
-notions of validity in other </span><acronym title="World Wide Web Consortium"><span class="insert">W3C</span></acronym><span class="insert"> specifications. Unfortunately, this
-terminology is incompatible with the usual meaning of "validity" in logic;
+notions of validity in other </span><acronym title="World Wide Web Consortium"><span class="insert">W3C</span></acronym><span class="insert"> specifications. This
+terminology differs from the usual meaning of "validity" in logic;
 our notion of validity of a PROV instance/document is closer to
 logical "consistency".
 </span></p>
@@ -1194,8 +1213,10 @@
 to support them at all.</span>  
 Applications producing provenance <em class="rfc2119" title="should">should</em> ensure that it is
 <a href="#dfn-valid" class="internalDFN">valid</a>, and similarly applications consuming provenance <em class="rfc2119" title="may">may</em> reject provenance that is not <a href="#dfn-valid" class="internalDFN">valid</a>.  Applications
-which are determining whether PROV instances or documents convey the same
-information <em class="rfc2119" title="should">should</em> check equivalence as specified here, and <em class="rfc2119" title="should">should</em>
+<span class="delete">which</span><span class="insert">that</span> are determining whether PROV instances or documents convey the same
+information <em class="rfc2119" title="should">should</em> check equivalence as specified <span class="delete">here, and </span><span class="insert">here.  As a
+guideline, applications </span>should
+ 
 treat equivalent instances or documents in the same way.<span class="insert">  This is a
 guideline only, because meaning of "in the same way" is
 application-specific.  For example, applications that manipulate the syntax of
@@ -1214,24 +1235,27 @@
 <a href="#compliance">Section 3</a> summarizes the
 requirements for compliance with this document, which are specified in
 detail in the rest of the document.  </p>
-
-<p> <a href="#inferences">Section 4</a> presents definitions and inferences.  Definitions allow replacing shorthand notation in [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-N">PROV-N</a></cite>]
+<p>
+<a href="#concepts"><span class="insert">Section 4</span></a><span class="insert"> defines basic concepts used in the
+rest of the specification.  </span></p>
+
+<p> <a href="#inferences">Section <span class="delete">4</span><span class="insert">5</span></a> presents definitions and inferences.  Definitions allow replacing shorthand notation in [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-N">PROV-N</a></cite>]
 with more explicit and complete statements; inferences allow adding
 new facts representing implicit knowledge about the structure of
 provenance.  </p>
 
-<p><a href="#constraints">Section 5</a> presents four kinds of constraints,
+<p><a href="#constraints">Section <span class="delete">5</span><span class="insert">6</span></a> presents four kinds of constraints,
 <em>uniqueness</em> constraints that prescribe that certain statements
 must be unique within PROV <a>instances</a>,
 <em>event ordering</em> constraints that require that the records in a
-PROV <a href="#dfn-instance" class="internalDFN">instance</a> are consistent with a sensible ordering of events
+PROV <a>instance</a> are consistent with a sensible ordering of events
 relating the activities, entities and agents involved, 
 <em>impossibility</em> constraints that forbid certain patterns of
 statements in valid PROV instances, and <em>type</em> constraints that
 classify the types of identifiers in valid PROV instances.
 </p>
 
-<p><a href="#normalization-validity-equivalence">Section 6</a> defines the notions
+<p><a href="#normalization-validity-equivalence">Section <span class="delete">6</span><span class="insert">7</span></a> defines the notions
 of <a>validity</a>, <a>equivalence</a> and <a>normalization</a>.
 </p>
 
@@ -1293,7 +1317,7 @@
 thing are called <em>alternates</em>, and the PROV relations of
 <span class="name">specializationOf</span> and <span class="name">alternateOf</span> can be used to link such entities.</p>
 
-<p>Besides entities, a variety of other PROV objects have
+<p>Besides entities, a variety of other PROV objects <span class="delete">have</span><span class="insert">and relationships carry</span>
 attributes, including activity, generation, usage, invalidation, start, end,
 communication, attribution, association, delegation, and
 derivation. Each object has an associated duration interval (which may
@@ -1576,19 +1600,21 @@
        <td class="name">e2</td> 
        <td class="name">'entity'</td>
      </tr>
-      <tr style="text-align: center; ">
-	<td rowspan="3" class="name">mentionOf(e1,e2,b)</td>
-    	<td class="name">e1</td> 
-	<td class="name">'entity'</td>
-     </tr>
-     <tr style="text-align: center; ">
-       <td class="name">e2</td> 
-       <td class="name">'entity'</td>
-     </tr>
-     <tr style="text-align: center; ">
-       <td class="name">b</td> 
-       <td class="name">'entity'</td>
-     </tr>
+      
+	<span class="delete">mentionOf(e1,e2,b)</span>
+    	<span class="delete">e1</span> 
+	<span class="delete">'entity'</span>
+     
+     
+       <span class="delete">e2</span> 
+       <span class="delete">'entity'</span>
+     
+     
+       <span class="delete">b</span> 
+       <span class="delete">'entity'</span>
+     
+           
+
            <tr style="text-align: center; ">
 	<td rowspan="2" class="name">hadMember(c,e)</td>
     	<td class="name">c</td> 
@@ -1632,8 +1658,8 @@
 equivalence procedurally, that is, in terms of a reference
 implementation based on normalization.  Although both declarative and
 procedural specification techniques have advantages, a purely
-declarative specification offers much less assistance for
-implementers, while a procedural approach immediately demonstrates
+declarative specification offers much less guidance for
+implementers, while the procedural approach adopted here immediately demonstrates
 implementability and provides an adequate (polynomial-time) default implementation.  In
 this section we relate the declarative meaning of formulas to their
 procedural meaning.  [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-SEM"><span class="insert">PROV-SEM</span></a></cite><span class="insert">] will provide an alternative,
@@ -1679,21 +1705,24 @@
 </p>
 
   
- <h4 id="substitution">Substitution</h4>
+ <h4 id="substitution-1">Substitution</h4>
 <p>A <em>substitution</em> is a function that maps variables to terms. Concretely, since we only
   need to consider substitutions of finite sets of variables, we can
   write substitutions as <span class="math">[x<sub>1</sub> = t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span>.  A substitution
   <span class="math">S = [x<sub>1</sub> = t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span> 
-  can be <em>applied</em> to a term as follows.
+  can be <em>applied</em> to a term <span class="delete">as follows.</span><span class="insert">by replacing occurrences of
+</span><span class="math"><span class="insert">x_i</span></span><span class="insert"> with </span><span class="math"><span class="insert">t_i</span></span><span class="insert">.</span>
 </p>
-<ol><li>
-  If the term is a variable <span class="math">x<sub>i</sub></span>, one of the variables in the
-  domain of <span class="math">S</span>, then <span class="math">S(x<sub>i</sub>) = t<sub>i</sub></span>.
-  </li>
-  <li>If the term is a constant identifier or literal <span class="math">c</span>, then <span class="math">S(c) = c</span>.
-  </li>
-  </ol>
-<p>
+<span class="delete">
+  If the term is a variable </span><span class="delete">x</span><span class="delete">i</span><span class="delete">, one of the variables in the
+  domain of </span><span class="delete">S</span><span class="delete">, then </span><span class="delete">S(x</span><span class="delete">i</span><span class="delete">) = t</span><span class="delete">i</span><span class="delete">.
+  </span>
+  <span class="delete">If the term is a constant identifier or literal </span><span class="delete">c</span><span class="delete">, then </span><span class="delete">S(c) = c</span><span class="delete">.
+  </span>
+  
+
+
+  <p>
   In addition, a substitution can be applied to an atomic formula
   (PROV statement) <span class="math">p(t<sub>1</sub>,...,t<sub>n</sub>)</span> by applying it to each term,
   that is, <span class="math">S(p(t<sub>1</sub>,...,t<sub>n</sub>)) = p(S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.  Likewise, a
@@ -1741,15 +1770,15 @@
   can be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>. A ⇔ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the
   free variables of the definition.  
 </li>
-<li>An inference of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub></span> and ... and <span class="name">A<sub>l</sub></span>  <span class="conditional">THEN</span>  there
+<li>An inference of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub></span> and ... and <span class="name">A<sub><span class="delete">l</span><span class="insert">p</span></sub></span>  <span class="conditional">THEN</span>  there
   exists <span class="name">y<sub>1</sub></span>...<span class="name">y<sub>m</sub></span> such that <span class="name">B<sub>1</sub></span> and ... and <span class="name">B<sub>k</sub></span> can
-  be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>.  A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the
+  be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>.  A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the
   free variables of the inference.  
 </li>
-<li>A uniqueness, ordering, or typing constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> <span class="conditional">THEN</span> <span class="name">C</span> can be viewed as a formula
-  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ C</span>.  </li>
-<li>A constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> <span class="conditional">THEN INVALID</span> can be viewed as a formula
-  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ False</span>.  </li>
+<li>A uniqueness, ordering, or typing constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub></span> <span class="conditional">THEN</span> <span class="name">C</span> can be viewed as a formula
+  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub> ⇒ C</span>.  </li>
+<li>A constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub></span> <span class="conditional">THEN INVALID</span> can be viewed as a formula
+  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub> ⇒ False</span>.  </li>
   </ul>
 
 
@@ -1774,23 +1803,23 @@
   <li>A logical implication as used in an inference is
    satisfied with the formula  <span class="math">∀
   x<sub>1</sub>,....,x<sub>n</sub>.  A<sub>1</sub> ∧ ... ∧
-  A<sub>l</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧
+  A<sub><span class="delete">l</span><span class="insert">p</span></sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧
   ... ∧ B<sub>k</sub></span> holds, that is, for any substitution of
   the variables <span class="math">x<sub>1</sub>,....,x<sub>n</sub></span>, if  <span class="math">A<sub>1</sub> ∧ ... ∧
-  A<sub>l</sub></span> is true, then 
+  A<sub><span class="delete">l</span><span class="insert">p</span></sub></span> is true, then 
  for some further substitution of terms for variables <span class="math">
   y<sub>1</sub>...y<sub>m</sub></span>, formula <span class="math">B<sub>1</sub> ∧ ... ∧
   B<sub>k</sub></span> is also true.</li>
   <li>A uniqueness, ordering, or typing constraint is satisfied when
-  its associated formula <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ C</span> holds, that is, for any substitution of
+  its associated formula <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub> ⇒ C</span> holds, that is, for any substitution of
   the variables <span class="math">x<sub>1</sub>,....,x<sub>n</sub></span>, if  <span class="math">A<sub>1</sub> ∧ ... ∧
-  A<sub>l</sub></span> is true, then <span class="math">C</span> is
+  A<sub><span class="delete">l</span><span class="insert">p</span></sub></span> is true, then <span class="math">C</span> is
   also true.</li>
   <li>An impossibility constraint is satisfied when the formula
-  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒
+  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub> ⇒
   False</span> holds.  This is logically equivalent to <span class="math">∄
-  x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span>, that is, there exists no
-  substitution for <span class="math">x<sub>1</sub>...x<sub>n</sub></span> making <span class="math">A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> true.
+  x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub></span>, that is, there exists no
+  substitution for <span class="math">x<sub>1</sub>...x<sub>n</sub></span> making <span class="math">A<sub>1</sub> ∧ ... ∧ A<sub><span class="delete">l</span><span class="insert">p</span></sub></span> true.
 </li></ol>  
 
 <h4 id="unification-and-merging"><span class="insert">Unification and </span>Merging</h4>
@@ -1804,7 +1833,8 @@
 where terms can involve variables, constants and function symbols.  In PROV,
   by comparison, </span>unification<span class="delete">, a common operation in logical
   reasoning, including logic programming and automated reasoning.
-Merging</span><span class="insert"> only needs to deal with
+Merging</span><span class="insert"> only needs to deal with variables,
+  constants and literals.
 </span></p>
 <p><span class="insert">
 Unifying</span> two terms <span class="math">t,t'</span> results in either substitution <span class="math">S</span>
@@ -2113,7 +2143,11 @@
 type or relation involved.
 </p>
 
-<div class="note">Table: work in progress; these entries might change when the document is updated.</div>
+<span class="delete">Table: work in progress; these entries might change when the document is updated.</span>
+
+
+
+
 
 <div id="prov-constraints-fig" style="text-align: left;">
 <table class="thinborder" style="margin-left: auto; margin-right: auto; border-color: black;">
@@ -2127,20 +2161,20 @@
 	<td class="essential"><a>Entity</a></td>
 	<td><a class="rule-text" href="#entity-generation-invalidation-inference_text"><span>Inference 7 (entity-generation-invalidation-inference)</span></a><br>
 		<a class="rule-text" href="#specialization-attributes-inference_text"><span>Inference 21 (specialization-attributes-inference)</span></a><br>
-		<a class="rule-text" href="#key-object_text"><span>Constraint 23 (key-object)</span></a><br>
-		<a class="rule-text" href="#impossible-object-property-overlap_text"><span>Constraint 56 (impossible-object-property-overlap)</span></a><br>
-		<a class="rule-text" href="#entity-activity-disjoint_text"><span>Constraint 57 (entity-activity-disjoint)</span></a><br>
+		<a class="rule-text" href="#key-object_text"><span>Constraint <span class="delete">23</span><span class="insert">22</span> (key-object)</span></a><br>
+		<a class="rule-text" href="#impossible-object-property-overlap_text"><span>Constraint <span class="delete">56</span><span class="insert">54</span> (impossible-object-property-overlap)</span></a><br>
+		<a class="rule-text" href="#entity-activity-disjoint_text"><span>Constraint <span class="delete">57</span><span class="insert">55</span> (entity-activity-disjoint)</span></a><br>
 	</td>
 	<td rowspan="8" style="text-align: center; "><a href="http://www.w3.org/TR/prov-dm/#component1" title="Component 1: Entities/Activities">1</a></td>
 </tr>
 <tr class="component1-color">
 	<td class="essential"><a>Activity</a></td>
 	<td><a class="rule-text" href="#activity-start-end-inference_text"><span>Inference 8 (activity-start-end-inference)</span></a><br>
-		<a class="rule-text" href="#key-object_text"><span>Constraint 23 (key-object)</span></a><br>
-		<a class="rule-text" href="#unique-startTime_text"><span>Constraint 29 (unique-startTime)</span></a><br>
-		<a class="rule-text" href="#unique-endTime_text"><span>Constraint 30 (unique-endTime)</span></a><br>
-		<a class="rule-text" href="#impossible-object-property-overlap_text"><span>Constraint 56 (impossible-object-property-overlap)</span></a><br>
-		<a class="rule-text" href="#entity-activity-disjoint_text"><span>Constraint 57 (entity-activity-disjoint)</span></a><br>
+		<a class="rule-text" href="#key-object_text"><span>Constraint <span class="delete">23</span><span class="insert">22</span> (key-object)</span></a><br>
+		<a class="rule-text" href="#unique-startTime_text"><span>Constraint <span class="delete">29</span><span class="insert">28</span> (unique-startTime)</span></a><br>
+		<a class="rule-text" href="#unique-endTime_text"><span>Constraint <span class="delete">30</span><span class="insert">29</span> (unique-endTime)</span></a><br>
+		<a class="rule-text" href="#impossible-object-property-overlap_text"><span>Constraint <span class="delete">56</span><span class="insert">54</span> (impossible-object-property-overlap)</span></a><br>
+		<a class="rule-text" href="#entity-activity-disjoint_text"><span>Constraint <span class="delete">57</span><span class="insert">55</span> (entity-activity-disjoint)</span></a><br>
 	</td>
 </tr>
 <tr class="component1-color">
@@ -2148,99 +2182,99 @@
 	<td><a class="rule-text" href="#generation-use-communication-inference_text"><span>Inference 6 (generation-use-communication-inference)</span></a><br>
 
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#unique-generation_text"><span>Constraint 25 (unique-generation)</span></a><br>
-		<a class="rule-text" href="#generation-within-activity_text"><span>Constraint 36 (generation-within-activity)</span></a><br>
-		<a class="rule-text" href="#generation-precedes-invalidation_text"><span>Constraint 38 (generation-precedes-invalidation)</span></a><br>
-		<a class="rule-text" href="#generation-precedes-usage_text"><span>Constraint 39 (generation-precedes-usage)</span></a><br>
-		<a class="rule-text" href="#generation-generation-ordering_text"><span>Constraint 41 (generation-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#derivation-usage-generation-ordering_text"><span>Constraint 43 (derivation-usage-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#derivation-generation-generation-ordering_text"><span>Constraint 44 (derivation-generation-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#wasStartedBy-ordering_text"><span>Constraint 45 (wasStartedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#wasEndedBy-ordering_text"><span>Constraint 46 (wasEndedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#specialization-generation-ordering_text"><span>Constraint 47 (specialization-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint 49 (wasAssociatedWith-ordering)</span></a><br>
-		<a class="rule-text" href="#wasAttributedTo-ordering_text"><span>Constraint 50 (wasAttributedTo-ordering)</span></a><br>
-		<a class="rule-text" href="#actedOnBehalfOf-ordering_text"><span>Constraint 51 (actedOnBehalfOf-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#unique-generation_text"><span>Constraint <span class="delete">25</span><span class="insert">24</span> (unique-generation)</span></a><br>
+		<a class="rule-text" href="#generation-within-activity_text"><span>Constraint <span class="delete">36</span><span class="insert">34</span> (generation-within-activity)</span></a><br>
+		<a class="rule-text" href="#generation-precedes-invalidation_text"><span>Constraint <span class="delete">38</span><span class="insert">36</span> (generation-precedes-invalidation)</span></a><br>
+		<a class="rule-text" href="#generation-precedes-usage_text"><span>Constraint <span class="delete">39</span><span class="insert">37</span> (generation-precedes-usage)</span></a><br>
+		<a class="rule-text" href="#generation-generation-ordering_text"><span>Constraint <span class="delete">41</span><span class="insert">39</span> (generation-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#derivation-usage-generation-ordering_text"><span>Constraint <span class="delete">43</span><span class="insert">41</span> (derivation-usage-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#derivation-generation-generation-ordering_text"><span>Constraint <span class="delete">44</span><span class="insert">42</span> (derivation-generation-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#wasStartedBy-ordering_text"><span>Constraint <span class="delete">45</span><span class="insert">43</span> (wasStartedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#wasEndedBy-ordering_text"><span>Constraint <span class="delete">46</span><span class="insert">44</span> (wasEndedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#specialization-generation-ordering_text"><span>Constraint <span class="delete">47</span><span class="insert">45</span> (specialization-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint <span class="delete">49</span><span class="insert">47</span> (wasAssociatedWith-ordering)</span></a><br>
+		<a class="rule-text" href="#wasAttributedTo-ordering_text"><span>Constraint <span class="delete">50</span><span class="insert">48</span> (wasAttributedTo-ordering)</span></a><br>
+		<a class="rule-text" href="#actedOnBehalfOf-ordering_text"><span>Constraint <span class="delete">51</span><span class="insert">49</span> (actedOnBehalfOf-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component1-color">
 	<td class="essential"><a>Usage</a></td>
 	<td><a class="rule-text" href="#generation-use-communication-inference_text"><span>Inference 6 (generation-use-communication-inference)</span></a><br>
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#usage-within-activity_text"><span>Constraint 35 (usage-within-activity)</span></a><br>
-		<a class="rule-text" href="#generation-precedes-usage_text"><span>Constraint 39 (generation-precedes-usage)</span></a><br>
-		<a class="rule-text" href="#usage-precedes-invalidation_text"><span>Constraint 40 (usage-precedes-invalidation)</span></a><br>
-		<a class="rule-text" href="#derivation-usage-generation-ordering_text"><span>Constraint 43 (derivation-usage-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#usage-within-activity_text"><span>Constraint <span class="delete">35</span><span class="insert">33</span> (usage-within-activity)</span></a><br>
+		<a class="rule-text" href="#generation-precedes-usage_text"><span>Constraint <span class="delete">39</span><span class="insert">37</span> (generation-precedes-usage)</span></a><br>
+		<a class="rule-text" href="#usage-precedes-invalidation_text"><span>Constraint <span class="delete">40</span><span class="insert">38</span> (usage-precedes-invalidation)</span></a><br>
+		<a class="rule-text" href="#derivation-usage-generation-ordering_text"><span>Constraint <span class="delete">43</span><span class="insert">41</span> (derivation-usage-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component1-color">
 	<td class="essential"><a>Communication</a></td>
 	<td><a class="rule-text" href="#communication-generation-use-inference_text"><span>Inference 5 (communication-generation-use-inference)</span></a><br>
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#wasInformedBy-ordering_text"><span>Constraint 37 (wasInformedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#wasInformedBy-ordering_text"><span>Constraint <span class="delete">37</span><span class="insert">35</span> (wasInformedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component1-color">
 	<td class="essential"><a>Start</a></td>
 	<td><a class="rule-text" href="#wasStartedBy-inference_text"><span>Inference 9 (wasStartedBy-inference)</span></a><br>
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#unique-wasStartedBy_text"><span>Constraint 27 (unique-wasStartedBy)</span></a><br>
-		<a class="rule-text" href="#unique-startTime_text"><span>Constraint 29 (unique-startTime)</span></a><br>
-		<a class="rule-text" href="#start-precedes-end_text"><span>Constraint 32 (start-precedes-end)</span></a><br>
-		<a class="rule-text" href="#usage-within-activity_text"><span>Constraint 35 (usage-within-activity)</span></a><br>
-		<a class="rule-text" href="#generation-within-activity_text"><span>Constraint 36 (generation-within-activity)</span></a><br>
-		<a class="rule-text" href="#wasInformedBy-ordering_text"><span>Constraint 37 (wasInformedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#start-start-ordering_text"><span>Constraint 33 (start-start-ordering)</span></a><br>
-		<a class="rule-text" href="#wasStartedBy-ordering_text"><span>Constraint 45 (wasStartedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint 49 (wasAssociatedWith-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#unique-wasStartedBy_text"><span>Constraint <span class="delete">27</span><span class="insert">26</span> (unique-wasStartedBy)</span></a><br>
+		<a class="rule-text" href="#unique-startTime_text"><span>Constraint <span class="delete">29</span><span class="insert">28</span> (unique-startTime)</span></a><br>
+		<a class="rule-text" href="#start-precedes-end_text"><span>Constraint <span class="delete">32</span><span class="insert">30</span> (start-precedes-end)</span></a><br>
+		<a class="rule-text" href="#usage-within-activity_text"><span>Constraint <span class="delete">35</span><span class="insert">33</span> (usage-within-activity)</span></a><br>
+		<a class="rule-text" href="#generation-within-activity_text"><span>Constraint <span class="delete">36</span><span class="insert">34</span> (generation-within-activity)</span></a><br>
+		<a class="rule-text" href="#wasInformedBy-ordering_text"><span>Constraint <span class="delete">37</span><span class="insert">35</span> (wasInformedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#start-start-ordering_text"><span>Constraint <span class="delete">33</span><span class="insert">31</span> (start-start-ordering)</span></a><br>
+		<a class="rule-text" href="#wasStartedBy-ordering_text"><span>Constraint <span class="delete">45</span><span class="insert">43</span> (wasStartedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint <span class="delete">49</span><span class="insert">47</span> (wasAssociatedWith-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component1-color">
 	<td class="essential"><a>End</a></td>
 	<td><a class="rule-text" href="#wasEndedBy-inference_text"><span>Inference 10 (wasEndedBy-inference)</span></a><br>
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#unique-wasEndedBy_text"><span>Constraint 28 (unique-wasEndedBy)</span></a><br>
-		<a class="rule-text" href="#unique-endTime_text"><span>Constraint 30 (unique-endTime)</span></a><br>
-		<a class="rule-text" href="#start-precedes-end_text"><span>Constraint 32 (start-precedes-end)</span></a><br>
-		<a class="rule-text" href="#usage-within-activity_text"><span>Constraint 35 (usage-within-activity)</span></a><br>
-		<a class="rule-text" href="#generation-within-activity_text"><span>Constraint 36 (generation-within-activity)</span></a><br>
-		<a class="rule-text" href="#wasInformedBy-ordering_text"><span>Constraint 37 (wasInformedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#end-end-ordering_text"><span>Constraint 34 (end-end-ordering)</span></a><br>
-		<a class="rule-text" href="#wasEndedBy-ordering_text"><span>Constraint 46 (wasEndedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint 49 (wasAssociatedWith-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#unique-wasEndedBy_text"><span>Constraint <span class="delete">28</span><span class="insert">27</span> (unique-wasEndedBy)</span></a><br>
+		<a class="rule-text" href="#unique-endTime_text"><span>Constraint <span class="delete">30</span><span class="insert">29</span> (unique-endTime)</span></a><br>
+		<a class="rule-text" href="#start-precedes-end_text"><span>Constraint <span class="delete">32</span><span class="insert">30</span> (start-precedes-end)</span></a><br>
+		<a class="rule-text" href="#usage-within-activity_text"><span>Constraint <span class="delete">35</span><span class="insert">33</span> (usage-within-activity)</span></a><br>
+		<a class="rule-text" href="#generation-within-activity_text"><span>Constraint <span class="delete">36</span><span class="insert">34</span> (generation-within-activity)</span></a><br>
+		<a class="rule-text" href="#wasInformedBy-ordering_text"><span>Constraint <span class="delete">37</span><span class="insert">35</span> (wasInformedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#end-end-ordering_text"><span>Constraint <span class="delete">34</span><span class="insert">32</span> (end-end-ordering)</span></a><br>
+		<a class="rule-text" href="#wasEndedBy-ordering_text"><span>Constraint <span class="delete">46</span><span class="insert">44</span> (wasEndedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint <span class="delete">49</span><span class="insert">47</span> (wasAssociatedWith-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component1-color">
 	<td class="essential"><a>Invalidation</a></td>
 	<td><a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#unique-invalidation_text"><span>Constraint 26 (unique-invalidation)</span></a><br>
-		<a class="rule-text" href="#generation-precedes-invalidation_text"><span>Constraint 38 (generation-precedes-invalidation)</span></a><br>
-		<a class="rule-text" href="#usage-precedes-invalidation_text"><span>Constraint 40 (usage-precedes-invalidation)</span></a><br>
-		<a class="rule-text" href="#invalidation-invalidation-ordering_text"><span>Constraint 42 (invalidation-invalidation-ordering)</span></a><br>
-		<a class="rule-text" href="#wasStartedBy-ordering_text"><span>Constraint 45 (wasStartedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#wasEndedBy-ordering_text"><span>Constraint 46 (wasEndedBy-ordering)</span></a><br>
-		<a class="rule-text" href="#specialization-invalidation-ordering_text"><span>Constraint 48 (specialization-invalidation-ordering)</span></a><br>
-		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint 49 (wasAssociatedWith-ordering)</span></a><br>
-		<a class="rule-text" href="#wasAttributedTo-ordering_text"><span>Constraint 50 (wasAttributedTo-ordering)</span></a><br>
-		<a class="rule-text" href="#actedOnBehalfOf-ordering_text"><span>Constraint 51 (actedOnBehalfOf-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#unique-invalidation_text"><span>Constraint <span class="delete">26</span><span class="insert">25</span> (unique-invalidation)</span></a><br>
+		<a class="rule-text" href="#generation-precedes-invalidation_text"><span>Constraint <span class="delete">38</span><span class="insert">36</span> (generation-precedes-invalidation)</span></a><br>
+		<a class="rule-text" href="#usage-precedes-invalidation_text"><span>Constraint <span class="delete">40</span><span class="insert">38</span> (usage-precedes-invalidation)</span></a><br>
+		<a class="rule-text" href="#invalidation-invalidation-ordering_text"><span>Constraint <span class="delete">42</span><span class="insert">40</span> (invalidation-invalidation-ordering)</span></a><br>
+		<a class="rule-text" href="#wasStartedBy-ordering_text"><span>Constraint <span class="delete">45</span><span class="insert">43</span> (wasStartedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#wasEndedBy-ordering_text"><span>Constraint <span class="delete">46</span><span class="insert">44</span> (wasEndedBy-ordering)</span></a><br>
+		<a class="rule-text" href="#specialization-invalidation-ordering_text"><span>Constraint <span class="delete">48</span><span class="insert">46</span> (specialization-invalidation-ordering)</span></a><br>
+		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint <span class="delete">49</span><span class="insert">47</span> (wasAssociatedWith-ordering)</span></a><br>
+		<a class="rule-text" href="#wasAttributedTo-ordering_text"><span>Constraint <span class="delete">50</span><span class="insert">48</span> (wasAttributedTo-ordering)</span></a><br>
+		<a class="rule-text" href="#actedOnBehalfOf-ordering_text"><span>Constraint <span class="delete">51</span><span class="insert">49</span> (actedOnBehalfOf-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
@@ -2252,10 +2286,10 @@
 
 
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#derivation-usage-generation-ordering_text"><span>Constraint 43 (derivation-usage-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#derivation-generation-generation-ordering_text"><span>Constraint 44 (derivation-generation-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#derivation-usage-generation-ordering_text"><span>Constraint <span class="delete">43</span><span class="insert">41</span> (derivation-usage-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#derivation-generation-generation-ordering_text"><span>Constraint <span class="delete">44</span><span class="insert">42</span> (derivation-generation-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 	<td rowspan="5" style="text-align: center; "><a href="http://www.w3.org/TR/prov-dm/#component2" title="Component 2: Derivations">2</a></td>
 </tr>
@@ -2279,8 +2313,8 @@
 
 <tr class="component3-color" style="border-collapse: collapse; ">
 	<td class="essential"><a>Agent</a></td>
-	<td><a class="rule-text" href="#key-object_text"><span>Constraint 23 (key-object)</span></a><br>
-		<a class="rule-text" href="#impossible-object-property-overlap_text"><span>Constraint 56 (impossible-object-property-overlap)</span></a><br>
+	<td><a class="rule-text" href="#key-object_text"><span>Constraint <span class="delete">23</span><span class="insert">22</span> (key-object)</span></a><br>
+		<a class="rule-text" href="#impossible-object-property-overlap_text"><span>Constraint <span class="delete">56</span><span class="insert">54</span> (impossible-object-property-overlap)</span></a><br>
 	</td>
 	<td rowspan="5" style="text-align: center; "><a href="http://www.w3.org/TR/prov-dm/#component3" title="Component 3: Agents/Responsibility">3</a></td>
 </tr>
@@ -2288,47 +2322,47 @@
 	<td class="essential"><a>Attribution</a></td>
 	<td><a class="rule-text" href="#attribution-inference_text"><span>Inference 13 (attribution-inference)</span></a><br>
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#wasAttributedTo-ordering_text"><span>Constraint 50 (wasAttributedTo-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#wasAttributedTo-ordering_text"><span>Constraint <span class="delete">50</span><span class="insert">48</span> (wasAttributedTo-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component3-color">
 	<td class="essential"><a>Association</a></td>
 	<td><a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint 49 (wasAssociatedWith-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#wasAssociatedWith-ordering_text"><span>Constraint <span class="delete">49</span><span class="insert">47</span> (wasAssociatedWith-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component3-color">
 	<td class="essential"><a>Delegation</a></td>
 	<td><a class="rule-text" href="#delegation-inference_text"><span>Inference 14 (delegation-inference)</span></a><br>
 		<a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
-		<a class="rule-text" href="#actedOnBehalfOf-ordering_text"><span>Constraint 51 (actedOnBehalfOf-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint 55 (impossible-property-overlap)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
+		<a class="rule-text" href="#actedOnBehalfOf-ordering_text"><span>Constraint <span class="delete">51</span><span class="insert">49</span> (actedOnBehalfOf-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-property-overlap_text"><span>Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
 <tr class="component3-color">
 	<td class="essential"><a>Influence</a></td>
 	<td><a class="rule-text" href="#influence-inference_text"><span>Inference 15 (influence-inference)</span></a><br>
-		<a class="rule-text" href="#key-properties_text"><span>Constraint 24 (key-properties)</span></a><br>
+		<a class="rule-text" href="#key-properties_text"><span>Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</span></a><br>
 	</td>
 </tr>
 <tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
 
 <tr class="component4-color">
 	<td><a title="bundle">Bundle constructor</a></td>
-	<td>No specific constraints; see <a href="#bundle-constraints" class="sectionRef">section 6.2 Bundles and Documents</a></td>
+	<td>No specific constraints; see <a href="#bundle-constraints" class="sectionRef">section <span class="delete">6.2</span><span class="insert">7.2</span> Bundles and Documents</a></td>
 	<td rowspan="2" style="text-align: center; "><a href="http://www.w3.org/TR/prov-dm/#component4" title="Component 4: Bundles">4</a></td>
 </tr>
 <tr class="component4-color">
 	<td class="provType"><a title="bundle">Bundle type</a></td>
-	<td> No specific constraints; see <a href="#bundle-constraints" class="sectionRef">section 6.2 Bundles and Documents</a>
+	<td> No specific constraints; see <a href="#bundle-constraints" class="sectionRef">section <span class="delete">6.2</span><span class="insert">7.2</span> Bundles and Documents</a>
         </td>
 </tr>
 <tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
@@ -2338,7 +2372,7 @@
 	<td><a class="rule-text" href="#alternate-reflexive_text"><span>Inference 16 (alternate-reflexive)</span></a><br>
 		<a class="rule-text" href="#alternate-transitive_text"><span>Inference 17 (alternate-transitive)</span></a><br>
 		<a class="rule-text" href="#alternate-symmetric_text"><span>Inference 18 (alternate-symmetric)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 	<td rowspan="3" style="text-align: center; "><a href="http://www.w3.org/TR/prov-dm/#component5" title="Component 5: Alternate Entities">5</a></td>
 </tr>
@@ -2347,19 +2381,21 @@
 	<td><a class="rule-text" href="#specialization-transitive_text"><span>Inference 19 (specialization-transitive)</span></a><br>
 		<a class="rule-text" href="#specialization-alternate-inference_text"><span>Inference 20 (specialization-alternate-inference)</span></a><br>
 		<a class="rule-text" href="#specialization-attributes-inference_text"><span>Inference 21 (specialization-attributes-inference)</span></a><br>
-		<a class="rule-text" href="#specialization-generation-ordering_text"><span>Constraint 47 (specialization-generation-ordering)</span></a><br>
-		<a class="rule-text" href="#specialization-invalidation-ordering_text"><span>Constraint 48 (specialization-invalidation-ordering)</span></a><br>
-		<a class="rule-text" href="#impossible-specialization-reflexive_text"><span>Constraint 54 (impossible-specialization-reflexive)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+		<a class="rule-text" href="#specialization-generation-ordering_text"><span>Constraint <span class="delete">47</span><span class="insert">45</span> (specialization-generation-ordering)</span></a><br>
+		<a class="rule-text" href="#specialization-invalidation-ordering_text"><span>Constraint <span class="delete">48</span><span class="insert">46</span> (specialization-invalidation-ordering)</span></a><br>
+		<a class="rule-text" href="#impossible-specialization-reflexive_text"><span>Constraint <span class="delete">54</span><span class="insert">52</span> (impossible-specialization-reflexive)</span></a><br>
+		<a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
 	</td>
 </tr>
-<tr class="component5-color">
-	<td><a>Mention</a></td>
-	<td><a class="rule-text" href="#mention-specialization-inference_text"><span>Inference 22 (mention-specialization-inference)</span></a><br>
-		<a class="rule-text" href="#unique-mention_text"><span>Constraint 31 (unique-mention)</span></a><br>
-		<a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
-	</td>
-</tr>
+
+	<span class="delete">Mention</span>
+	<span class="delete">Inference 22 (mention-specialization-inference)</span>
+		<span class="delete">Constraint 31 (unique-mention)</span>
+		<span class="delete">Constraint 52 (typing)</span>
+	
+
+
+
 <tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
 
 <tr class="component6-color">
@@ -2369,8 +2405,8 @@
 </tr>
 <tr class="component6-color">
 	<td><a>Membership</a></td>
-	<td> <a class="rule-text" href="#membership-empty-collection_text"><span>Constraint 58 (membership-empty-collection)</span></a><br>
-             <a class="rule-text" href="#typing_text"><span>Constraint 52 (typing)</span></a><br>
+	<td> <a class="rule-text" href="#membership-empty-collection_text"><span>Constraint <span class="delete">58</span><span class="insert">56</span> (membership-empty-collection)</span></a><br>
+             <a class="rule-text" href="#typing_text"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a><br>
         </td>
 </tr>
 </tbody></table>
@@ -2386,22 +2422,26 @@
 
 <p>
   For the purpose of compliance, the normative sections of this document
-  are <a href="#compliance" class="sectionRef">section 3. Compliance with this document</a>, <a href="#inferences" class="sectionRef">section 4. Definitions and Inferences</a>, <a href="#constraints" class="sectionRef">section 5. Constraints</a>, and <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>.  
+  are <a href="#compliance" class="sectionRef">section 3. Compliance with this document</a>, 
+<a href="#concepts" class="sectionRef"><span class="insert">section 4. Basic concepts</span></a><span class="insert">,
+</span><a href="#inferences" class="sectionRef">section <span class="delete">4.</span><span class="insert">5.</span> Definitions and Inferences</a>, 
+<a href="#constraints" class="sectionRef">section <span class="delete">5.</span><span class="insert">6.</span> Constraints</a>, and 
+<a href="#normalization-validity-equivalence" class="sectionRef">section <span class="delete">6.</span><span class="insert">7.</span> Normalization, Validity, and Equivalence</a>.  
 
 
  To be compliant:
   </p><ol><li>When processing provenance, an
-    application <em class="rfc2119" title="may">may</em> apply the inferences and definitions in <a href="#inferences" class="sectionRef">section 4. Definitions and Inferences</a>.</li>
+    application <em class="rfc2119" title="may">may</em> apply the inferences and definitions in <a href="#inferences" class="sectionRef">section <span class="delete">4.</span><span class="insert">5.</span> Definitions and Inferences</a>.</li>
    <li>If determining whether a PROV instance or document is <a href="#dfn-valid" class="internalDFN">valid</a>, an
     application <em class="rfc2119" title="must">must</em> <span class="delete">check that</span><span class="insert">determine whether</span> all of the
-    constraints of <a href="#constraints" class="sectionRef">section 5. Constraints</a> are
+    constraints of <a href="#constraints" class="sectionRef">section <span class="delete">5.</span><span class="insert">6.</span> Constraints</a> are
   satisfied   on 
   the <a href="#dfn-normal-form" class="internalDFN">normal form</a> of the instance or document.  </li>
    <li> If producing provenance meant for other applications to
-    use, the application <em class="rfc2119" title="should">should</em> produce <a href="#dfn-valid" class="internalDFN">valid</a> provenance, as specified in <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>. </li>
+    use, the application <em class="rfc2119" title="should">should</em> produce <a href="#dfn-valid" class="internalDFN">valid</a> provenance, as specified in <a href="#normalization-validity-equivalence" class="sectionRef">section <span class="delete">6.</span><span class="insert">7.</span> Normalization, Validity, and Equivalence</a>. </li>
     <li>If determining whether two PROV instances or documents are
   <a href="#dfn-equivalent" class="internalDFN">equivalent</a>, an application <em class="rfc2119" title="must">must</em> determine whether their
-  normal forms are equal, as specified in <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>.
+  normal forms are equal, as specified in <a href="#normalization-validity-equivalence" class="sectionRef">section <span class="delete">6.</span><span class="insert">7.</span> Normalization, Validity, and Equivalence</a>.
   </li></ol>
 
   <p><span class="delete">Compliant </span><span class="insert">This specification defines validity and equivalence procedurally
@@ -2433,18 +2473,126 @@
 
  
 
+
+
+
+ <div id="concepts" class="section">
+  <h2><span class="secno">4. </span><span class="insert">Basic concepts</span></h2>
+
+  <p><span class="insert">This section specifies the key concepts of terms, statements, instances, substitution,
+  satisfaction, and unification, which have already been discussed in
+  </span><a href="#rationale"><span class="insert">Section 2</span></a><span class="insert">.  
+  </span></p>
+
+  <p><span class="insert">Many PROV relation statements have an identifier, identifying a
+  link between two or more related objects.  Identifiers can sometimes
+  be omitted in [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-N"><span class="insert">PROV-N</span></a></cite><span class="insert">] notation.  For the purpose of inference and
+  validity checking, we generate special identifiers called
+  </span><dfn id="dfn-variables"><span class="insert">variables</span></dfn><span class="insert"> denoting the unknown values.
+  Generally, identifiers occurring in constraints and inferences are
+  variables.  Variables that are generated during inferences and
+  appear inside an instance are often called </span><dfn id="dfn-existential-variables"><span class="insert">existential
+  variables</span></dfn><span class="insert">, because they are implicitly existentially quantified.
+</span></p>
+  
+  <p><span class="insert"> A </span><dfn id="term"><span class="insert">PROV term</span></dfn><span class="insert"> is a constant identifier
+  </span><span class="math"><span class="insert">c</span></span><span class="insert">, a placeholder </span><span class="name"><span class="insert">-</span></span><span class="insert">, a literal value, 
+  or an existential variable </span><span class="math"><span class="insert">x</span></span><span class="insert">.  An
+  arbitrary PROV term is written  </span><span class="math"><span class="insert">t</span></span><span class="insert">.</span></p>
+  
+  <p><span class="insert"> A </span><dfn id="statement"><span class="insert">PROV statement</span></dfn><span class="insert"> is an expression of
+  the form </span><span class="math"><span class="insert">p(t</span><sub><span class="insert">1</span></sub><span class="insert">,...,t</span><sub><span class="insert">n</span></sub><span class="insert">)</span></span><span class="insert"> or </span><span class="math"><span class="insert">p(id;t</span><sub><span class="insert">1</span></sub><span class="insert">,...,t</span><sub><span class="insert">n</span></sub><span class="insert">)</span></span><span class="insert"> where
+  </span><span class="math"><span class="insert">id,t</span><sub><span class="insert">1</span></sub><span class="insert">,...,t</span><sub><span class="insert">n</span></sub></span><span class="insert"> are
+  PROV </span><a><span class="insert">term</span></a><span class="insert">s and </span><span class="math"><span class="insert">p</span></span><span class="insert"> is one of the
+  basic PROV relations. An arbitrary PROV statement is written  </span><span class="math"><span class="insert">A</span></span><span class="insert">.</span></p>
+  
+<p><span class="insert">  A </span><dfn id="instance"><span class="insert">PROV instance</span></dfn><span class="insert"> is a set of PROV
+  statements.  Two instances are considered to be the same if they
+  contain the same statements, without regard to order or repetition.
+  An arbitrary PROV instance is written </span><span class="math"><span class="insert">I</span></span><span class="insert">.
+</span></p>
+
+  <p><span class="insert">A </span><dfn id="substitution"><span class="insert">substitution</span></dfn> <span class="math"><span class="insert">S</span></span><span class="insert"> is a mapping </span><span class="math"><span class="insert">
+  [x</span><sub><span class="insert">1</span></sub><span class="insert">=t</span><sub><span class="insert">1</span></sub><span class="insert">,...,x</span><sub><span class="insert">n</span></sub><span class="insert">=t</span><sub><span class="insert">n</span></sub><span class="insert">]</span></span><span class="insert"> associating existential variables
+  with terms.  A substitution is </span><em><span class="insert">applied</span></em><span class="insert"> to a term, statement
+  or instance by replacing all occurrences of each of the variables
+  </span><span class="math"><span class="insert">x</span><sub><span class="insert">i</span></sub></span><span class="insert"> with the corresponding </span><span class="math"><span class="insert">t</span><sub><span class="insert">i</span></sub></span><span class="insert">.  Specifically, if </span><span class="math"><span class="insert">S =
+  [x</span><sub><span class="insert">1</span></sub><span class="insert">=t</span><sub><span class="insert">1</span></sub><span class="insert">,...,x</span><sub><span class="insert">n</span></sub><span class="insert">=t</span><sub><span class="insert">n</span></sub><span class="insert">]</span></span><span class="insert">
+  then the application of </span><span class="math"><span class="insert">S</span></span><span class="insert"> to a term, statement or instance, written </span><span class="math"><span class="insert">S(t)</span></span><span class="insert">, </span><span class="math"><span class="insert">S(A)</span></span><span class="insert"> and
+  </span><span class="math"><span class="insert">S(I)</span></span><span class="insert"> respectively, is defined as follows:</span></p>
+<ul><li><span class="math"><span class="insert">S(c) = c</span></span><span class="insert"> if </span><span class="math"><span class="insert">c</span></span><span class="insert"> is a constant identifier.</span></li>
+<li><span class="math"><span class="insert">S(x</span><sub><span class="insert">i</span></sub><span class="insert">) = t</span><sub><span class="insert">i</span></sub></span><span class="insert"> if </span><span class="math"><span class="insert">x</span><sub><span class="insert">i</span></sub></span><span class="insert"> is one of the variables bound to a
+  term </span><span class="math"><span class="insert">t</span><sub><span class="insert">i</span></sub></span><span class="insert"> in </span><span class="math"><span class="insert">S</span></span><span class="insert">.</span></li>
+<li><span class="math"><span class="insert">S(x) = x</span></span><span class="insert"> if </span><span class="math"><span class="insert">x</span></span><span class="insert"> is a variable not bound in </span><span class="math"><span class="insert">S</span></span><span class="insert">.</span></li>
+<li><span class="math"><span class="insert">S(p(t</span><sub><span class="insert">1</span></sub><span class="insert">,...,t</span><sub><span class="insert">n</span></sub><span class="insert">)) = p(S(t</span><sub><span class="insert">1</span></sub><span class="insert">),...,S(t</span><sub><span class="insert">n</span></sub><span class="insert">))</span></span><span class="insert">.</span></li>
+<li><span class="math"><span class="insert">S(p(id;t</span><sub><span class="insert">1</span></sub><span class="insert">,...,t</span><sub><span class="insert">n</span></sub><span class="insert">)) = p(S(id);S(t</span><sub><span class="insert">1</span></sub><span class="insert">),...,S(t</span><sub><span class="insert">n</span></sub><span class="insert">))</span></span><span class="insert">.</span></li>
+<li><span class="math"><span class="insert">S(I) = { S(A) | A ∈ I } </span></span><span class="insert"> if </span><span class="math"><span class="insert">I</span></span><span class="insert"> is an instance.</span></li>
+</ul>
+
+  <p><span class="insert">Suppose </span><span class="math"><span class="insert">A</span></span><span class="insert"> is a statement and </span><span class="math"><span class="insert">I</span></span><span class="insert"> is an
+  instance and </span><span class="math"><span class="insert">S</span></span><span class="insert"> a substitution.  We say that </span><span class="math"><span class="insert">A</span></span><span class="insert"> is
+  </span><dfn id="dfn-satisfied"><span class="insert">satisfied</span></dfn><span class="insert"> in </span><span class="math"><span class="insert">I</span></span><span class="insert"> by </span><span class="math"><span class="insert">S</span></span><span class="insert"> if </span><span class="math"><span class="insert">S(A) ∈ I</span></span><span class="insert">.  Likewise,
+  we say that a set of statements </span><span class="math"><span class="insert">{A</span><sub><span class="insert">1</span></sub><span class="insert">,...,A</span><sub><span class="insert">n</span></sub><span class="insert">}</span></span><span class="insert"> is satisfied in
+  </span><span class="math"><span class="insert">I</span></span><span class="insert"> if each </span><span class="math"><span class="insert">A</span><sub><span class="insert">i</span></sub></span><span class="insert"> is satisfied in </span><span class="math"><span class="insert">I</span></span><span class="insert"> by </span><span class="math"><span class="insert">S</span></span><span class="insert">. Finally, we
+  say that a set of statements is </span><dfn id="dfn-satisfiable"><span class="insert">satisfiable</span></dfn><span class="insert">
+  in </span><span class="math"><span class="insert">I</span></span><span class="insert"> if there is some substitution </span><span class="math"><span class="insert">S</span></span><span class="insert"> that satisfies the
+  statements in </span><span class="math"><span class="insert">I</span></span><span class="insert">.
+</span></p>
+ 
+    <p> <dfn id="dfn-unification"><span class="insert">Unification</span></dfn><span class="insert"> is an operation that can be applied
+   to a pair of terms.
+   The result of unification is either a </span><dfn id="dfn-unifier"><span class="insert">unifier</span></dfn><span class="insert">, that is, a substitution </span><span class="math"><span class="insert">S</span></span><span class="insert"> such that </span><span class="math"><span class="insert">S(t)
+   = S(t')</span></span><span class="insert">, or failure, indicating
+   that there is no </span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert">. Unification of pairs of terms is defined as follows.</span></p>
+
+    <ul>
+      <li><span class="insert"> If </span><span class="math"><span class="insert">t</span></span><span class="insert"> and </span><span class="math"><span class="insert">t'</span></span><span class="insert"> are constant identifiers or literal values
+      (including the placeholder </span><span class="name"><span class="insert">-</span></span><span class="insert">), then
+      there are two cases.  If </span><span class="math"><span class="insert">t = t'</span></span><span class="insert"> then their </span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert"> is the
+      empty substitution, otherwise unification
+fails.  </span></li>
+   <li><span class="insert"> If </span><span class="math"><span class="insert">x</span></span><span class="insert"> is an existential variable
+      and 
+   </span><span class="math"><span class="insert">t'</span></span><span class="insert"> is any term (identifier, constant,
+      placeholder </span><span class="name"><span class="insert">-</span></span><span class="insert">, or
+      existential variable), then their
+   </span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert"> is
+      </span><span class="math"><span class="insert">[x=t']</span></span><span class="insert">.  In the special case where
+      </span><span class="math"><span class="insert">t'=x</span></span><span class="insert">, the  </span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert"> is the empty substitution.</span></li>
+         <li><span class="insert"> If </span><span class="math"><span class="insert">t</span></span><span class="insert"> is any term (identifier, constant,
+      placeholder </span><span class="name"><span class="insert">-</span></span><span class="insert">, or
+      existential variable) and
+   </span><span class="math"><span class="insert">x'</span></span><span class="insert"> is an existential variable, then their
+      </span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert"> is the same as the </span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert"> of </span><span class="math"><span class="insert">x</span></span><span class="insert">
+      and </span><span class="math"><span class="insert">t</span></span><span class="insert">.</span></li>
+      </ul>
+      
+
+
+<div class="remark"><span class="insert">Unification is analogous to unification in
+  logic programming and theorem proving, restricted to flat terms with
+constants and variables but   no function symbols.  No "occurs check" is needed because there are no
+  function symbols.</span></div>
+
+    <p><span class="insert">Two PROV instances </span><span class="math"><span class="insert">I</span></span><span class="insert"> and </span><span class="math"><span class="insert">I'</span></span><span class="insert"> are </span><dfn id="dfn-isomorphic"><span class="insert">isomorphic</span></dfn><span class="insert"> if
+  there exists an invertible substitution </span><span class="math"><span class="insert">S</span></span><span class="insert"> that maps each
+  variable of </span><span class="math"><span class="insert">I</span></span><span class="insert"> to a distinct variable of </span><span class="math"><span class="insert">I'</span></span><span class="insert"> and such that
+  </span><span class="math"><span class="insert">S(I) = I'</span></span><span class="insert">.</span></p>
+
+
+</div>
 <div id="inferences" class="section">
-<h2><span class="secno">4. </span>Definitions and Inferences</h2>
+<h2><span class="secno"><span class="insert">5. </span></span>Definitions and Inferences</h2>
 <p>
 This section  describes <a title="definition" href="#definition" class="internalDFN">definitions</a> and <a title="inference" href="#inference" class="internalDFN">inferences</a> that <em class="rfc2119" title="may">may</em> be used on
-  provenance data, and preserve <a>equivalence</a> on <a href="#dfn-valid" class="internalDFN">valid</a>
-PROV instances (as detailed in <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>).
+  provenance data, and <span class="insert">that </span>preserve <a>equivalence</a> on <a href="#dfn-valid" class="internalDFN">valid</a>
+PROV instances (as detailed in <a href="#normalization-validity-equivalence" class="sectionRef">section <span class="delete">6.</span><span class="insert">7.</span> Normalization, Validity, and Equivalence</a>).
 A <dfn id="definition">definition</dfn> is a rule that can be applied to
-  PROV instances to replace defined expressions with definitions. An  <dfn id="inference">inference</dfn> is a rule that can be applied
+  PROV instances to replace defined <span class="delete">expressions</span><span class="insert">statements</span> with <span class="delete">definitions.</span><span class="insert">other statements.</span> An  <dfn id="inference">inference</dfn> is a rule that can be applied
   to PROV instances to add new PROV statements.  A definition states that a
   provenance statement is equivalent to some other statements, whereas
-  an inference only states one direction of an implication; thus,
-  defined provenance statements can be replaced by their definitions.
+  an inference only states one direction of an <span class="delete">implication; thus,
+  defined provenance statements can be replaced by their definitions.</span><span class="insert">implication.</span>
 </p>
 
 
@@ -2474,7 +2622,7 @@
 
   <div class="remark"><span class="insert">
     We use definitions primarily to expand the compact, concrete
-    PROV-N syntax, including short forms and optional parameters to the abstract syntax
+    PROV-N syntax, including short forms and optional parameters, to the abstract syntax
     implicitly used in PROV-DM.
   </span></div>
 
@@ -2489,14 +2637,14 @@
 <p> Inferences can be applied to PROV instances.  Applying an inference to an instance means that if all of the provenance statements matching
   <span class="name">hyp<sub>1</sub></span>... <span class="name">hyp<sub>k</sub></span>
   can be found in the instance, then we check whether the conclusion 
-  <span class="name">concl<sub>1</sub></span> ... <span class="name">concl<sub>n</sub></span> is satisfied for some values
+  <span class="name">concl<sub>1</sub></span> ... <span class="name">concl<sub>n</sub></span> is <a href="#dfn-satisfied" class="internalDFN">satisfied</a> for some values
   of existential variables.  If so, application of the inference has
   no effect on the instance.  If not, then a copy the
   conclusion should be added to the instance, after
   generating fresh identifiers <span class="name">a<sub>1</sub></span>,...,<span class="name">a<sub>m</sub></span> for the existential variables.  These fresh
   identifiers might later be found to be equal to known identifiers;
   they play a similar role in PROV constraints to existential
-  variables in logic, to "labeled nulls" in database theory
+  variables in <span class="delete">logic, to "labeled nulls" in</span><span class="insert">logic [</span><cite><a class="bibref" rel="biblioentry" href="#bib-Logic"><span class="insert">Logic</span></a></cite><span class="insert">] or</span> database theory
   [<cite><a class="bibref" rel="biblioentry" href="#bib-DBCONSTRAINTS">DBCONSTRAINTS</a></cite><span class="delete">],  or</span><span class="insert">].
   
   In general, omitted optional parameters</span> to<span class="delete"> blank nodes in </span>
@@ -2528,33 +2676,38 @@
   inferences.  This issue is discussed in more detail under <a href="#uniqueness-constraints">Uniqueness Constraints</a>.
   </p>
   
-<p>In a [definition|inference], term symbols such as <span class="name">id</span>, 
+<p>In a <span class="delete">[definition|inference],</span><span class="insert">definition or inference,</span> term symbols such as <span class="name">id</span>, 
 	<span class="name">start</span>, <span class="name">end</span>, <span class="name">e</span>, 
 	<span class="name">a</span>, <span class="name">attrs</span>,
 	are assumed to be variables unless otherwise specified.  These variables are scoped at 
-	the [definition|inference|constraint] level, so the rule is equivalent to any one-for-one 
-	renaming of the variable names.  When several rules are collected within a [definition|inference] 
+	the <span class="delete">[definition|inference|constraint]</span><span class="insert">definition, inference, or constraint</span> level, so the rule is equivalent to any one-for-one 
+	renaming of the variable names.  When several rules are 
+	collected within a <span class="delete">[definition|inference]</span><span class="insert">definition or inference</span> 
 	as an ordered list, the scope of the variables in each rule is at the level of list elements, and so reuse of 
 	variable names in different rules does not affect the meaning.
 </p>
 <div id="optional-identifiers-and-attributes" class="section">
-  <h3><span class="secno">4.1 </span>Optional Identifiers and Attributes</h3>
-
-  <p>Many PROV relation statements have an identifier, identifying a
+  <h3><span class="secno"><span class="delete">4.1</span><span class="insert">5.1</span> </span>Optional Identifiers and Attributes</h3>
+
+  <span class="delete">Many PROV relation statements have an identifier, identifying a
   link between two or more related objects.  Identifiers can sometimes
-  be omitted in [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-O">PROV-O</a></cite>] notation.  For the purpose of inference and
+  be omitted in [</span><span class="delete">PROV-O</span><span class="delete">] notation.  For the purpose of inference and
   validity checking, we generate special identifiers called
-  <dfn id="dfn-existential-variables">existential variables</dfn> denoting the unknown values.
-</p>
-<p>
-Existential variables can be <a title="substitution" href="#dfn-substitution" class="internalDFN">substituted</a>
+  </span><span class="delete">existential variables</span><span class="delete"> denoting the unknown values.
+</span>
+<span class="delete">
+Existential variables can be </span><span class="delete">substituted</span><span class="delete">
   with other terms.  Specifically, a
-  <dfn id="dfn-substitution">substitution</dfn> is a function from a set of existential
-  variables to identifiers, literals, the placeholder <span class="name">-</span>,
-  or other <a href="#dfn-existential-variables" class="internalDFN">existential variables</a>.  A substitution <span class="math">S</span> can be
-  applied to an instance <span class="math">I</span> by replacing all occurrences of existential
-  variables <span class="math">x</span> in the instance with <span class="math">S(x)</span>.  
-</p>
+  </span><span class="delete">substitution</span><span class="delete"> is a function from a set of existential
+  variables to identifiers, literals, the placeholder </span><span class="delete">-</span><span class="delete">,
+  or other </span><span class="delete">existential variables</span><span class="delete">.  A substitution </span><span class="delete">S</span><span class="delete"> can be
+  applied to an instance </span><span class="delete">I</span><span class="delete"> by replacing all occurrences of existential
+  variables </span><span class="delete">x</span><span class="delete"> in the instance with </span><span class="delete">S(x)</span><span class="delete">.  
+</span>
+
+
+
+
 
 
 <p>
@@ -2623,7 +2776,7 @@
 
  <div class="remark">
   <p>Definitions  <a class="rule-ref" href="#optional-identifiers"><span>Definition 1 (optional-identifiers)</span></a> and <a class="rule-ref" href="#optional-attributes"><span>Definition 2 (optional-attributes)</span></a>.  
-do not apply to <span class="name">alternateOf</span>, <span class="name">specializationOf</span>, and <span class="name">mentionOf</span>, which do not have identifiers and attributes.
+do not apply to <span class="name">alternateOf</span><span class="delete">,</span><span class="insert"> and</span> <span class="name">specializationOf<span class="delete">, and </span><span class="delete">mentionOf</span></span>, which do not have identifiers and attributes.
 </p>
  </div>
 
@@ -2663,8 +2816,9 @@
 
   <p>
 There are no expansion rules for entity, agent, communication,
- attribution, influence, alternate, specialization, or mention
-   relations, because these
+ attribution, influence, alternate, <span class="delete">specialization, </span>or <span class="delete">mention
+   </span><span class="insert">specialization 
+   </span>relations, because these
  have no optional parameters aside from the identifier and attributes,
  which are expanded by the rules in <a class="rule-ref" href="#optional-identifiers"><span>Definition 1 (optional-identifiers)</span></a> and <a class="rule-ref" href="#optional-attributes"><span>Definition 2 (optional-attributes)</span></a>.  </p>
    </div>
@@ -2767,7 +2921,7 @@
 The rationale for this is that when a is provided, then there have to be two events, namely <span class="name">u</span> and <span class="name">g</span>, which account for the usage of <span class="name">e1</span> and the generation of <span class="name">e2</span>, respectively, by <span class="name">a</span>. Conversely, if <span class="name">a</span> is not provided, then one cannot tell whether one or more activities are involved in the derivation, and the explicit introduction of such events, which correspond to a single <span class="delete">acitivity,</span><span class="insert">activity,</span> would therefore not be justified.  </p>
 
 
-<p>  A  later constraint, <a class="rule-ref" href="#impossible-unspecified-derivation-generation-use"><span>Constraint 53 (impossible-unspecified-derivation-generation-use)</span></a>,
+<p>  A  later constraint, <a class="rule-ref" href="#impossible-unspecified-derivation-generation-use"><span>Constraint <span class="delete">53</span><span class="insert">51</span> (impossible-unspecified-derivation-generation-use)</span></a>,
   forbids specifying generation and use parameters when the activity
   is unspecified.</p>
     
@@ -2777,7 +2931,7 @@
    IF</span> there exists <span class="name">t1</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t2</span> <em class="rfc2119" title="may">may</em> be a placeholder.
   </li>
 <li>  <span class="name">activity(id,t1,-,attrs)</span> <span class="conditional">IF AND ONLY
-   IF</span> there exists <span class="name">t2</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t1</span> <em class="rfc2119" title="must not">must not</em> be a placeholder.
+   IF</span> there exists <span class="name">t2</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t1</span> <span class="delete">must not</span><em class="rfc2119" title="may"><span class="insert">may</span></em> be a placeholder.
 </li>
 
     <li>For each  <span class="name">r</span> in { 
@@ -2801,11 +2955,11 @@
     such that <span class="name">r(a<sub>0</sub>;...,a<sub>i-1</sub>,a',a<sub>i+1</sub>,...,a<sub>n</sub>)</span>.
     </p></li>
   <li>If <span class="name">a</span> is not the placeholder <span class="name">-</span>, and <span class="name">u</span> is any term, then the following definition holds:
-   <p> <span class="name">wasDerivedFrom(id;e2,e1,a,-,u,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">g</span>
+   <p> <span class="name"><span class="delete">wasDerivedFrom(id;e2,e1,a,-,u,attrs)</span><span class="insert">wasDerivedFrom(id; e2,e1,a,-,u,attrs)</span></span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">g</span>
     such that <span class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</span>.</p></li>
   <li>If <span class="name">a</span> is not the placeholder <span class="name">-</span>, and <span class="name">g</span> is any term,
     then the following definition holds:
-   <p> <span class="name">wasDerivedFrom(id;e2,e1,a,g,-,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">u</span>
+   <p> <span class="name"><span class="delete">wasDerivedFrom(id;e2,e1,a,g,-,attrs)</span><span class="insert">wasDerivedFrom(id; e2,e1,a,g,-,attrs)</span></span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">u</span>
     such that <span class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</span>.</p></li></ol>
     </div>
 
@@ -2829,7 +2983,7 @@
 </div>
     
 <div id="entities-and-activities" class="section">
-  <h3><span class="secno">4.2 </span>Entities and Activities</h3>
+  <h3><span class="secno"><span class="delete">4.2</span><span class="insert">5.2</span> </span>Entities and Activities</h3>
 
 
   
@@ -2956,7 +3110,7 @@
 </div>
 
  <div id="derivations" class="section"> 
-<h3><span class="secno">4.3 </span>Derivations</h3>
+<h3><span class="secno"><span class="delete">4.3</span><span class="insert">5.3</span> </span>Derivations</h3>
 
 
 <hr>
@@ -2999,7 +3153,7 @@
 
 
 <div id="agents" class="section">
-<h3><span class="secno">4.4 </span>Agents</h3>
+<h3><span class="secno"><span class="delete">4.4</span><span class="insert">5.4</span> </span>Agents</h3>
 
 <p id="attribution-inference_text"> Attribution is the ascribing of an entity to an agent.  An
 entity can only be ascribed to an agent if the agent was associated with
@@ -3119,13 +3273,14 @@
 
 
  <div id="alternate-and-specialized-entities" class="section"> 
-<h3><span class="secno">4.5 </span>Alternate and Specialized Entities</h3>
+<h3><span class="secno"><span class="delete">4.5</span><span class="insert">5.5</span> </span>Alternate and Specialized Entities</h3>
 
 
 
   
 <hr>
-  <p id="alternate-reflexive_text">The relation <span class="name">alternateOf</span> is an <a href="#dfn-equivalence-relation" class="internalDFN">equivalence relation</a>: that is,
+  <p id="alternate-reflexive_text">The relation <span class="name">alternateOf</span> is an <a href="#dfn-equivalence-relation" class="internalDFN">equivalence relation</a><span class="delete">:</span><span class="insert"> om
+  entities:</span> that is,
   it is <a href="#dfn-reflexive" class="internalDFN">reflexive</a>,
   <a href="#dfn-transitive" class="internalDFN">transitive</a> and <a href="#dfn-symmetric" class="internalDFN">symmetric</a>.  As a consequence, the
   following inferences can be applied:</p>
@@ -3166,7 +3321,7 @@
 <p id="specialization-transitive_text">
 Similarly, specialization is a
     <a href="#dfn-strict-partial-order" class="internalDFN">strict partial order</a>: it is <a href="#dfn-irreflexive" class="internalDFN">irreflexive</a> and
-    <a href="#dfn-transitive" class="internalDFN">transitive</a>.  Irreflexivity is handled later as <a class="rule-ref" href="#impossible-specialization-reflexive"><span>Constraint 54 (impossible-specialization-reflexive)</span></a>
+    <a href="#dfn-transitive" class="internalDFN">transitive</a>.  Irreflexivity is handled later as <a class="rule-ref" href="#impossible-specialization-reflexive"><span>Constraint <span class="delete">54</span><span class="insert">52</span> (impossible-specialization-reflexive)</span></a>
     </p>
        <div class="inference" id="specialization-transitive"><div class="ruleTitle"><a class="internalDFN" href="#specialization-transitive">Inference 19 (specialization-transitive)</a></div>
 <p>
@@ -3203,20 +3358,25 @@
 
 
   
-  <hr>
-
-  <div class="note">
-<p>Note: The following inference is associated with a feature "<a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">at risk</a>" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</p>
-</div>
-
-
-    <p id="mention-specialization-inference_text">If one entity is a mention of another in a bundle, then the former is also a specialization of the latter:</p>
+  
+
+  
+<span class="delete">Note: The following inference is associated with a feature "</span><span class="delete">at risk</span><span class="delete">" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</span>
+
+
+
+    <span class="delete">If one entity is a mention of another in a bundle, then the former is also a specialization of the latter:</span>
     
-       <div class="inference" id="mention-specialization-inference"><div class="ruleTitle"><a class="internalDFN" href="#mention-specialization-inference">Inference 22 (mention-specialization-inference)</a></div>
-<p>
-<span class="conditional">IF</span> <span class="name">mentionOf(e2,e1,b)</span> <span class="conditional">THEN</span> <span class="name">specializationOf(e2,e1)</span>.</p>
-    </div> 
-
+       <span class="delete">Inference 22 (mention-specialization-inference)</span>
+
+<span class="delete">IF</span> <span class="delete">mentionOf(e2,e1,b)</span> <span class="delete">THEN</span> <span class="delete">specializationOf(e2,e1)</span><span class="delete">.</span>
+     
+
+
+
+
+
+  
 
 </div>
 
@@ -3229,7 +3389,7 @@
 
 
 <div id="constraints" class="section">
-<h2><span class="secno">5. </span>Constraints</h2>
+<h2><span class="secno"><span class="delete">5.</span><span class="insert">6.</span> </span>Constraints</h2>
 
 
 
@@ -3237,7 +3397,7 @@
 <p>
 This section defines a collection of constraints on PROV instances.
 There are three kinds of constraints:
-  </p><ul><li><em>uniqueness constraints</em> that say that a <a>PROV
+  </p><ul><li><em>uniqueness constraints</em> that say that a <a href="#instance" class="internalDFN">PROV
   instance</a> can contain at most one statement of each kind with a
     given identifier. For
   example, if we describe the same generation event twice, then the
@@ -3254,7 +3414,7 @@
     patterns of statements in <a href="#dfn-valid" class="internalDFN">valid</a> PROV instances.
     </li></ul>
   
-  <p>As in a [definition|inference], term symbols such as <span class="name">id</span>, 
+  <p>As in a <span class="delete">[definition|inference],</span><span class="insert">definition or inference,</span> term symbols such as <span class="name">id</span>, 
 	<span class="name">start</span>, <span class="name">end</span>, <span class="name">e</span>, 
 	<span class="name">a</span>, <span class="name">attrs</span> in a constraint,
 	are assumed to be variables unless otherwise specified.  These variables are scoped at 
@@ -3267,7 +3427,7 @@
 
 
  
-  <h3><span class="secno">5.1 </span>Uniqueness Constraints</h3>
+  <h3><span class="secno"><span class="delete">5.1</span><span class="insert">6.1</span> </span>Uniqueness Constraints</h3>
 
 
     
@@ -3282,55 +3442,45 @@
     <span class="name">activity(a,2011-11-16T16:00:00,_t1,[a=1])</span> and <span class="name">activity(a,_t2,2011-11-16T18:00:00,[b=2])</span>, with existential variables <span class="name">_t1</span> and <span class="name">_t2</span>.  The <a>merge</a> of
     these two statements (describing the same activity <span class="name">a</span>) is <span class="name">activity(a,2011-11-16T16:00:00,2011-11-16T18:00:00,[a=1,b=2])</span>.  </p>
 
-    <p> <span class="delete">Merging</span><dfn id="dfn-unification"><span class="insert">Unification</span></dfn> is an operation that can be applied
-   to a pair of <span class="delete">terms, or a pair of attribute lists.</span><span class="insert">terms.</span>
-   The result of <span class="delete">merging</span><span class="insert">unification</span> is either a <dfn id="dfn-unifier"><span class="insert">unifier</span></dfn><span class="insert">, that is,
-   a </span>substitution <span class="delete">(mapping</span><span class="math"><span class="insert">S</span></span><span class="insert"> such that </span><span class="math"><span class="insert">S(t)</span>
-   <span class="delete">existentially quantified variables to terms)</span><span class="insert">= S(t')</span></span><span class="insert">,</span> or failure, indicating 
-   that <span class="delete">the merge
-   cannot be performed.  Merging</span><span class="insert">there is no </span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert">. Unification</span> of pairs of <span class="delete">terms, attribute lists,
-   or statements</span><span class="insert">terms</span> is defined as follows.</p>
-
-    <ul>
-      <li> If <span class="name">t</span> and <span class="name">t'</span> are constant identifiers or values
-      (including the placeholder <span class="name">-</span>), then
-   <span class="insert">
-      there are two cases.  If </span><span class="name"><span class="insert">t = t'</span></span><span class="insert"> then </span>their <span class="delete">merge</span><span class="delete"> exists only if they are equal,</span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a><span class="insert"> is the
-      empty substitution,</span> otherwise <span class="delete">merging</span><span class="insert">unification</span>
-fails.  </li>
-   <li> If <span class="name">x</span> is an existential variable
+     <span class="delete">Merging</span><span class="delete"> is an operation that can be applied
+   to a pair of terms, or a pair of attribute lists.
+   The result of merging is either a substitution (mapping
+   existentially quantified variables to terms) or failure, indicating that the merge
+   cannot be performed.  Merging of pairs of terms, attribute lists,
+   or statements is defined as follows.</span>
+
+    
+      <span class="delete"> If </span><span class="delete">t</span><span class="delete"> and </span><span class="delete">t'</span><span class="delete"> are constant identifiers or values
+      (including the placeholder </span><span class="delete">-</span><span class="delete">), then
+   their </span><span class="delete">merge</span><span class="delete"> exists only if they are equal, otherwise merging
+fails.  </span>
+   <span class="delete"> If </span><span class="delete">x</span><span class="delete"> is an existential variable
       and 
-   <span class="name">t'</span> is any term (identifier, constant,
-      placeholder <span class="name">-</span>, or
+   </span><span class="delete">t'</span><span class="delete"> is any term (identifier, constant,
+      placeholder </span><span class="delete">-</span><span class="delete">, or
       existential variable), then their
-   <span class="delete">merge</span><span class="delete"> is </span><span class="delete">t'</span><span class="delete">, and the resulting substitution</span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a> is
-      <span class="name">[x=t']</span>.  In the special case where 
-      <span class="name">t'=x</span>, the<span class="delete"> merge</span>  <a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a> is
-      <span class="delete">x</span><span class="delete"> and the resulting substitution is empty.</span><span class="insert"> the empty substitution.</span></li>
-         <li> If <span class="name">t</span> is any term (identifier, constant,
-      placeholder <span class="name">-</span>, or
+   </span><span class="delete">merge</span><span class="delete"> is </span><span class="delete">t'</span><span class="delete">, and the resulting substitution is
+      </span><span class="delete">[x=t']</span><span class="delete">.  In the special case where </span><span class="delete">t'=x</span><span class="delete">, the merge is
+      </span><span class="delete">x</span><span class="delete"> and the resulting substitution is empty.</span>
+         <span class="delete"> If </span><span class="delete">t</span><span class="delete"> is any term (identifier, constant,
+      placeholder </span><span class="delete">-</span><span class="delete">, or
       existential variable) and
-   <span class="name">x'</span> is an existential variable, then their
-      <span class="delete">merge</span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a> is the same as the <span class="delete">merge</span><a href="#dfn-unifier" class="internalDFN"><span class="insert">unifier</span></a> of <span class="name">x</span> 
-      and <span class="name">t</span>.</li>
-  <span class="delete"> The </span><span class="delete">merge</span><span class="delete"> of two attribute lists  </span><span class="delete">attrs1</span><span class="delete"> and  </span><span class="delete">attrs2</span>
-   
-      </ul>
-      
-
-
-<div class="remark"><span class="insert">Unification </span>is <span class="delete">their union, considered as sets of key-value pairs, written  </span><span class="delete">attrs1 ∪ attrs2</span><span class="delete">.  Duplicate keys</span><span class="insert">analogous to unification in
-  logic programming and theorem proving, restricted to flat terms</span> with<span class="delete">
+   </span><span class="delete">x'</span><span class="delete"> is an existential variable, then their
+      merge is the same as the merge of </span><span class="delete">x</span><span class="delete"> and </span><span class="delete">t</span><span class="delete">.</span>
+  <span class="delete"> The </span><span class="delete">merge</span><span class="delete"> of two attribute lists  </span><span class="delete">attrs1</span><span class="delete"> and  </span><span class="delete">attrs2</span><span class="delete">
+   is their union, considered as sets of key-value pairs, written  </span><span class="delete">attrs1 ∪ attrs2</span><span class="delete">.  Duplicate keys with
       different  are
-      allowed,</span><span class="insert">
-constants and variables</span> but<span class="delete"> equal key-value pairs are merged.</span>
+      allowed, but equal key-value pairs are merged.</span>
 
 
 
 <span class="delete">Merging for terms is analogous to unification in
   logic programming and theorem proving, restricted to flat terms with
-  </span>   no function symbols.  No occurs check is needed because there are no
-  function symbols.</div>
+  no function symbols.  No occurs check is needed because there are no
+  function symbols.</span>
+
+  
+
 
   <p>
 A typical uniqueness constraint is as follows:
@@ -3405,7 +3555,7 @@
   This is enforced through
   the following key constraints:
   </p>
-  <div class="constraint" id="key-object"><div class="ruleTitle"><a class="internalDFN" href="#key-object">Constraint 23 (key-object)</a></div>
+  <div class="constraint" id="key-object"><div class="ruleTitle"><a class="internalDFN" href="#key-object">Constraint <span class="delete">23</span><span class="insert">22</span> (key-object)</a></div>
 <p></p><ol>
   <li>The identifier field <span class="delete">e</span><a href="http://www.w3.org/TR/prov-dm/#entity.id"><span class="name"><span class="insert">id</span></span></a> is a <span class="conditional">KEY</span> for
   the <span class="name"><span class="delete">entity(e,attrs)</span><span class="insert">entity(id,attrs)</span></span> statement.
@@ -3426,7 +3576,7 @@
    constraints require that all of the information about each identified
    statement can be merged into a single, consistent statement:
   </p>
-  <div class="constraint" id="key-properties"><div class="ruleTitle"><a class="internalDFN" href="#key-properties">Constraint 24 (key-properties)</a></div>
+  <div class="constraint" id="key-properties"><div class="ruleTitle"><a class="internalDFN" href="#key-properties">Constraint <span class="delete">24</span><span class="insert">23</span> (key-properties)</a></div>
 <p></p><ol>
   <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#generation.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
   the <span class="name">wasGeneratedBy(id; e,a,t,attrs)</span> statement.
@@ -3446,24 +3596,33 @@
   <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#invalidation.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
   the <span class="name">wasInvalidatedBy(id; e,a,t,attrs)</span> statement.
   </li>
-
-  
-  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#derivation.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
-  the <span class="name">wasDerivedFrom(id;  e2, e1, a, g2, u1, attrs)</span> statement.
-  </li>
- <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#attribution.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
-  the <span class="name">wasAttributedTo(id; e,ag,attr)</span> statement.
+  <li><span class="insert">The identifier field </span><a href="http://www.w3.org/TR/prov-dm/#derivation.id"><span class="name"><span class="insert">id</span></span></a><span class="insert"> is a </span><span class="conditional"><span class="insert">KEY</span></span><span class="insert"> for
+  the </span><span class="name"><span class="insert">wasDerivedFrom(id;  e2, e1, a, g2, u1, attrs)</span></span><span class="insert"> statement.
+  </span></li>
+ <li><span class="insert">The identifier field </span><a href="http://www.w3.org/TR/prov-dm/#attribution.id"><span class="name"><span class="insert">id</span></span></a><span class="insert"> is a </span><span class="conditional"><span class="insert">KEY</span></span><span class="insert"> for
+  the </span><span class="name"><span class="insert">wasAttributedTo(id; e,ag,attr)</span></span><span class="insert"> statement.
+  </span></li>
+  <li><span class="insert">The identifier field </span><a href="http://www.w3.org/TR/prov-dm/#association.id"><span class="name"><span class="insert">id</span></span></a><span class="insert"> is a </span><span class="conditional"><span class="insert">KEY</span></span><span class="insert"> for
+  the </span><span class="name"><span class="insert">wasAssociatedWith(id; a,ag,pl,attrs)</span></span><span class="insert"> statement.
+ </span></li>
+
+  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#delegation.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
+  the <span class="name"><span class="delete">wasDerivedFrom(id;  e2, e1, a, g2, u1, attrs)</span><span class="insert">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span></span> statement.
   </li>
-  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#association.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
-  the <span class="name">wasAssociatedWith(id; a,ag,pl,attrs)</span> statement.
- </li>
-  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#association.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
-  the <span class="name">wasAssociatedWith(id; a,ag,-,attrs)</span> statement.
-  </li>
-  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#delegation.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
-  the <span class="name">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span> statement.
-  </li>
-  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#influence.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
+ 
+  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#influence.id"><span class="name">id</span><span class="delete"> is a </span><span class="delete">KEY</span><span class="delete"> for
+  the </span><span class="delete">wasAttributedTo(id; e,ag,attr)</span><span class="delete"> statement.
+  </span>
+  <span class="delete">The identifier field </span><span class="delete">id</span><span class="delete"> is a </span><span class="delete">KEY</span><span class="delete"> for
+  the </span><span class="delete">wasAssociatedWith(id; a,ag,pl,attrs)</span><span class="delete"> statement.
+ </span>
+  <span class="delete">The identifier field </span><span class="delete">id</span><span class="delete"> is a </span><span class="delete">KEY</span><span class="delete"> for
+  the </span><span class="delete">wasAssociatedWith(id; a,ag,-,attrs)</span><span class="delete"> statement.
+  </span>
+  <span class="delete">The identifier field </span><span class="delete">id</span><span class="delete"> is a </span><span class="delete">KEY</span><span class="delete"> for
+  the </span><span class="delete">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span><span class="delete"> statement.
+  </span>
+  <span class="delete">The identifier field </span><span class="delete">id</span></a> is a <span class="conditional">KEY</span> for
   the <span class="name">wasInfluencedBy(id; o2,o1,attrs)</span> statement.
   </li>
 </ol>
@@ -3478,14 +3637,14 @@
 <p> Entities may have multiple generation or invalidation events
   (either or both may, however, be left implicit).  An entity can be
   generated by more than one activity, with one generation event per
-  each entity-activity pair.  These events must be simultaneous, as required by <a class="rule-ref" href="#generation-generation-ordering"><span>Constraint 41 (generation-generation-ordering)</span></a>
-  and <a class="rule-ref" href="#invalidation-invalidation-ordering"><span>Constraint 42 (invalidation-invalidation-ordering)</span></a>.
+  each entity-activity pair.  These events must be simultaneous, as required by <a class="rule-ref" href="#generation-generation-ordering"><span>Constraint <span class="delete">41</span><span class="insert">39</span> (generation-generation-ordering)</span></a>
+  and <a class="rule-ref" href="#invalidation-invalidation-ordering"><span>Constraint <span class="delete">42</span><span class="insert">40</span> (invalidation-invalidation-ordering)</span></a>.
 
 </p>
 </div>
 
 
-<div class="constraint" id="unique-generation"><div class="ruleTitle"><a class="internalDFN" href="#unique-generation">Constraint 25 (unique-generation)</a></div>
+<div class="constraint" id="unique-generation"><div class="ruleTitle"><a class="internalDFN" href="#unique-generation">Constraint <span class="delete">25</span><span class="insert">24</span> (unique-generation)</a></div>
 <p>
 <span class="conditional">IF</span> <span class="name">wasGeneratedBy(gen1; e,a,_t1,_attrs1)</span> and <span class="name">wasGeneratedBy(gen2; e,a,_t2,_attrs2)</span>,
 <span class="conditional">THEN</span> <span class="name">gen1</span> = <span class="name">gen2</span>.</p>
@@ -3496,7 +3655,7 @@
 </p><hr>
 <p id="unique-invalidation_text">
 
-</p><div class="constraint" id="unique-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#unique-invalidation">Constraint 26 (unique-invalidation)</a></div>
+</p><div class="constraint" id="unique-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#unique-invalidation">Constraint <span class="delete">26</span><span class="insert">25</span> (unique-invalidation)</a></div>
 <p>
 <span class="conditional">IF</span> <span class="name">wasInvalidatedBy(inv1; e,a,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(inv2; e,a,_t2,_attrs2)</span>,
 <span class="conditional">THEN</span> <span class="name">inv1</span> = <span class="name">inv2</span>.</p>
@@ -3531,18 +3690,18 @@
 That is, an activity may be started by
 several other activities, with shared or separate triggering
 entities.  If an activity is started or ended by multiple events, they must all
-be simultaneous, as specified in <a class="rule-ref" href="#start-start-ordering"><span>Constraint 33 (start-start-ordering)</span></a>
-and <a class="rule-ref" href="#end-end-ordering"><span>Constraint 34 (end-end-ordering)</span></a>.
+be simultaneous, as specified in <a class="rule-ref" href="#start-start-ordering"><span>Constraint <span class="delete">33</span><span class="insert">31</span> (start-start-ordering)</span></a>
+and <a class="rule-ref" href="#end-end-ordering"><span>Constraint <span class="delete">34</span><span class="insert">32</span> (end-end-ordering)</span></a>.
 </p>
 
-<div class="constraint" id="unique-wasStartedBy"><div class="ruleTitle"><a class="internalDFN" href="#unique-wasStartedBy">Constraint 27 (unique-wasStartedBy)</a></div>
+<div class="constraint" id="unique-wasStartedBy"><div class="ruleTitle"><a class="internalDFN" href="#unique-wasStartedBy">Constraint <span class="delete">27</span><span class="insert">26</span> (unique-wasStartedBy)</a></div>
 <p>
 <span class="conditional">IF</span> <span class="name">wasStartedBy(start1; a,_e1,a0,_t1,_attrs1)</span> and <span class="name">wasStartedBy(start2; a,_e2,a0,_t2,_attrs2)</span>,  <span class="conditional">THEN</span> <span class="name">start1</span> = <span class="name">start2</span>.</p>
 </div> 
 
 <p id="unique-wasEndedBy_text">
 
-</p><div class="constraint" id="unique-wasEndedBy"><div class="ruleTitle"><a class="internalDFN" href="#unique-wasEndedBy">Constraint 28 (unique-wasEndedBy)</a></div>
+</p><div class="constraint" id="unique-wasEndedBy"><div class="ruleTitle"><a class="internalDFN" href="#unique-wasEndedBy">Constraint <span class="delete">28</span><span class="insert">27</span> (unique-wasEndedBy)</a></div>
 <p>
 <span class="conditional">IF</span> <span class="name">wasEndedBy(end1; a,_e1,a0,_t1,_attrs1)</span> and <span class="name">wasEndedBy(end2; a,_e2,a0,_t2,_attrs2)</span>,  <span class="conditional">THEN</span> <span class="name">end1</span> = <span class="name">end2</span>.</p>
 </div> 
@@ -3557,7 +3716,7 @@
  <p id="unique-startTime_text">An <a href="#dfn-start-event" class="internalDFN">activity start event</a> is the <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> that marks the instant an activity starts. It allows for an optional time attribute.  <span id="optional-start-time">Activities also allow for an optional start time attribute.  If both are specified, they <em class="rfc2119" title="must">must</em> be the same, as expressed by the following constraint.</span>
 </p>
 
-<div class="constraint" id="unique-startTime"><div class="ruleTitle"><a class="internalDFN" href="#unique-startTime">Constraint 29 (unique-startTime)</a></div>
+<div class="constraint" id="unique-startTime"><div class="ruleTitle"><a class="internalDFN" href="#unique-startTime">Constraint <span class="delete">29</span><span class="insert">28</span> (unique-startTime)</a></div>
 <p>
 <span class="conditional">IF</span> <span class="name">activity(a2,t1,_t2,_attrs)</span> and <span class="name">wasStartedBy(_start; a2,_e,_a1,t,_attrs)</span>,  <span class="conditional">THEN</span> <span class="name">t1</span>=<span class="name">t</span>.</p>
 </div> 
@@ -3567,7 +3726,7 @@
 <p id="unique-endTime_text">An <a href="#dfn-end-event" class="internalDFN">activity end event</a> is the <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> that marks the instant an activity ends. It allows for an optional time attribute.  <span id="optional-end-time">Activities also allow for an optional end time attribute.  If both are specified, they <em class="rfc2119" title="must">must</em> be the same, as expressed by the following constraint.</span>
 </p>
 
-<div class="constraint" id="unique-endTime"><div class="ruleTitle"><a class="internalDFN" href="#unique-endTime">Constraint 30 (unique-endTime)</a></div>
+<div class="constraint" id="unique-endTime"><div class="ruleTitle"><a class="internalDFN" href="#unique-endTime">Constraint <span class="delete">30</span><span class="insert">29</span> (unique-endTime)</a></div>
 <p>
 <span class="conditional">IF</span> <span class="name">activity(a2,_t1,t2,_attrs)</span> and <span class="name">wasEndedBy(_end; a2,_e,_a1,t,_attrs1)</span>,  <span class="conditional">THEN</span> <span class="name">t2</span> = <span class="name">t</span>.</p>
 </div> 
@@ -3578,21 +3737,28 @@
 </p><hr>
 
 
-<div class="note">
-<p>Note: The following constraint is associated with a feature "<a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">at risk</a>" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</p>
-</div>
+
+<span class="delete">Note: The following constraint is associated with a feature "</span><span class="delete">at risk</span><span class="delete">" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</span>
+
   
 
-<div id="unique-mention_text">
-<p>An entity can be the subject of at most one mention relation.</p>
-</div>
-
-
-<div class="constraint" id="unique-mention"><div class="ruleTitle"><a class="internalDFN" href="#unique-mention">Constraint 31 (unique-mention)</a></div>
-<p>
-<span class="conditional">IF</span> <span class="name">mentionOf(e, e1, b1)</span> and <span class="name">mentionOf(e, e2, b2)</span>,
-<span class="conditional">THEN</span>  <span class="name">e1</span>=<span class="name">e2</span> and <span class="name">b1</span>=<span class="name">b2</span>.</p>
-</div> 
+
+<span class="delete">An entity can be the subject of at most one mention relation.</span>
+
+
+
+<span class="delete">Constraint 31 (unique-mention)</span>
+
+<span class="delete">IF</span> <span class="delete">mentionOf(e, e1, b1)</span><span class="delete"> and </span><span class="delete">mentionOf(e, e2, b2)</span><span class="delete">,
+</span><span class="delete">THEN</span>  <span class="delete">e1</span><span class="delete">=</span><span class="delete">e2</span><span class="delete"> and </span><span class="delete">b1</span><span class="delete">=</span><span class="delete">b2</span><span class="delete">.</span>
+ 
+
+
+
+
+
+
+
 
 
 
@@ -3601,7 +3767,7 @@
 </div>  
 
 <div id="event-ordering-constraints" class="section">
-<h3><span class="secno">5.2 </span>Event Ordering Constraints</h3>
+<h3><span class="secno"><span class="delete">5.2</span><span class="insert">6.2</span> </span>Event Ordering Constraints</h3>
 
 
 <p>Given that provenance consists of a description of past entities
@@ -3626,7 +3792,7 @@
 <p>Specifically, <dfn id="dfn-precedes">precedes</dfn> is a <a href="#dfn-preorder" class="internalDFN">preorder</a>
 between <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous events</a>.  A
 constraint of the form
-<span class="name">e1</span> precedes <span class="name">e2</span> means that <span class="name">e1</span>
+<span class="name">e1</span> <a href="#dfn-precedes" class="internalDFN">precedes</a> <span class="name">e2</span> means that <span class="name">e1</span>
 happened at the same time as or before <span class="name">e2</span>.
 For symmetry, <dfn id="dfn-follows">follows</dfn> is defined as the
 inverse of <a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>; that is, a constraint of
@@ -3674,7 +3840,7 @@
 
 
 <div id="activity-constraints" class="section">
-<h4><span class="secno">5.2.1 </span>Activity constraints</h4>
+<h4><span class="secno"><span class="delete">5.2.1</span><span class="insert">6.2.1</span> </span>Activity constraints</h4>
 
 <p>
 This section specifies ordering constraints from the perspective of
@@ -3699,13 +3865,17 @@
 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" href="#dfn-event" class="internalDFN">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 class="note"> Miscellaneous suggestions about figures
+  <span class="delete"> Miscellaneous suggestions about figures
   (originally from Tim Lebo):
-<ul>
-  <li>
-    I think it would help if the "corresponding edges between entities and activities" where the same visual style as the vertical line marking the time the Usage, generation and derivation occurred. A matching visual style provides a Gestalt that matches the concept. I am looking at subfigures b and c in 5.2. </li></ul>
-  </div>
-
+</span>
+  <span class="delete">
+    I think it would help if the "corresponding edges between entities and activities" where the same visual style as the vertical line marking the time the Usage, generation and derivation occurred. A matching visual style provides a Gestalt that matches the concept. I am looking at subfigures b and c in 5.2. </span>
+  
+
+  
+
+
+  
   <div style="text-align: center;">
 
 <span class="figure" id="ordering-activity">
@@ -3724,9 +3894,9 @@
 event</a> always <a href="#dfn-precedes" class="internalDFN">precedes</a> the corresponding <a href="#dfn-end-event" class="internalDFN">activity end
 event</a>.  This is illustrated by
 <a href="#ordering-activity">Figure 3</a>
-(a) and expressed by <a class="rule-ref" href="#start-precedes-end"><span>Constraint 32 (start-precedes-end)</span></a>.</p>
-
-<div class="constraint" id="start-precedes-end"><div class="ruleTitle"><a class="internalDFN" href="#start-precedes-end">Constraint 32 (start-precedes-end)</a></div>
+(a) and expressed by <a class="rule-ref" href="#start-precedes-end"><span>Constraint <span class="delete">32</span><span class="insert">30</span> (start-precedes-end)</span></a>.</p>
+
+<div class="constraint" id="start-precedes-end"><div class="ruleTitle"><a class="internalDFN" href="#start-precedes-end">Constraint <span class="delete">32</span><span class="insert">30</span> (start-precedes-end)</a></div>
 <p>
 <span class="conditional">IF</span>
 <span class="name">wasStartedBy(start; a,_e1,_a1,_t1,_attrs1)</span> 
@@ -3749,7 +3919,7 @@
 other.  Using this constraint in both directions means that each event
 <a href="#dfn-precedes" class="internalDFN">precedes</a> the other.
 </p>
-<div class="constraint" id="start-start-ordering"><div class="ruleTitle"><a class="internalDFN" href="#start-start-ordering">Constraint 33 (start-start-ordering)</a></div>
+<div class="constraint" id="start-start-ordering"><div class="ruleTitle"><a class="internalDFN" href="#start-start-ordering">Constraint <span class="delete">33</span><span class="insert">31</span> (start-start-ordering)</a></div>
  <p>
     <span class="conditional">IF</span>
 <span class="name">wasStartedBy(start1; a,_e1,_a1,_t1,_attrs1)</span> 
@@ -3771,7 +3941,7 @@
 other.  Using this constraint in both directions means that each event
 <a href="#dfn-precedes" class="internalDFN">precedes</a> the other, that is, they are simultaneous.
 </p>
-<div class="constraint" id="end-end-ordering"><div class="ruleTitle"><a class="internalDFN" href="#end-end-ordering">Constraint 34 (end-end-ordering)</a></div>
+<div class="constraint" id="end-end-ordering"><div class="ruleTitle"><a class="internalDFN" href="#end-end-ordering">Constraint <span class="delete">34</span><span class="insert">32</span> (end-end-ordering)</a></div>
  <p>
     <span class="conditional">IF</span>
 <span class="name">wasEndedBy(end1; a,_e1,_a1,_t1,_attrs1)</span> 
@@ -3787,9 +3957,9 @@
 <hr>
 
 <p id="usage-within-activity_text">A usage implies ordering of <a title="instantaneous event" href="#dfn-event" class="internalDFN">events</a>, since the <a title="entity usage event" href="#dfn-usage-event" class="internalDFN">usage event</a> had to occur during the associated activity. This is
-illustrated by <a href="#ordering-activity">Figure 3</a> (b) and  expressed by <a class="rule-ref" href="#usage-within-activity"><span>Constraint 35 (usage-within-activity)</span></a>.</p>
-
-<div class="constraint" id="usage-within-activity"><div class="ruleTitle"><a class="internalDFN" href="#usage-within-activity">Constraint 35 (usage-within-activity)</a></div>
+illustrated by <a href="#ordering-activity">Figure 3</a> (b) and  expressed by <a class="rule-ref" href="#usage-within-activity"><span>Constraint <span class="delete">35</span><span class="insert">33</span> (usage-within-activity)</span></a>.</p>
+
+<div class="constraint" id="usage-within-activity"><div class="ruleTitle"><a class="internalDFN" href="#usage-within-activity">Constraint <span class="delete">35</span><span class="insert">33</span> (usage-within-activity)</a></div>
 <ol>
     <li>
   <span class="conditional">IF</span>
@@ -3820,9 +3990,9 @@
 
 
 <p id="generation-within-activity_text">A generation implies ordering of <a title="instantaneous event" href="#dfn-event" class="internalDFN">events</a>, since the <a title="entity generation event" href="#dfn-generation-event" class="internalDFN">generation event</a> had to occur during the associated activity. This is
-illustrated by <a href="#ordering-activity">Figure 3</a> (c) and  expressed by <a class="rule-ref" href="#generation-within-activity"><span>Constraint 36 (generation-within-activity)</span></a>.</p> 
-
-<div class="constraint" id="generation-within-activity"><div class="ruleTitle"><a class="internalDFN" href="#generation-within-activity">Constraint 36 (generation-within-activity)</a></div>
+illustrated by <a href="#ordering-activity">Figure 3</a> (c) and  expressed by <a class="rule-ref" href="#generation-within-activity"><span>Constraint <span class="delete">36</span><span class="insert">34</span> (generation-within-activity)</span></a>.</p> 
+
+<div class="constraint" id="generation-within-activity"><div class="ruleTitle"><a class="internalDFN" href="#generation-within-activity">Constraint <span class="delete">36</span><span class="insert">34</span> (generation-within-activity)</a></div>
    <ol>
     <li>
   <span class="conditional">IF</span>
@@ -3859,9 +4029,9 @@
 follow the end event of <span class="name">a2</span>. This is
 illustrated by
 <a href="#ordering-activity">Figure 3</a>
-(d) and expressed by <a class="rule-ref" href="#wasInformedBy-ordering"><span>Constraint 37 (wasInformedBy-ordering)</span></a>.</p>
-
-<div class="constraint" id="wasInformedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasInformedBy-ordering">Constraint 37 (wasInformedBy-ordering)</a></div>
+(d) and expressed by <a class="rule-ref" href="#wasInformedBy-ordering"><span>Constraint <span class="delete">37</span><span class="insert">35</span> (wasInformedBy-ordering)</span></a>.</p>
+
+<div class="constraint" id="wasInformedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasInformedBy-ordering">Constraint <span class="delete">37</span><span class="insert">35</span> (wasInformedBy-ordering)</a></div>
 <p>
   <span class="conditional">IF</span>
 <span class="name">wasInformedBy(_id; a2,a1,_attrs)</span> 
@@ -3882,10 +4052,15 @@
 </p></div>
 
 <div id="entity-constraints" class="section">
-<h4><span class="secno">5.2.2 </span> Entity constraints</h4>
-
-
-<div class="note">The figure(s) in this section should have vertical lines with visual styles that match the diagonal arrow that they go with. </div>
+<h4><span class="secno"><span class="delete">5.2.2</span><span class="insert">6.2.2</span> </span> Entity constraints</h4>
+
+
+<span class="delete">The figure(s) in this section should have vertical lines with visual styles that match the diagonal arrow that they go with. </span>
+
+
+
+
+
 
 <p>
 As with activities, entities have lifetimes: they are generated, then
@@ -3914,7 +4089,7 @@
 explicitly here to cover the case of an entity that is generated and
 invalidated without being used.)</p>
 
-<div class="constraint" id="generation-precedes-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#generation-precedes-invalidation">Constraint 38 (generation-precedes-invalidation)</a></div>
+<div class="constraint" id="generation-precedes-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#generation-precedes-invalidation">Constraint <span class="delete">38</span><span class="insert">36</span> (generation-precedes-invalidation)</a></div>
 <p>
  <span class="conditional">IF</span>
 <span class="name">wasGeneratedBy(gen; e,_a1,_t1,_attrs1)</span> 
@@ -3935,9 +4110,9 @@
 <p id="generation-precedes-usage_text"> 
 A usage and a generation for a given entity implies ordering of <a title="instantaneous event" href="#dfn-event" class="internalDFN">events</a>, since the <a title="entity generation
 event" href="#dfn-generation-event" class="internalDFN">generation event</a> had to precede the <a title="entity usage event" href="#dfn-usage-event" class="internalDFN">usage event</a>. This is
-illustrated by <a href="#ordering-entity">Figure 4</a>(a) and  expressed by <a class="rule-ref" href="#generation-precedes-usage"><span>Constraint 39 (generation-precedes-usage)</span></a>.</p>
-
-<div class="constraint" id="generation-precedes-usage"><div class="ruleTitle"><a class="internalDFN" href="#generation-precedes-usage">Constraint 39 (generation-precedes-usage)</a></div>
+illustrated by <a href="#ordering-entity">Figure 4</a>(a) and  expressed by <a class="rule-ref" href="#generation-precedes-usage"><span>Constraint <span class="delete">39</span><span class="insert">37</span> (generation-precedes-usage)</span></a>.</p>
+
+<div class="constraint" id="generation-precedes-usage"><div class="ruleTitle"><a class="internalDFN" href="#generation-precedes-usage">Constraint <span class="delete">39</span><span class="insert">37</span> (generation-precedes-usage)</a></div>
 <p>  <span class="conditional">IF</span>
 <span class="name">wasGeneratedBy(gen; e,_a1,_t1,_attrs1)</span> 
 and
@@ -3952,9 +4127,9 @@
 
 <hr>
 
-<p id="usage-precedes-invalidation_text">All usages of an entity precede its invalidation, which is captured by <a class="rule-ref" href="#usage-precedes-invalidation"><span>Constraint 40 (usage-precedes-invalidation)</span></a> (without any explicit graphical representation).</p> 
-
-<div class="constraint" id="usage-precedes-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#usage-precedes-invalidation">Constraint 40 (usage-precedes-invalidation)</a></div>
+<p id="usage-precedes-invalidation_text">All usages of an entity precede its invalidation, which is captured by <a class="rule-ref" href="#usage-precedes-invalidation"><span>Constraint <span class="delete">40</span><span class="insert">38</span> (usage-precedes-invalidation)</span></a> (without any explicit graphical representation).</p> 
+
+<div class="constraint" id="usage-precedes-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#usage-precedes-invalidation">Constraint <span class="delete">40</span><span class="insert">38</span> (usage-precedes-invalidation)</a></div>
 <p>
 <span class="conditional">IF</span>
 <span class="name">used(use; _a1,e,_t1,_attrs1)</span> 
@@ -3966,7 +4141,7 @@
 <span class="name">inv</span>.</p>
 </div>
 
-<hr>
+
 
 
 <hr>
@@ -3978,7 +4153,7 @@
 other.  Using this constraint in both directions means that each event
 <a href="#dfn-precedes" class="internalDFN">precedes</a> the other.
 </p>
-<div class="constraint" id="generation-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#generation-generation-ordering">Constraint 41 (generation-generation-ordering)</a></div>
+<div class="constraint" id="generation-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#generation-generation-ordering">Constraint <span class="delete">41</span><span class="insert">39</span> (generation-generation-ordering)</a></div>
  <p>
     <span class="conditional">IF</span>
 <span class="name">wasGeneratedBy(gen1; e,_a1,_t1,_attrs1)</span> 
@@ -4000,7 +4175,7 @@
 other.  Using this constraint in both directions means that each event
 <a href="#dfn-precedes" class="internalDFN">precedes</a> the other, that is, they are simultaneous.
 </p>
-<div class="constraint" id="invalidation-invalidation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#invalidation-invalidation-ordering">Constraint 42 (invalidation-invalidation-ordering)</a></div>
+<div class="constraint" id="invalidation-invalidation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#invalidation-invalidation-ordering">Constraint <span class="delete">42</span><span class="insert">40</span> (invalidation-invalidation-ordering)</a></div>
  <p>
     <span class="conditional">IF</span>
 <span class="name">wasInvalidatedBy(inv1; e,_a1,_t1,_attrs1)</span> 
@@ -4021,10 +4196,10 @@
 First, we consider derivations, where the activity and usage are known. In that case, the <a title="entity usage event" href="#dfn-usage-event" class="internalDFN">usage</a> of <span class="name">e1</span> has to precede the <a title="entity generation
 event" href="#dfn-generation-event" class="internalDFN">generation</a> of <span class="name">e2</span>.
 This is
-illustrated by <a href="#ordering-entity-fig">Figure 4</a> (b) and  expressed by  <a class="rule-ref" href="#derivation-usage-generation-ordering"><span>Constraint 43 (derivation-usage-generation-ordering)</span></a>.</p>
-
-
-<div class="constraint" id="derivation-usage-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#derivation-usage-generation-ordering">Constraint 43 (derivation-usage-generation-ordering)</a></div>
+illustrated by <a href="#ordering-entity-fig">Figure 4</a> (b) and  expressed by  <a class="rule-ref" href="#derivation-usage-generation-ordering"><span>Constraint <span class="delete">43</span><span class="insert">41</span> (derivation-usage-generation-ordering)</span></a>.</p>
+
+
+<div class="constraint" id="derivation-usage-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#derivation-usage-generation-ordering">Constraint <span class="delete">43</span><span class="insert">41</span> (derivation-usage-generation-ordering)</a></div>
   <p>
   In this constraint, <span class="name">_a</span>, <span class="name">gen2</span>, <span class="name">use1</span> <em class="rfc2119" title="must not">must not</em> be placeholders.</p>
 <p>
@@ -4042,11 +4217,11 @@
 <p id="derivation-generation-generation-ordering_text">
 When the activity, generation or usage is unknown, a similar constraint exists, except that the constraint refers to its
 generation event, as
-illustrated by <a href="#ordering-entity-fig">Figure 4</a> (c) and  expressed by <a class="rule-ref" href="#derivation-generation-generation-ordering"><span>Constraint 44 (derivation-generation-generation-ordering)</span></a>.</p>
-
-<div class="constraint" id="derivation-generation-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#derivation-generation-generation-ordering">Constraint 44 (derivation-generation-generation-ordering)</a></div>
+illustrated by <a href="#ordering-entity-fig">Figure 4</a> (c) and  expressed by <a class="rule-ref" href="#derivation-generation-generation-ordering"><span>Constraint <span class="delete">44</span><span class="insert">42</span> (derivation-generation-generation-ordering)</span></a>.</p>
+
+<div class="constraint" id="derivation-generation-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#derivation-generation-generation-ordering">Constraint <span class="delete">44</span><span class="insert">42</span> (derivation-generation-generation-ordering)</a></div>
   <p>
-In this constraint, any <span class="name">_a</span>, <span class="name">_g</span>, <span class="name">_u</span> <em class="rfc2119" title="may">may</em> be placeholders.</p>
+In this constraint, any<span class="insert"> of</span> <span class="name">_a</span>, <span class="name">_g</span>, <span class="name">_u</span> <em class="rfc2119" title="may">may</em> be placeholders.</p>
 <p>
  <span class="conditional">IF</span>
 <span class="name">wasDerivedFrom(_d; e2,e1,_a,_g,_u,attrs)</span>
@@ -4080,10 +4255,10 @@
 <p id="wasStartedBy-ordering_text">
 The entity that triggered the start of an activity must exist before the activity starts.
 This is
-illustrated by <a href="#ordering-entity-trigger">Figure 5</a>(a) and  expressed by <a class="rule-ref" href="#wasStartedBy-ordering"><span>Constraint 45 (wasStartedBy-ordering)</span></a>.</p>
-
-
-<div class="constraint" id="wasStartedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasStartedBy-ordering">Constraint 45 (wasStartedBy-ordering)</a></div>
+illustrated by <a href="#ordering-entity-trigger">Figure 5</a>(a) and  expressed by <a class="rule-ref" href="#wasStartedBy-ordering"><span>Constraint <span class="delete">45</span><span class="insert">43</span> (wasStartedBy-ordering)</span></a>.</p>
+
+
+<div class="constraint" id="wasStartedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasStartedBy-ordering">Constraint <span class="delete">45</span><span class="insert">43</span> (wasStartedBy-ordering)</a></div>
  <ol>
     <li>
     <span class="conditional">IF</span>
@@ -4115,7 +4290,7 @@
 <a href="#ordering-entity-trigger">Figure 5</a>(b).</p>
 
 
-<div class="constraint" id="wasEndedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasEndedBy-ordering">Constraint 46 (wasEndedBy-ordering)</a></div>
+<div class="constraint" id="wasEndedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasEndedBy-ordering">Constraint <span class="delete">46</span><span class="insert">44</span> (wasEndedBy-ordering)</a></div>
  <ol>
       <li>
     <span class="conditional">IF</span>
@@ -4153,7 +4328,7 @@
 specific entity must have been generated after the
 less specific entity was generated.
 </p>
-<div class="constraint" id="specialization-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#specialization-generation-ordering">Constraint 47 (specialization-generation-ordering)</a></div>
+<div class="constraint" id="specialization-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#specialization-generation-ordering">Constraint <span class="delete">47</span><span class="insert">45</span> (specialization-generation-ordering)</a></div>
   <p>
 <span class="conditional">IF</span> <span class="name">specializationOf(e2,e1)</span> and <span class="name">wasGeneratedBy(gen1; e1,_a1,_t1,_attrs1)</span> and
   <span class="name">wasGeneratedBy(gen2; e2,_a2,_t2,_attrs2)</span>
@@ -4168,7 +4343,7 @@
 then
 the invalidation event of the more specific entity precedes that of
 the less specific entity.
-</p><div class="constraint" id="specialization-invalidation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#specialization-invalidation-ordering">Constraint 48 (specialization-invalidation-ordering)</a></div>
+</p><div class="constraint" id="specialization-invalidation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#specialization-invalidation-ordering">Constraint <span class="delete">48</span><span class="insert">46</span> (specialization-invalidation-ordering)</a></div>
   <p>
 <span class="conditional">IF</span> <span class="name">specializationOf(e1,e2)</span> and
  <span class="name">wasInvalidatedBy(inv1; e1,_a1,_t1,_attrs1)</span> and 
@@ -4180,7 +4355,7 @@
 </div>
 
 <div id="agent-constraints" class="section">
-<h4><span class="secno">5.2.3 </span> Agent constraints</h4>
+<h4><span class="secno"><span class="delete">5.2.3</span><span class="insert">6.2.3</span> </span> Agent constraints</h4>
 
 <p> Like entities and activities, agents have lifetimes that follow a
 familiar pattern.  An agent that is also an entity can be generated
@@ -4207,11 +4382,11 @@
 associated with an agent must have some overlap with the agent. The
 agent <em class="rfc2119" title="must">must</em> have been generated (or started), or <em class="rfc2119" title="must">must</em> have become
 associated with the activity, after the activity start: so, the agent <em class="rfc2119" title="must">must</em> exist before the activity end. Likewise, the agent may be destructed (or ended), or may terminate its association with the activity, before the activity end: hence, the agent invalidation (or end) is required to happen after the activity start.
-This is illustrated by <a href="#ordering-agents">Figure 6</a> (a) and  expressed by <a class="rule-ref" href="#wasAssociatedWith-ordering"><span>Constraint 49 (wasAssociatedWith-ordering)</span></a>.</p>
-
-
-
-<div class="constraint" id="wasAssociatedWith-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasAssociatedWith-ordering">Constraint 49 (wasAssociatedWith-ordering)</a></div>
+This is illustrated by <a href="#ordering-agents">Figure 6</a> (a) and  expressed by <a class="rule-ref" href="#wasAssociatedWith-ordering"><span>Constraint <span class="delete">49</span><span class="insert">47</span> (wasAssociatedWith-ordering)</span></a>.</p>
+
+
+
+<div class="constraint" id="wasAssociatedWith-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasAssociatedWith-ordering">Constraint <span class="delete">49</span><span class="insert">47</span> (wasAssociatedWith-ordering)</a></div>
   <p>
 In the following inferences, <span class="name">_pl</span> <em class="rfc2119" title="may">may</em> be
  a placeholder <span class="name">-</span>.
@@ -4270,12 +4445,12 @@
 
 <p id="wasAttributedTo-ordering_text">An agent to which an entity was attributed, <em class="rfc2119" title="must">must</em> exist before this entity was generated.
 This is
-illustrated by <a href="#ordering-agents">Figure 6</a> (b) and  expressed by  <a class="rule-ref" href="#wasAttributedTo-ordering"><span>Constraint 50 (wasAttributedTo-ordering)</span></a>.</p>
+illustrated by <a href="#ordering-agents">Figure 6</a> (b) and  expressed by  <a class="rule-ref" href="#wasAttributedTo-ordering"><span>Constraint <span class="delete">50</span><span class="insert">48</span> (wasAttributedTo-ordering)</span></a>.</p>
 
 
 
  
-<div class="constraint" id="wasAttributedTo-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasAttributedTo-ordering">Constraint 50 (wasAttributedTo-ordering)</a></div>
+<div class="constraint" id="wasAttributedTo-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasAttributedTo-ordering">Constraint <span class="delete">50</span><span class="insert">48</span> (wasAttributedTo-ordering)</a></div>
       <ol> <li>
     <span class="conditional">IF</span>
 <span class="name">wasAttributedTo(_at; e,ag,_attrs)</span> 
@@ -4308,7 +4483,7 @@
 <p id="actedOnBehalfOf-ordering_text">For delegation, <span class="delete">two agents need</span><span class="insert">the responsible agent has</span> to <span class="insert">precede or </span>have some overlap <span class="delete">in their lifetime.</span><span class="insert">with the subordinate agent.</span></p>
 
 
-<div class="constraint" id="actedOnBehalfOf-ordering"><div class="ruleTitle"><a class="internalDFN" href="#actedOnBehalfOf-ordering">Constraint 51 (actedOnBehalfOf-ordering)</a></div>
+<div class="constraint" id="actedOnBehalfOf-ordering"><div class="ruleTitle"><a class="internalDFN" href="#actedOnBehalfOf-ordering">Constraint <span class="delete">51</span><span class="insert">49</span> (actedOnBehalfOf-ordering)</a></div>
  <ol> <li>
 	 <span class="conditional">IF</span>
 <span class="name">actedOnBehalfOf(_del; ag2,ag1,_a,_attrs)</span> 
@@ -4343,12 +4518,17 @@
 
 
 <div id="type-constraints" class="section">
-<h3><span class="secno">5.3 </span>Type Constraints</h3>
-
-<p id="typing_text">The following rule  establishes types denoted by identifiers from their use within expressions. 
+<h3><span class="secno"><span class="delete">5.3</span><span class="insert">6.3</span> </span>Type Constraints</h3>
+
+<p id="typing_text">The following <span class="delete">rule  establishes</span><span class="insert">rules assign</span> types <span class="delete">denoted by</span><span class="insert">to</span> identifiers<span class="delete"> from</span><span class="insert">
+based on</span> their use within <span class="delete">expressions.</span><span class="insert">statements.</span> 
 The function <span class="name">typeOf</span> gives the set of types denoted by an identifier.
-That is,  <span class="name">typeOf(e)</span> returns the set of types associated with identifier  <span class="name">e</span>. The function <span class="name">typeOf</span> is not a term of PROV, but a construct introduced to validate PROV statements. 
-</p>
+That is,  <span class="name">typeOf(e)</span> returns the set of types 
+associated with identifier  <span class="name">e</span>. The function 
+<span class="name">typeOf</span> is not a <span class="delete">term of</span><span class="insert">PROV statement, but a
+construct used only during validation</span> PROV, <span class="delete">but a construct introduced</span><span class="insert">similar</span> to <span class="delete">validate PROV statements. 
+</span><a href="#dfn-precedes" class="internalDFN"><span class="insert">precedes</span></a><span class="insert">.
+</span></p>
 
 
 
@@ -4360,18 +4540,18 @@
  (e.g. <span class="name">'prov:EmptyCollection'</span> is a subtype of <span class="name">'prov:Collection'</span>) or because certain types are not
  disjoint (such as <span class="name">'agent'</span> and <span class="name">'entity'</span>). The set of types
  does not reflect all of the distinctions among objects, only those
- relevant for checking validity.  In particular, subtypes such as <span class="name">'plan'</span> and <span class="name">'bundle'</span> are omitted, and statements such as <span class="name">wasAssociatedWith</span> and <span class="name">mentionOf</span> that have plan or bundle parameters only check that these parameters are entities.
+ relevant for checking validity.  In particular, <span class="delete">subtypes</span><span class="insert">a subtype</span> such as <span class="name">'plan'</span> <span class="delete">and </span><span class="delete">'bundle'</span><span class="delete"> are</span><span class="insert">is</span> omitted, and statements such as <span class="name">wasAssociatedWith</span> <span class="delete">and </span><span class="delete">mentionOf</span> that have plan<span class="delete"> or bundle</span> parameters only check that these parameters are entities.
 </p>
 
 <p>To check if a PROV instance satisfies type constraints, one obtains the types of identifiers by application of
-<a class="rule-ref" href="#typing"><span>Constraint 52 (typing)</span></a>
+<a class="rule-ref" href="#typing"><span>Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</span></a>
 and check that none of the impossibility constraints 
-<a class="rule-ref" href="#entity-activity-disjoint"><span>Constraint 57 (entity-activity-disjoint)</span></a> and
-<a class="rule-ref" href="#membership-empty-collection"><span>Constraint 58 (membership-empty-collection)</span></a> are
+<a class="rule-ref" href="#entity-activity-disjoint"><span>Constraint <span class="delete">57</span><span class="insert">55</span> (entity-activity-disjoint)</span></a> and
+<a class="rule-ref" href="#membership-empty-collection"><span>Constraint <span class="delete">58</span><span class="insert">56</span> (membership-empty-collection)</span></a> are
   violated as a result.</p>
 
 
-<div class="constraint" id="typing"><div class="ruleTitle"><a class="internalDFN" href="#typing">Constraint 52 (typing)</a></div>
+<div class="constraint" id="typing"><div class="ruleTitle"><a class="internalDFN" href="#typing">Constraint <span class="delete">52</span><span class="insert">50</span> (typing)</a></div>
 
 
 <ol>
@@ -4518,29 +4698,37 @@
 <span class="name">'entity' ∈ typeOf(e1)</span>.
 
 
+
+
+
+
+
 </li><li>
+
+
 <span class="conditional">IF</span> 
-   <span class="name">mentionOf(e2,e1,b)</span>  
+   <span class="name"><span class="delete">mentionOf(e2,e1,b)</span><span class="insert">hadMember(c,e)</span></span>  
 <span class="conditional">THEN</span> 
-<span class="name">'entity' ∈ typeOf(e2)</span> AND
-<span class="name">'entity' ∈ typeOf(e1)</span> AND
-<span class="name">'entity' ∈ typeOf(b)</span>.
+<span class="name"><span class="insert">'prov:Collection' ∈ typeOf(c)</span></span><span class="insert"> AND
+</span><span class="name">'entity' ∈ <span class="delete">typeOf(e2)</span><span class="insert">typeOf(c)</span></span> AND
+<span class="name">'entity' ∈ <span class="delete">typeOf(e1)</span><span class="delete"> AND
+</span><span class="delete">'entity' ∈ typeOf(b)</span><span class="insert">typeOf(e)</span></span>.
 
 
 </li><li>
 
 <span class="conditional">IF</span> 
-   <span class="name">hadMember(c,e)</span>  
-<span class="conditional">THEN</span> 
-<span class="name">'prov:Collection' ∈ typeOf(c)</span> AND
-<span class="name">'entity' ∈ typeOf(c)</span> AND
-<span class="name">'entity' ∈ typeOf(e)</span>.
-
-
-</li><li>
-
-<span class="conditional">IF</span> 
-   <span class="name">entity(c,[prov:type='prov:EmptyCollection'])</span>  
+   <span class="name"><span class="delete">hadMember(c,e)</span>  
+<span class="delete">THEN</span> 
+<span class="delete">'prov:Collection' ∈ typeOf(c)</span><span class="delete"> AND
+</span><span class="delete">'entity' ∈ typeOf(c)</span><span class="delete"> AND
+</span><span class="delete">'entity' ∈ typeOf(e)</span><span class="delete">.
+
+
+</span>
+
+<span class="delete">IF</span> 
+   entity(c,[prov:type='prov:EmptyCollection'])</span>  
 <span class="conditional">THEN</span> 
 <span class="name">'entity' ∈ typeOf(c)</span>  AND
 <span class="name">'prov:Collection' ∈ typeOf(c)</span>AND
@@ -4552,7 +4740,7 @@
 </div> 
 
 <div id="impossibility-constraints" class="section">
-<h3><span class="secno">5.4 </span>Impossibility constraints</h3>
+<h3><span class="secno"><span class="delete">5.4</span><span class="insert">6.4</span> </span>Impossibility constraints</h3>
 
 <p> Impossibility constraints require that certain patterns of
 statements never appear in <a href="#dfn-valid" class="internalDFN">valid</a> PROV instances.  Impossibility
@@ -4577,7 +4765,7 @@
     are unspecified.  It is forbidden to specify a generation or use
     event without specifying the activity.</p>
 
-        <div class="constraint" id="impossible-unspecified-derivation-generation-use"><div class="ruleTitle"><a class="internalDFN" href="#impossible-unspecified-derivation-generation-use">Constraint 53 (impossible-unspecified-derivation-generation-use)</a></div>
+        <div class="constraint" id="impossible-unspecified-derivation-generation-use"><div class="ruleTitle"><a class="internalDFN" href="#impossible-unspecified-derivation-generation-use">Constraint <span class="delete">53</span><span class="insert">51</span> (impossible-unspecified-derivation-generation-use)</a></div>
 <p> In the following rules, <span class="name">g</span> and <span class="name">u</span> <em class="rfc2119" title="must not">must not</em> be <span class="name">-</span>.</p>
 	  <ol>
   <li> <span class="conditional">IF</span>
@@ -4596,7 +4784,7 @@
     <a href="#dfn-strict-partial-order" class="internalDFN">strict partial order</a>: it is <a href="#dfn-irreflexive" class="internalDFN">irreflexive</a> and
     <a href="#dfn-transitive" class="internalDFN">transitive</a>.</p>
 
-        <div class="constraint" id="impossible-specialization-reflexive"><div class="ruleTitle"><a class="internalDFN" href="#impossible-specialization-reflexive">Constraint 54 (impossible-specialization-reflexive)</a></div>
+        <div class="constraint" id="impossible-specialization-reflexive"><div class="ruleTitle"><a class="internalDFN" href="#impossible-specialization-reflexive">Constraint <span class="delete">54</span><span class="insert">52</span> (impossible-specialization-reflexive)</a></div>
 
 	  <p> <span class="conditional">IF</span> <span class="name">specializationOf(e,e)</span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
     </div>
@@ -4611,7 +4799,7 @@
    <p id="impossible-property-overlap_text"> Furthermore,  identifiers
    of basic relationships are disjoint.
   </p>
-  <div class="constraint" id="impossible-property-overlap"><div class="ruleTitle"><a class="internalDFN" href="#impossible-property-overlap">Constraint 55 (impossible-property-overlap)</a></div>
+  <div class="constraint" id="impossible-property-overlap"><div class="ruleTitle"><a class="internalDFN" href="#impossible-property-overlap">Constraint <span class="delete">55</span><span class="insert">53</span> (impossible-property-overlap)</a></div>
   <p>
 For each <span class="name">r</span> and <span class="name">s</span>
    in { 
@@ -4656,7 +4844,7 @@
    <p id="impossible-object-property-overlap_text"> Identifiers of entities,
   agents and activities cannot also be identifiers of properties.
   </p>
-  <div class="constraint" id="impossible-object-property-overlap"><div class="ruleTitle"><a class="internalDFN" href="#impossible-object-property-overlap">Constraint 56 (impossible-object-property-overlap)</a></div>
+  <div class="constraint" id="impossible-object-property-overlap"><div class="ruleTitle"><a class="internalDFN" href="#impossible-object-property-overlap">Constraint <span class="delete">56</span><span class="insert">54</span> (impossible-object-property-overlap)</a></div>
   <p>
 For each <span class="name">p</span> in {<span class="name">entity</span>, <span class="name">activity</span>
    or <span class="name">agent</span>} and for each  <span class="name">r</span> in { 
@@ -4685,7 +4873,7 @@
    <p id="entity-activity-disjoint_text">   The set of entities and activities are disjoint, expressed by 
   the following constraint:
   </p>
-  <div class="constraint" id="entity-activity-disjoint"><div class="ruleTitle"><a class="internalDFN" href="#entity-activity-disjoint">Constraint 57 (entity-activity-disjoint)</a></div>
+  <div class="constraint" id="entity-activity-disjoint"><div class="ruleTitle"><a class="internalDFN" href="#entity-activity-disjoint">Constraint <span class="delete">57</span><span class="insert">55</span> (entity-activity-disjoint)</a></div>
 
     
 <p>
@@ -4700,7 +4888,7 @@
 	  Similarly, there is no disjointness between activities and
  agents, and one can assert both <span class="name">activity(a1)</span> and <span class="name">agent(a1)</span> in a valid PROV instance. 
  However, one should keep in mind that some specific types of agents may not be suitable as activities. 
- For example, asserting statements such as <span class="name">agent(Bob, [type=prov:Person])</span> and <span class="name">activity(Bob)</span> is discouraged. In these cases, disjointness can be ensured by explicitly asserting the agent as both agent and entity, and applying <a class="rule-ref" href="#entity-activity-disjoint"><span>Constraint 57 (entity-activity-disjoint)</span></a>.
+ For example, asserting statements such as <span class="name">agent(Bob, [type=prov:Person])</span> and <span class="name">activity(Bob)</span> is discouraged. In these cases, disjointness can be ensured by explicitly asserting the agent as both agent and entity, and applying <a class="rule-ref" href="#entity-activity-disjoint"><span>Constraint <span class="delete">57</span><span class="insert">55</span> (entity-activity-disjoint)</span></a>.
   </div>
 
 
@@ -4708,7 +4896,7 @@
    <p id="membership-empty-collection_text"> An empty collection cannot contain any member, expressed by
   the following constraint:
   </p>
-  <div class="constraint" id="membership-empty-collection"><div class="ruleTitle"><a class="internalDFN" href="#membership-empty-collection">Constraint 58 (membership-empty-collection)</a></div>
+  <div class="constraint" id="membership-empty-collection"><div class="ruleTitle"><a class="internalDFN" href="#membership-empty-collection">Constraint <span class="delete">58</span><span class="insert">56</span> (membership-empty-collection)</a></div>
 <p> <span class="conditional">IF</span> 
  <span class="name">hasMember(c,e)</span> and
 <span class="name">'prov:EmptyCollection' ∈ typeOf(c)</span>
@@ -4723,7 +4911,7 @@
 </div> 
 
   <div id="normalization-validity-equivalence" class="section">
-<h2><span class="secno">6. </span>Normalization, Validity, and Equivalence</h2>
+<h2><span class="secno"><span class="delete">6.</span><span class="insert">7.</span> </span>Normalization, Validity, and Equivalence</h2>
 
 
   <p>We define the notions of <a title="normal form" href="#dfn-normal-form" class="internalDFN">normalization</a>, <a title="valid" href="#dfn-valid" class="internalDFN">validity</a> and
@@ -4731,11 +4919,12 @@
 for PROV instances and then extend them to PROV documents.</p>
 
 <div id="instance" class="section">
-  <h3><span class="secno">6.1 </span>Instances</h3>
+  <h3><span class="secno"><span class="delete">6.1</span><span class="insert">7.1</span> </span>Instances</h3>
   
 <div class="remark">
-  Implementations should decide up front what reasoning about
-  co-reference should be applied, and rewrite the instance (by
+  <span class="delete">Implementations</span><span class="insert">Before normalization or validation, implementations</span> should <span class="delete">decide up front what</span><span class="insert">expand
+  namespace prefixes and  perform any appropriate</span> reasoning about
+  co-reference <span class="delete">should be applied,</span><span class="insert">of identifiers,</span> and rewrite the instance (by
   replacing co-referent identifiers with a single common identifier) to
   make this explicit, before doing validation, equivalence checking,
   or normalization.
@@ -4747,7 +4936,7 @@
 
 <p> We define the <dfn id="dfn-normal-form">normal form</dfn> of a PROV instance as the set
 of provenance statements resulting from applying all definitions,
-  inferences, and uniqueness constraints.</p>
+  inferences, and uniqueness <span class="delete">constraints.</span><span class="insert">constraints, obtained as follows:</span></p>
 
 
 
@@ -4772,18 +4961,19 @@
     <li>If no definitions, inferences, or uniqueness constraints can be applied to instance <span class="math">I<sub>3</sub></span>, then <span class="math">I<sub>3</sub></span> is the
     normal form of <span class="math">I</span>.</li>
     <li>Otherwise, the normal form of <span class="math">I</span> is the same as the normal form
-    of <span class="math">I<sub>3</sub></span> (that is, proceed by recursively normalizing <span class="math">I<sub>3</sub></span>).
+    of <span class="math">I<sub>3</sub></span> (that is, proceed by<span class="delete"> recursively </span>
+    normalizing <span class="math">I<sub>3</sub></span><span class="delete">).</span><span class="insert"> at step 1).</span>
  </li></ol>
  
 <p>Because of the potential interaction among definitions, inferences, and
-  constraints, the above algorithm is recursive.  Nevertheless,
+  constraints, the above algorithm is <span class="delete">recursive.</span><span class="insert">iterative.</span>  Nevertheless,
   all of our constraints fall into a class of <a>tuple-generating
   dependencies</a> and <a>equality-generating dependencies</a> that
   satisfy a termination condition called <a>weak acyclicity</a> that
   has been studied in the context of relational databases
   [<cite><a class="bibref" rel="biblioentry" href="#bib-DBCONSTRAINTS">DBCONSTRAINTS</a></cite>].  Therefore, the above algorithm terminates, independently
   of the order in which inferences and constraints are applied.
-  <a href="#termination">Appendix C</a> gives a proof that normalization terminates and produces
+  <a href="#termination">Appendix <span class="delete">C</span><span class="insert">A</span></a> gives a proof that normalization terminates and produces
   a unique (up to isomorphism) normal form.
 </p>
   
@@ -4797,7 +4987,8 @@
   validity:</p>
 
 <ol>
-  <li>Normalize the instance <span class="math">I</span>, obtaining normalized instance <span class="math">I'</span>.  If
+  <li>Normalize the instance <span class="math">I</span>, obtaining<span class="delete"> normalized instance</span><span class="insert">
+  normal form</span> <span class="math">I'</span>.  If
   normalization fails, then <span class="math">I</span> is not <a href="#dfn-valid" class="internalDFN">valid</a>.
   </li>
   <li>Apply all event ordering constraints to <span class="math">I'</span> to build a graph <span class="math">G</span> whose nodes
@@ -4818,15 +5009,14 @@
   </ol>
 
 <p>A normal form of a PROV instance does not exist when a uniqueness 
-  constraint fails due to<span class="insert"> unification or</span> merging failure. </p>
-
-
-  <p>Two PROV instances <span class="math"><span class="insert">I</span></span><span class="insert"> and </span><span class="math"><span class="insert">I'</span></span><span class="insert"> are </span><dfn id="dfn-isomorphic"><span class="insert">isomorphic</span></dfn><span class="insert"> if
-  there exists an invertible substitution </span><span class="math"><span class="insert">S</span></span><span class="insert"> that maps each
-  variable of </span><span class="math"><span class="insert">I</span></span><span class="insert"> to a distinct variable of </span><span class="math"><span class="insert">I'</span></span><span class="insert"> and such that
-  </span><span class="math"><span class="insert">S(I) = I'</span></span><span class="insert">.</span></p>
-
-<p><span class="insert">  Two </span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert"> PROV instances </span>are <dfn id="dfn-equivalent">equivalent</dfn> if they 
+  constraint fails due to <span class="insert">unification or </span>merging failure. </p>
+
+
+  
+
+
+
+<p>  Two <a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a> PROV instances are <dfn id="dfn-equivalent">equivalent</dfn> if they 
   have <a href="#dfn-isomorphic" class="internalDFN">isomorphic</a> normal <span class="delete">forms (that</span><span class="insert">forms.  That</span> is, after applying all possible inference
 rules, the two instances produce the same set of PROV statements,
 up to reordering of statements and attributes within attribute lists,
@@ -4867,9 +5057,9 @@
   however, can
   change the meaning, so does not preserve equivalence.)</li>
   <li>
-  Applying inference rules, definitions, and uniqueness constraints preserves equivalence.  That is, a <a>PROV
+  Applying inference rules, definitions, and uniqueness constraints preserves equivalence.  That is, a <a href="#instance" class="internalDFN">PROV
   instance</a> is equivalent to the instance obtained by applying any
-  inference rule or definition, or by <a title="unification" href="#dfn-unification" class="internalDFN"><span class="insert">unifying</span></a><span class="insert"> two terms or </span><a href="#dfn-merging" class="internalDFN">merging</a> two statements to
+  inference rule or definition, or by <a title="unification" href="#dfn-unification" class="internalDFN"><span class="insert">unifying</span></a><span class="insert"> two terms or</span> <a href="#dfn-merging" class="internalDFN">merging</a> two statements to
   enforce a uniqueness constraint.
   </li>
   <li>Equivalence is <a href="#dfn-reflexive" class="internalDFN">reflexive</a>, <a href="#dfn-symmetric" class="internalDFN">symmetric</a>, and 
@@ -4889,37 +5079,40 @@
 </div>
 
 <div id="bundle-constraints" class="section">
-<h3><span class="secno">6.2 </span>Bundles and Documents</h3>
+<h3><span class="secno"><span class="delete">6.2</span><span class="insert">7.2</span> </span>Bundles and Documents</h3>
 
 
 <p>The definitions, inferences, and constraints, and
 the resulting notions of normalization, validity and equivalence,
-assume a PROV document that consists only of a <a>toplevel
-instance</a>, containing all PROV statements in the top level of the
-document (that is, not enclosed in a named <a>bundle</a>).  In this
+<span class="delete">assume</span><span class="insert">work on</span> a <span class="insert">single </span>PROV <span class="delete">document that consists only of a </span><span class="delete">toplevel
+instance</span><span class="delete">, containing all PROV statements in the top level of the
+document (that is, not enclosed in a named </span><span class="delete">bundle</span><span class="delete">).</span><span class="insert">instance.</span>  In this
 section, we describe how to deal with general PROV
-documents, possibly including multiple named bundles.  Briefly, each bundle is
+documents, possibly including multiple named <span class="delete">bundles.</span><span class="insert">bundles as well as a
+toplevel instance.</span>  Briefly, each bundle is
 handled independently; there is no interaction between bundles from
 the perspective of applying definitions, inferences, or constraints,
 computing normal forms, or checking validity or equivalence.</p>
 
 <p> We model a general PROV document, containing <span class="name">n</span> named bundles
 <span class="name">b<sub>1</sub>...b<sub>n</sub></span>, as a tuple
-<span class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,b<sub>n</sub>=B<sub>n</sub>])</span>
-where <span class="name">B<sub>0</sub></span> is the set of
-statements of the <a>toplevel instance</a>, and for each <span class="name">i</span>, <span class="name">B<sub>i</sub></span> is the set of
-statements of bundle <span class="name">b<sub>i</sub></span>.  Names <span class="name">b<sub>1</sub>...b<sub>n</sub></span> are assumed to be distinct.  This notation is shorthand for the
+<span class="name"><span class="delete">(B</span><span class="insert">(I</span><sub>0</sub>,[b<sub>1</sub><span class="delete">=B</span><span class="insert">=I</span><sub>1</sub>,...,b<sub>n</sub><span class="delete">=B</span><span class="insert">=I</span><sub>n</sub>])</span>
+where <span class="name"><span class="delete">B</span><span class="insert">I</span><sub>0</sub></span> is the <span class="delete">set of
+statements of the </span>toplevel<span class="delete"> instance</span><span class="insert">
+instance, and for each </span><span class="name"><span class="insert">i</span></span>, <span class="delete">and for each </span><span class="delete">i</span><span class="delete">, </span><span class="delete">B</span><span class="name"><span class="insert">I</span><sub>i</sub></span> is the <span class="delete">set of
+statements of </span><span class="insert">instance associated with
+</span>bundle <span class="name">b<sub>i</sub></span>.<span class="delete">  Names </span><span class="delete">b</span><span class="delete">1</span><span class="delete">...b</span><span class="delete">n</span><span class="delete"> are assumed to be distinct.  </span>   This notation is shorthand for the
 following PROV-N syntax:</p>
 
 <div class="name">
 <span class="delete">B</span><span class="insert">document</span><br><span class="insert">
-&nbsp;&nbsp;&nbsp;B</span><sub>0</sub><br>
+&nbsp;&nbsp;&nbsp;I</span><sub>0</sub><br>
 <span class="delete">bundle</span><span class="insert">&nbsp;&nbsp;&nbsp;bundle</span> b<sub>1</sub><br>
-<span class="delete">&nbsp;&nbsp;&nbsp;  B</span><span class="insert">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;B</span><sub>1</sub><br>
+<span class="delete">&nbsp;&nbsp;&nbsp;  B</span><span class="insert">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;I</span><sub>1</sub><br>
 <span class="delete">endBundle</span><span class="insert">&nbsp;&nbsp;&nbsp;endBundle</span><br>
 <span class="delete">...</span><span class="insert">&nbsp;&nbsp;&nbsp;...</span><br>
 <span class="delete">bundle</span><span class="insert">&nbsp;&nbsp;&nbsp;bundle</span> b<sub>n</sub><br>
-<span class="delete">&nbsp;&nbsp;&nbsp;  B</span><span class="insert">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;B</span><sub>n</sub><br>
+<span class="delete">&nbsp;&nbsp;&nbsp;  B</span><span class="insert">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;I</span><sub>n</sub><br>
 <span class="delete">endBundle</span><span class="insert">&nbsp;&nbsp;&nbsp;endBundle</span><br><span class="insert">
 endDocument</span>
 </div>
@@ -4928,18 +5121,18 @@
 
 
 <p> The <a href="#dfn-normal-form" class="internalDFN">normal form</a> of a PROV document
-<span class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,[b<sub>n</sub>=B<sub>n</sub>])</span> is <span class="name">(B'<sub>0</sub>,[b<sub>1</sub>=B'<sub>1</sub>,...,b<sub>n</sub>=B'<sub>n</sub>])</span>
-where <span class="name">B'<sub>i</sub></span> is the normal
-form of <span class="name">B<sub>i</sub></span> for each <span class="name">i</span> between 0 and <span class="name">n</span>.  </p>
-
-<p>A PROV document is <a href="#dfn-valid" class="internalDFN">valid</a> if each of the bundles <span class="name">B<sub>0</sub></span>,
-..., <span class="name">B<sub>n</sub></span> are valid and none of the bundle identifiers <span class="name">b<sub>i</sub></span> are repeated.</p>
-
-<p>Two (valid) PROV documents <span class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,b<sub>n</sub>=B<sub>n</sub>])</span> and
-<span class="name">(B'<sub>0</sub>,[b<sub>1</sub>'=B'<sub>1</sub>,...,b'<sub>m</sub>=B'<sub>m</sub>])</span> are <a href="#dfn-equivalent" class="internalDFN">equivalent</a> if <span class="name">B<sub>0</sub></span> is
-equivalent to <span class="name">B'<sub>0</sub></span> and <span class="name">n = m</span> and
+<span class="name"><span class="delete">(B</span><span class="insert">(I</span><sub>0</sub>,[b<sub>1</sub><span class="delete">=B</span><span class="insert">=I</span><sub>1</sub>,...,[b<sub>n</sub><span class="delete">=B</span><span class="insert">=I</span><sub>n</sub>])</span> is <span class="name"><span class="delete">(B'</span><span class="insert">(I'</span><sub>0</sub>,[b<sub>1</sub><span class="delete">=B'</span><span class="insert">=I'</span><sub>1</sub>,...,b<sub>n</sub><span class="delete">=B'</span><span class="insert">=I'</span><sub>n</sub>])</span>
+where <span class="name"><span class="delete">B'</span><span class="insert">I'</span><sub>i</sub></span> is the normal
+form of <span class="name"><span class="delete">B</span><span class="insert">I</span><sub>i</sub></span> for each <span class="name">i</span> between 0 and <span class="name">n</span>.  </p>
+
+<p>A PROV document is <a href="#dfn-valid" class="internalDFN">valid</a> if each of the bundles <span class="name"><span class="delete">B</span><span class="insert">I</span><sub>0</sub></span>,
+..., <span class="name"><span class="delete">B</span><span class="insert">I</span><sub>n</sub></span> are valid and none of the bundle identifiers <span class="name">b<sub>i</sub></span> are repeated.</p>
+
+<p>Two (valid) PROV documents <span class="name"><span class="delete">(B</span><span class="insert">(I</span><sub>0</sub>,[b<sub>1</sub><span class="delete">=B</span><span class="insert">=I</span><sub>1</sub>,...,b<sub>n</sub><span class="delete">=B</span><span class="insert">=I</span><sub>n</sub>])</span> and
+<span class="name"><span class="delete">(B'</span><span class="insert">(I'</span><sub>0</sub>,[b<sub>1</sub><span class="delete">'=B'</span><span class="insert">'=I'</span><sub>1</sub>,...,b'<sub>m</sub><span class="delete">=B'</span><span class="insert">=I'</span><sub>m</sub>])</span> are <a href="#dfn-equivalent" class="internalDFN">equivalent</a> if <span class="name"><span class="delete">B</span><span class="insert">I</span><sub>0</sub></span> is
+equivalent to <span class="name"><span class="delete">B'</span><span class="insert">I'</span><sub>0</sub></span> and <span class="name">n = m</span> and
 there exists a permutation <span class="name">P : {1..n} -&gt; {1..n}</span> such that for each <span class="name">i</span>, <span class="name">b<sub>i</sub> =
-b'<sub>P(i)</sub></span> and <span class="name">B<sub>i</sub></span> is equivalent to <span class="name">B'<sub>P(i)</sub></span>.
+b'<sub>P(i)</sub></span> and <span class="name"><span class="delete">B</span><span class="insert">I</span><sub>i</sub></span> is equivalent to <span class="name"><span class="delete">B'</span><span class="insert">I'</span><sub>P(i)</sub></span>.
 </p>
 
 </div> 
@@ -4958,7 +5151,7 @@
 
 
 <div class="glossary section" id="glossary"> 
-      <h2><span class="secno">7. </span>Glossary</h2>
+      <h2><span class="secno"><span class="delete">7.</span><span class="insert">8.</span> </span>Glossary</h2>
 
       <ul> 
        <li> <dfn id="dfn-antisymmetric">antisymmetric</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a href="#dfn-antisymmetric" class="internalDFN">antisymmetric</a> if
@@ -4970,14 +5163,17 @@
        <a href="#dfn-transitive" class="internalDFN">transitive</a>.</li>
        <li> <dfn id="dfn-irreflexive">irreflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a href="#dfn-irreflexive" class="internalDFN">irreflexive</a> if
       for <span class="math">x R x</span> does not hold for any element <span class="math">x</span> of <span class="math">X</span>.</li>
-        <li> <dfn id="dfn-reflexive">reflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a href="#dfn-reflexive" class="internalDFN">reflexive</a> if
-      for any element <span class="math">x</span> of <span class="math">X</span>, we have <span class="math">x R x</span>.</li>
-      <li><dfn id="dfn-partial-order">partial order</dfn>: A partial order is a relation
+         <span class="delete">reflexive</span><span class="delete">: A relation </span><span class="delete">R</span><span class="delete"> over </span><span class="delete">X</span><span class="delete"> is </span><span class="delete">reflexive</span><span class="delete"> if
+      for any element </span><span class="delete">x</span><span class="delete"> of </span><span class="delete">X</span><span class="delete">, we have </span><span class="delete">x R x</span><span class="delete">.</span>
+      
+     <li><dfn id="dfn-partial-order">partial order</dfn>: A partial order is a relation
       that is <a href="#dfn-reflexive" class="internalDFN">reflexive</a>, <a href="#dfn-antisymmetric" class="internalDFN">antisymmetric</a>, and <a href="#dfn-transitive" class="internalDFN">transitive</a>.</li>
       <li><dfn id="dfn-preorder">preorder</dfn>: A preorder is a relation that is
       <a href="#dfn-reflexive" class="internalDFN">reflexive</a> and <a href="#dfn-transitive" class="internalDFN">transitive</a>.  (It is not necessarily antisymmetric,
       meaning there can be cycles of distinct elements <span class="math">x<sub>1</sub> R x<sub>2</sub> R ... R
       x<sub>n</sub> R x<sub>1</sub>.</span></li>
+        <li> <dfn id="dfn-reflexive"><span class="insert">reflexive</span></dfn><span class="insert">: A relation </span><span class="math"><span class="insert">R</span></span><span class="insert"> over </span><span class="math"><span class="insert">X</span></span><span class="insert"> is </span><a href="#dfn-reflexive" class="internalDFN"><span class="insert">reflexive</span></a><span class="insert"> if
+      for any element </span><span class="math"><span class="insert">x</span></span><span class="insert"> of </span><span class="math"><span class="insert">X</span></span><span class="insert">, we have </span><span class="math"><span class="insert">x R x</span></span><span class="insert">.</span></li>
     <li><dfn id="dfn-strict-partial-order">strict partial order</dfn>: A strict partial order is a
       relation that is <a href="#dfn-irreflexive" class="internalDFN">irreflexive</a>, <a href="#dfn-asymmetric" class="internalDFN">asymmetric</a> and <a href="#dfn-transitive" class="internalDFN">transitive</a>.</li>
       <li><dfn id="dfn-strict-preorder">strict preorder</dfn>: A strict preorder is a relation
@@ -5034,15 +5230,17 @@
 	</tr>
 	<tr>
 	  <td>1</td>
-	  <td>19, 20, 21, 22</td>
-	  <td class="name">specializationOf, mentionOf</td>
+	  <td>19, 20, <span class="delete">21, 22</span><span class="insert">21</span></td>
+	  <td class="name"><span class="delete">specializationOf, mentionOf</span><span class="insert">specializationOf</span></td>
+	    
 	  <td class="name">specializationOf, entity</td>
 	</tr>
 	<tr>
 	  <td>2</td>
 	  <td>7, 8, 13, 14</td>
 	  <td class="name">entity, activity, wasAttributedTo, actedOnBehalfOf</td>
-	  <td class="name">wasInvalidatedBy, wasStartedBy, wasEndedBy</td>
+	  <td class="name">wasInvalidatedBy, wasStartedBy, <span class="delete">wasEndedBy</span><span class="insert">wasEndedBy,
+	wasAssociatedWith</span></td>
 	</tr>	
 	<tr>
 	  <td>3</td>
@@ -5184,6 +5382,10 @@
   <li><span class="insert">Dropped RDF as a normative reference.</span></li>
   <li><span class="insert">Made PROV-DM and PROV-N into normative references.</span></li>
   <li><span class="insert">Added "document" and "endDocument" to sec. 6.2.</span></li>
+  <li><span class="insert">Added sentence of explanation of purpose to beginning.</span></li>
+  <li><span class="insert">Moved "mention" to a separate note. </span></li>
+  <li><span class="insert">Added </span><a href="#concepts"><span class="insert">Section 4: Basic Concepts</span></a><span class="insert">.</span></li>
+  <li><span class="insert">Miscellaneous final cleanup prior to CR staging.</span></li>
 </ul>
 
 </div>
@@ -5309,17 +5511,27 @@
 
 
 
+
+
+
+
+
+
+
+
 <div id="references" class="appendix section"><h2><span class="secno"><span class="delete">C.</span><span class="insert">D.</span> </span>References</h2><div id="normative-references" class="section"><h3><span class="secno"><span class="delete">C.1</span><span class="insert">D.1</span> </span>Normative references</h3><dl class="bibliography"><dt id="bib-IRI">[IRI]</dt><dd>M. Duerst, M. Suignard. <a href="http://www.ietf.org/rfc/rfc3987.txt"><cite>Internationalized Resource Identifiers (IRI).</cite></a> January 2005. Internet RFC 3987. URL: <a href="http://www.ietf.org/rfc/rfc3986.txt">http://www.ietf.org/rfc/rfc3987.txt</a> 
-</dd><span class="delete">[RDF]</span><dt id="bib-PROV-DM"><span class="insert">[PROV-DM]</span></dt><dd><span class="insert">Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, James Cheney, Stephen Cresswell, Yolanda Gil, Paul Groth, </span>Graham <span class="delete">Klyne and Jeremy J. Carroll (eds.) </span><span class="insert">Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes </span><a href="http://www.w3.org/TR/prov-dm/"><cite><span class="delete">Resource Description Framework (RDF): Concepts and Abstract Syntax</span><span class="insert">PROV-DM: The PROV Data Model</span></cite></a>. <span class="delete">2004, W3C Recommendation.</span><span class="insert">2012, Working Draft.</span> URL: <span class="delete">http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/</span><a href="http://www.w3.org/TR/prov-dm/"><span class="insert">http://www.w3.org/TR/prov-dm/</span></a>
-</dd><dt id="bib-PROV-N"><span class="insert">[PROV-N]</span></dt><dd><span class="insert">Luc Moreau and Paolo Missier (eds.), James Cheney, Stian Soiland-Reyes </span><a href="http://www.w3.org/TR/prov-n/"><cite><span class="insert">PROV-N: The Provenance Notation</span></cite></a><span class="insert">. 2011, Working Draft. URL: </span><a href="http://www.w3.org/TR/prov-n/"><span class="insert">http://www.w3.org/TR/prov-n/</span></a>
+</dd><span class="delete">[RDF]</span><dt id="bib-PROV-DM"><span class="insert">[PROV-DM]</span></dt><dd><span class="delete">Graham Klyne and Jeremy J. Carroll (eds.) </span><span class="insert">Luc Moreau and Paolo Missier, eds. </span><a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/"><cite><span class="delete">Resource Description Framework (RDF): Concepts and Abstract Syntax</span><span class="insert">PROV-DM: The PROV Data Model</span></cite></a>. <span class="delete">2004,</span><span class="insert">11 December 2012,</span> W3C <span class="insert">Candidate </span>Recommendation. URL: <span class="delete">http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/</span><a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/"><span class="insert">http://www.w3.org/TR/2012/CR-prov-dm-20121211/</span></a>
+</dd><dt id="bib-PROV-N"><span class="insert">[PROV-N]</span></dt><dd><span class="insert">Luc Moreau and Paolo Missier, eds. </span><a href="http://www.w3.org/TR/2012/CR-prov-n-20121211/"><cite><span class="insert">PROV-N: The Provenance Notation</span></cite></a><span class="insert">. 11 December 2012, W3C Candidate Recommendation. URL: </span><a href="http://www.w3.org/TR/2012/CR-prov-n-20121211/"><span class="insert">http://www.w3.org/TR/2012/CR-prov-n-20121211/</span></a><span class="insert">.
+</span></dd><dt id="bib-PROV-O"><span class="insert">[PROV-O]</span></dt><dd><span class="insert">Timothy Lebo, Satya Sahoo, and Deborah McGuinness, eds. </span><a href="http://www.w3.org/TR/2012/CR-prov-o-20121211/"><cite><span class="insert">Provenance Formal Model</span></cite></a><span class="insert">. 11 December 2012, W3C Candidate Recommendation. URL: </span><a href="http://www.w3.org/TR/2012/CR-prov-o-20121211/"><span class="insert">http://www.w3.org/TR/2012/CR-prov-o-20121211/</span></a><span class="insert">.</span>
 </dd><dt id="bib-RFC2119">[RFC2119]</dt><dd>S. Bradner. <a href="http://www.ietf.org/rfc/rfc2119.txt"><cite>Key words for use in RFCs to Indicate Requirement Levels.</cite></a> March 1997. Internet RFC 2119.  URL: <a href="http://www.ietf.org/rfc/rfc2119.txt">http://www.ietf.org/rfc/rfc2119.txt</a> 
 </dd></dl></div><div id="informative-references" class="section"><h3><span class="secno"><span class="delete">C.2</span><span class="insert">D.2</span> </span>Informative references</h3><dl class="bibliography"><dt id="bib-CHR">[CHR]</dt><dd>Thom Frühwirth <a href="http://constraint-handling-rules.org/"><cite>Constraint        Handling Rules</cite></a>. Cambridge University Press  URL: <a href="http://constraint-handling-rules.org/">http://constraint-handling-rules.org/</a>
 </dd><dt id="bib-CLOCK">[CLOCK]</dt><dd>Lamport, L. <a href="http://research.microsoft.com/users/lamport/pubs/time-clocks.pdf"><cite>Time, clocks, and the ordering of events in a distributed system</cite></a>. Communications of the ACM 21 (7): 558–565. 1978. URL: <a href="http://research.microsoft.com/users/lamport/pubs/time-clocks.pdf">http://research.microsoft.com/users/lamport/pubs/time-clocks.pdf</a> DOI: doi:10.1145/359545.359563.
 </dd><dt id="bib-DBCONSTRAINTS">[DBCONSTRAINTS]</dt><dd> Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, and Lucian Popa  <a href="http://dx.doi.org/10.1016/j.tcs.2004.10.033"><cite>Data        exchange: Semantics and query answering</cite></a>.  Theoretical computer science 336(1):89-124   Elsevier  URL: <a href="http://dx.doi.org/10.1016/j.tcs.2004.10.033">http://dx.doi.org/10.1016/j.tcs.2004.10.033</a>
 </dd><dt id="bib-Logic">[Logic]</dt><dd>W. E. Johnson<a href="http://www.ditext.com/johnson/intro-3.html"><cite>Logic: Part III</cite></a>.1924. URL: <a href="http://www.ditext.com/johnson/intro-3.html">http://www.ditext.com/johnson/intro-3.html</a>
-</dd><span class="delete">[PROV-DM]</span><span class="delete">Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, James Cheney, Stephen Cresswell, Yolanda Gil, Paul Groth, Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes </span><span class="delete">PROV-DM: The PROV Data Model</span><span class="delete">. 2012, Working Draft. URL: </span><span class="delete">http://www.w3.org/TR/prov-dm/</span>
-<span class="delete">[PROV-N]</span><span class="delete">Luc Moreau and Paolo Missier (eds.), James Cheney, Stian Soiland-Reyes </span><span class="delete">PROV-N: The Provenance Notation</span><span class="delete">. 2011, Working Draft. URL: </span><span class="delete">http://www.w3.org/TR/prov-n/</span>
-<dt id="bib-PROV-O">[PROV-O]</dt><dd>Timothy Lebo, Satya Sahoo and Deborah McGuinness (eds.) Khalid Belhajjame, James Cheney, David Corsar, Daniel Garijo, Stian Soiland-Reyes, and Stephan Zednik <a href="http://www.w3.org/TR/prov-o/"><cite>Provenance Formal Model</cite></a>. 2011, Working Draft. URL: <a href="http://www.w3.org/TR/prov-o/">http://www.w3.org/TR/prov-o/</a>
-</dd><dt id="bib-PROV-SEM">[PROV-SEM]</dt><dd>James Cheney <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman"><cite>Formal Semantics Strawman</cite></a>. 2011, Work in progress. URL: <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman">http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman</a>
+</dd><span class="delete">[PROV-DM]</span><dt id="bib-PROV-AQ"><span class="insert">[PROV-AQ]</span></dt><dd><span class="delete">Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, James Cheney, Stephen Cresswell, Yolanda Gil,</span><span class="insert">Graham Klyne and</span> Paul Groth, <span class="delete">Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes </span><span class="insert">eds. </span><a href="http://www.w3.org/TR/2012/WD-prov-aq-20120619/"><cite><span class="delete">PROV-DM: The PROV Data Model</span><span class="insert">Provenance Access and Query</span></cite></a>. <span class="insert">19 June </span>2012, Working Draft. URL: <span class="delete">http://www.w3.org/TR/prov-dm/</span><a href="http://www.w3.org/TR/2012/WD-prov-aq-20120619/"><span class="insert">http://www.w3.org/TR/2012/WD-prov-aq-20120619/</span></a><span class="insert">.</span>
+</dd><span class="delete">[PROV-N]</span><dt id="bib-PROV-OVERVIEW"><span class="insert">[PROV-OVERVIEW]</span></dt><dd><span class="delete">Luc Moreau and Paolo Missier (eds.), James Cheney, Stian Soiland-Reyes </span><span class="insert">AUTHORS TBD. </span><a href="http://www.w3.org/TR/2012/WD-prov-overview-20121211/"><cite><span class="delete">PROV-N:</span><span class="insert">PROV-OVERVIEW:</span> The <span class="delete">Provenance Notation</span><span class="insert">PROV Family of Documents</span></cite></a>. <span class="delete">2011,</span><span class="insert">11 December 2012,</span> Working Draft. URL: <span class="delete">http://www.w3.org/TR/prov-n/</span><a href="http://www.w3.org/TR/2012/WD-prov-overview-20121211/"><span class="insert">http://www.w3.org/TR/2012/WD-prov-overview-20121211/</span></a><span class="insert">.</span>
+</dd><span class="delete">[PROV-O]</span><dt id="bib-PROV-PRIMER"><span class="insert">[PROV-PRIMER]</span></dt><dd><span class="delete">Timothy Lebo, Satya Sahoo and Deborah McGuinness (eds.) Khalid Belhajjame, James Cheney, David Corsar, Daniel Garijo, Stian Soiland-Reyes, and Stephan Zednik </span><span class="insert">Yolanda Gil and Simon Miles, eds. </span><a href="http://www.w3.org/TR/2012/WD-prov-primer-20121211/"><cite><span class="delete">Provenance Formal</span><span class="insert">Prov</span> Model<span class="insert"> Primer</span></cite></a>. <span class="delete">2011,</span><span class="insert">11 December 2012,</span> Working Draft. URL: <span class="delete">http://www.w3.org/TR/prov-o/</span><a href="http://www.w3.org/TR/2012/WD-prov-primer-20121211/"><span class="insert">http://www.w3.org/TR/2012/WD-prov-primer-20121211/</span></a><span class="insert">.</span>
+</dd><dt id="bib-PROV-SEM">[PROV-SEM]</dt><dd>James <span class="delete">Cheney</span><span class="insert">Cheney.</span> <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman"><cite>Formal Semantics Strawman</cite></a>. 2011, Work in progress. URL: <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman">http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman</a><span class="insert">.
+</span></dd><dt id="bib-PROV-XML"><span class="insert">[PROV-XML]</span></dt><dd><span class="insert">Hook Hua, Curt Tilmes, and Stephan Zednik, eds. </span><a href="http://www.w3.org/TR/2012/WD-prov-xml-20121211/"><cite><span class="insert">PROV-XML: The PROV XML Schema</span></cite></a><span class="insert">. 11 December 2012, Working Draft. URL: </span><a href="http://www.w3.org/TR/2012/WD-prov-xml-20121211/"><span class="insert">http://www.w3.org/TR/2012/WD-prov-xml-20121211/</span></a><span class="insert">.</span>
 </dd></dl></div></div></body></html>
 
--- a/model/prov-constraints.html	Tue Nov 20 10:06:12 2012 -0500
+++ b/model/prov-constraints.html	Tue Nov 20 15:10:55 2012 +0000
@@ -238,6 +238,7 @@
 
       });
 </script>
+    <script src="provbib.js" class="remove"></script>
 
     <script class="remove"> 
 
@@ -274,43 +275,8 @@
           "<a href=\"http://www.ditext.com/johnson/intro-3.html\"><cite>Logic: Part III</cite></a>."+
           "1924. "+
           "URL: <a href=\"http://www.ditext.com/johnson/intro-3.html\">http://www.ditext.com/johnson/intro-3.html</a>",
-        "PROV-SEM":
-          "James Cheney "+
-          "<a href=\"http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman\"><cite>Formal Semantics Strawman</cite></a>. "+
-          "2011, Work in progress. "+
-          "URL: <a href=\"http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman\">http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman</a>",
-
-        "PROV-PRIMER":
-          "Yolanda Gil and Simon Miles (eds.) Khalid Belhajjame, Helena Deus, Daniel Garijo, Graham Klyne, Paolo Missier, Stian Soiland-Reyes, and Stephan Zednik "+
-          "<a href=\"http://www.w3.org/TR/prov-primer/\"><cite>Prov Model Primer</cite></a>. "+
-          "2011, Working Draft. "+
-          "URL: <a href=\"http://www.w3.org/TR/prov-primer/\">http://www.w3.org/TR/prov-primer/</a>",
-
-
-        "PROV-DM":
-          "Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, James Cheney, Stephen Cresswell, Yolanda Gil, Paul Groth, Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes "+
-          "<a href=\"http://www.w3.org/TR/prov-dm/\"><cite>PROV-DM: The PROV Data Model</cite></a>. "+
-          "2012, Working Draft. "+
-          "URL: <a href=\"http://www.w3.org/TR/prov-dm/\">http://www.w3.org/TR/prov-dm/</a>",
-
-        "PROV-N":
-          "Luc Moreau and Paolo Missier (eds.), James Cheney, Stian Soiland-Reyes "+
-          "<a href=\"http://www.w3.org/TR/prov-n/\"><cite>PROV-N: The Provenance Notation</cite></a>. "+
-          "2011, Working Draft. "+
-          "URL: <a href=\"http://www.w3.org/TR/prov-n/\">http://www.w3.org/TR/prov-n/</a>",
-
-        "PROV-O":
-          "Timothy Lebo, Satya Sahoo and Deborah McGuinness (eds.) Khalid Belhajjame, James Cheney, David Corsar, Daniel Garijo, Stian Soiland-Reyes, and Stephan Zednik "+
-          "<a href=\"http://www.w3.org/TR/prov-o/\"><cite>Provenance Formal Model</cite></a>. "+
-          "2011, Working Draft. "+
-          "URL: <a href=\"http://www.w3.org/TR/prov-o/\">http://www.w3.org/TR/prov-o/</a>",
-      
-        "PROV-AQ":
-          "Graham Klyne and Paul Groth (eds.) Luc Moreau, Olaf Hartig, Yogesh Simmhan, James Meyers, Timothy Lebo, Khalid Belhajjame, and Simon Miles "+
-          "<a href=\"http://www.w3.org/TR/prov-aq/\"><cite>Provenance Access and Query</cite></a>. "+
-          "2011, Working Draft. "+
-          "URL: <a href=\"http://www.w3.org/TR/prov-aq/\">http://www.w3.org/TR/prov-aq/</a>",
-"RDF":
+
+         "RDF":
           "Graham Klyne and Jeremy J. Carroll (eds.) "+
           "<a href=\"http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/\"><cite>Resource Description Framework (RDF): Concepts and Abstract Syntax</cite></a>. "+
           "2004, W3C Recommendation. "+
@@ -318,7 +284,7 @@
 };
       var respecConfig = {
           // specification status (e.g. WD, LCWD, NOTE, etc.). If in doubt use ED.
-          specStatus:           "ED",
+          specStatus:           "CR",
           
           // the specification's short name, as in http://www.w3.org/TR/short-name/
           shortName:            "prov-constraints",
@@ -332,22 +298,24 @@
           // if you wish the publication date to be other than today, set this
         //  FPWD        publishDate:  "2012-05-03",
          // LC       publishDate:  "2012-09-11",
- 
+           // CR
+          publishDate:  "2012-12-11",
+
           // if the specification's copyright date is a range of years, specify
           // the start date here:
           copyrightStart: "2012",
  
           // if there is a previously published draft, uncomment this and set its YYYY-MM-DD date
           // and its maturity status
-          previousPublishDate:  "2012-05-03",
-          previousMaturity:  "WD",
+          previousPublishDate:  "2012-09-11",
+          previousMaturity:  "LC",
  
           // if there a publicly available Editor's Draft, this is the link
           edDraftURI:           "http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html",
  
           // if this is a LCWD, uncomment and set the end of its review period
-          // lcEnd: "2009-08-05",
-          lcEnd: "2012-10-10", 
+         //lcEnd: "2012-10-10", 
+          crEnd: "2012-01-31",
 
           // if you want to have extra CSS, append them to this list
           // it is recommended that the respec.css stylesheet be kept
@@ -392,7 +360,7 @@
           wgPatentURI:  "http://www.w3.org/2004/01/pp-impl/46974/status",
 
           // Add extraReferences to bibliography database
-          preProcess: [addExtraReferences],
+          preProcess: [addExtraReferences, addProvReferences],
 
           postProcess: [updateFigures, removeDataAttributes],
       };
@@ -443,46 +411,30 @@
 </section>
 
 <section id="sotd">
-<h4>Last Call</h4>
-<p>This is the second public release of the PROV-CONSTRAINTS document. 
-This is a Last Call Working Draft. The design is not expected to change significantly, going forward, and now is the key time for external review.</p>
-
-<!--
-<p>This specification identifies  <a
-href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">features at
-risk</a> related to the at-risk Mention feature of [[!PROV-DM]]:
-<a class="rule-text" href="#mention-specialization-inference"><span>TBD</span></a> and
-<a class="rule-text" href="#unique-mention"><span>TBD</span></a>.
-These might be removed from PROV-CONSTRAINTS.</p>
--->
-
-<h4>PROV Family of Specifications</h4>
-This document is part of the PROV family of specifications, a set of specifications defining various aspects that are necessary to achieve the vision of inter-operable
-interchange of provenance information in heterogeneous environments such as the Web.  The specifications are:
+<h4>PROV Family of Documents</h4>
+This document is part of the PROV family of documents, a set of documents defining various aspects that are necessary to achieve the vision of inter-operable
+interchange of provenance information in heterogeneous environments such as the Web.  These documents are:
 <ul>
-<li> <a href="http://www.w3.org/TR/prov-dm/">PROV-DM</a>, the PROV data model for provenance;</li>
-<li> <a href="http://www.w3.org/TR/prov-constraints/">PROV-CONSTRAINTS</a>, a set of constraints applying to the PROV data model  (this document);</li>
-<li> <a href="http://www.w3.org/TR/prov-n/">PROV-N</a>, a notation for provenance aimed at human consumption;</li>
-<li> <a href="http://www.w3.org/TR/prov-o/">PROV-O</a>, the PROV ontology, an OWL2 ontology allowing the mapping of PROV to RDF;</li>
-<li> <a href="http://www.w3.org/TR/prov-aq/">PROV-AQ</a>, the mechanisms for accessing and querying provenance; </li>
-<li> <a href="http://www.w3.org/TR/prov-primer/">PROV-PRIMER</a>, a primer for the PROV data model.</li>
+<li> <a href="http://www.w3.org/TR/2012/WD-prov-overview-20121211/">PROV-OVERVIEW</a> (Note), an overview of the PROV family of documents [[PROV-OVERVIEW]];</li>
+<li> <a href="http://www.w3.org/TR/2012/WD-prov-primer-20121211/">PROV-PRIMER</a> (Note), a primer for the PROV data model [[PROV-PRIMER]];</li>
+<li> <a href="http://www.w3.org/TR/2012/CR-prov-o-20121211/">PROV-O</a> (Recommendation), the PROV ontology, an OWL2 ontology allowing the mapping of PROV to RDF [[!PROV-O]];</li>
+<li> <a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/">PROV-DM</a> (Recommendation), the PROV data model for provenance [[!PROV-DM]];</li>
+<li> <a href="http://www.w3.org/TR/2012/CR-prov-n-20121211/">PROV-N</a> (Recommendation), a notation for provenance aimed at human consumption [[!PROV-N]];</li>
+<li> <a
+href="http://www.w3.org/TR/2012/CR-prov-constraints-20121211/">PROV-CONSTRAINTS</a>
+(Recommendation), a set of constraints applying to the PROV data model
+(this document);</li>
+<li> <a href="http://www.w3.org/TR/2012/WD-prov-aq-20120619/">PROV-AQ</a> (Note), the mechanisms for accessing and querying provenance [[PROV-AQ]]; </li>
+<li> <a href="http://www.w3.org/TR/2012/WD-prov-xml-20121211/">PROV-XML</a> (Note),  an XML schema for the PROV data model [[PROV-XML]].</li>
+
 </ul>
-<h4>How to read the PROV Family of Specifications</h4>
+<h4>How to read the PROV Family of Documentation</h4>
 <ul>
 <li>The primer is the entry point to PROV offering an introduction to the provenance model.</li>
-<li>The Linked Data and Semantic Web community should focus on PROV-O
-defining PROV classes and properties specified in an OWL2
-ontology. For further details, PROV-DM and PROV-CONSTRAINTS specify
-the constraints applicable to the data model, and its interpretation.  
-</li>
+<li>The Linked Data and Semantic Web community should focus on PROV-O defining PROV classes and properties specified in an OWL2 ontology. For further details, PROV-DM and PROV-CONSTRAINTS specify the constraints applicable to the data model, and its interpretation. </li>
 <li>Developers seeking to retrieve or publish provenance should focus on PROV-AQ.</li>
 <li>Readers seeking to implement other PROV serializations
-should focus on PROV-DM and PROV-CONSTRAINTS.  PROV-O and PROV-N offer
-examples of mapping to RDF and text, respectively.</li>
-<li>[[PROV-SEM]] provides a mathematical semantics and a collection of
-axioms that provide a (non-normative, but equivalent) declarative specification, aimed
-at readers with a mathematical logic or formal background.  This can
-serve as a starting point for alternative implementations. </li>
+should focus on PROV-DM and PROV-CONSTRAINTS.  PROV-O and PROV-N offer examples of mapping to RDF and text, respectively.</li>
 </ul>
 
 </section>
@@ -528,23 +480,20 @@
 
 <p>The PROV Data Model, PROV-DM, is a conceptual data model for provenance, which is
 realizable using different representations such as PROV-N and PROV-O.
-A PROV <dfn>document</dfn> is a set of PROV statements,
-together with zero or more <a>bundles</a>, or named sets of
-statements.  For
+A PROV <a>instance</a> is a set of PROV statements.
+A PROV <a>document</a> is an instance 
+together with zero or more <a>bundles</a>, or named instances.  For
 example, a PROV document could be a .provn document, the result
 of a query, a triple store containing PROV statements in RDF, etc.
-A PROV <dfn>instance</dfn> is a set of PROV statements.
 The
 PROV-DM specification [[PROV-DM]] imposes minimal requirements upon
 PROV instances. A <a>valid</a> PROV instance corresponds to a
 consistent history of objects and interactions to which logical
 reasoning can be safely applied. PROV instances need not
 be <a>valid</a>.
-</p>
-<p>
 The term <a>valid</a> is chosen by analogy with
-notions of validity in other W3C specifications. Unfortunately, this
-terminology is incompatible with the usual meaning of "validity" in logic;
+notions of validity in other W3C specifications. This
+terminology differs from the usual meaning of "validity" in logic;
 our notion of validity of a PROV instance/document is closer to
 logical "consistency".
 </p>
@@ -588,7 +537,7 @@
 applications compliant with PROV.  
 Applications producing provenance SHOULD ensure that it is
 <a>valid</a>, and similarly applications consuming provenance MAY reject provenance that is not <a>valid</a>.  Applications
-which are determining whether PROV instances or documents convey the same
+that are determining whether PROV instances or documents convey the same
 information SHOULD check equivalence as specified here.  As a
 guideline, applications should 
 treat equivalent instances or documents in the same way.  This is a
@@ -610,13 +559,17 @@
  href="#compliance">Section 3</a> summarizes the
 requirements for compliance with this document, which are specified in
 detail in the rest of the document.  </p>
-
-<p> <a href="#inferences">Section 4</a> presents definitions and inferences.  Definitions allow replacing shorthand notation in [[!PROV-N]]
+<p>
+<a
+ href="#concepts">Section 4</a> defines basic concepts used in the
+rest of the specification.  </p>
+
+<p> <a href="#inferences">Section 5</a> presents definitions and inferences.  Definitions allow replacing shorthand notation in [[!PROV-N]]
 with more explicit and complete statements; inferences allow adding
 new facts representing implicit knowledge about the structure of
 provenance.  </p>
 
-<p><a href="#constraints">Section 5</a> presents four kinds of constraints,
+<p><a href="#constraints">Section 6</a> presents four kinds of constraints,
 <em>uniqueness</em> constraints that prescribe that certain statements
 must be unique within PROV <a>instances</a>,
 <em>event ordering</em> constraints that require that the records in a
@@ -627,7 +580,7 @@
 classify the types of identifiers in valid PROV instances.
 </p>
 
-<p><a href="#normalization-validity-equivalence">Section 6</a> defines the notions
+<p><a href="#normalization-validity-equivalence">Section 7</a> defines the notions
 of <a>validity</a>, <a>equivalence</a> and <a>normalization</a>.
 </p>
 
@@ -689,7 +642,7 @@
 thing are called <em>alternates</em>, and the PROV relations of
 <span class="name">specializationOf</span> and <span class="name">alternateOf</span> can be used to link such entities.</p>
 
-<p>Besides entities, a variety of other PROV objects have
+<p>Besides entities, a variety of other PROV objects and relationships carry
 attributes, including activity, generation, usage, invalidation, start, end,
 communication, attribution, association, delegation, and
 derivation. Each object has an associated duration interval (which may
@@ -981,15 +934,15 @@
     	<td class="name">e1</td> 
 	<td class="name">'entity'</td>
      </tr>
--->
-     <tr style="text-align: center; ">
+    <tr style="text-align: center; ">
        <td class="name">e2</td> 
        <td class="name">'entity'</td>
      </tr>
-     <tr style="text-align: center; ">
+    <tr style="text-align: center; ">
        <td class="name">b</td> 
        <td class="name">'entity'</td>
      </tr>
+-->
            <tr style="text-align: center; ">
 	<td rowspan="2" class="name">hadMember(c,e)</td>
     	<td class="name">c</td> 
@@ -1030,8 +983,8 @@
 equivalence procedurally, that is, in terms of a reference
 implementation based on normalization.  Although both declarative and
 procedural specification techniques have advantages, a purely
-declarative specification offers much less assistance for
-implementers, while a procedural approach immediately demonstrates
+declarative specification offers much less guidance for
+implementers, while the procedural approach adopted here immediately demonstrates
 implementability and provides an adequate (polynomial-time) default implementation.  In
 this section we relate the declarative meaning of formulas to their
 procedural meaning.  [[PROV-SEM]] will provide an alternative,
@@ -1082,8 +1035,11 @@
   need to consider substitutions of finite sets of variables, we can
   write substitutions as <span class="math">[x<sub>1</sub> = t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span>.  A substitution
   <span class="math">S = [x<sub>1</sub> = t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span> 
-  can be <em>applied</em> to a term as follows.
+  can be <em>applied</em> to a term by replacing occurrences of
+<span class="math">x_i</span> with <span class="math">t_i</span>.
 </p>
+<!--
+as follows.
 <ol><li>
   If the term is a variable <span class="math">x<sub>i</sub></span>, one of the variables in the
   domain of <span class="math">S</span>, then <span class="math">S(x<sub>i</sub>) = t<sub>i</sub></span>.
@@ -1092,7 +1048,8 @@
   class="math">c</span>, then <span class="math">S(c) = c</span>.
   </li>
   </ol>
-<p>
+-->
+  <p>
   In addition, a substitution can be applied to an atomic formula
   (PROV statement) <span class="math">p(t<sub>1</sub>,...,t<sub>n</sub>)</span> by applying it to each term,
   that is, <span class="math">S(p(t<sub>1</sub>,...,t<sub>n</sub>)) = p(S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.  Likewise, a
@@ -1140,15 +1097,15 @@
   can be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>. A ⇔ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the
   free variables of the definition.  
 </li>
-<li>An inference of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub></span> and ... and <span class="name">A<sub>l</sub></span>  <span class="conditional">THEN</span>  there
+<li>An inference of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub></span> and ... and <span class="name">A<sub>p</sub></span>  <span class="conditional">THEN</span>  there
   exists <span class="name">y<sub>1</sub></span>...<span class="name">y<sub>m</sub></span> such that <span class="name">B<sub>1</sub></span> and ... and <span class="name">B<sub>k</sub></span> can
-  be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>.  A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the
+  be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>.  A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the
   free variables of the inference.  
 </li>
-<li>A uniqueness, ordering, or typing constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> <span class="conditional">THEN</span> <span class="name">C</span> can be viewed as a formula
-  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ C</span>.  </li>
-<li>A constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> <span class="conditional">THEN INVALID</span> can be viewed as a formula
-  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ False</span>.  </li>
+<li>A uniqueness, ordering, or typing constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> <span class="conditional">THEN</span> <span class="name">C</span> can be viewed as a formula
+  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ C</span>.  </li>
+<li>A constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> <span class="conditional">THEN INVALID</span> can be viewed as a formula
+  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ False</span>.  </li>
   </ul>
 
 
@@ -1173,23 +1130,23 @@
   <li>A logical implication as used in an inference is
    satisfied with the formula  <span class="math">∀
   x<sub>1</sub>,....,x<sub>n</sub>.  A<sub>1</sub> ∧ ... ∧
-  A<sub>l</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧
+  A<sub>p</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧
   ... ∧ B<sub>k</sub></span> holds, that is, for any substitution of
   the variables <span class="math">x<sub>1</sub>,....,x<sub>n</sub></span>, if  <span class="math">A<sub>1</sub> ∧ ... ∧
-  A<sub>l</sub></span> is true, then 
+  A<sub>p</sub></span> is true, then 
  for some further substitution of terms for variables <span class="math">
   y<sub>1</sub>...y<sub>m</sub></span>, formula <span class="math">B<sub>1</sub> ∧ ... ∧
   B<sub>k</sub></span> is also true.</li>
   <li>A uniqueness, ordering, or typing constraint is satisfied when
-  its associated formula <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ C</span> holds, that is, for any substitution of
+  its associated formula <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ C</span> holds, that is, for any substitution of
   the variables <span class="math">x<sub>1</sub>,....,x<sub>n</sub></span>, if  <span class="math">A<sub>1</sub> ∧ ... ∧
-  A<sub>l</sub></span> is true, then <span class="math">C</span> is
+  A<sub>p</sub></span> is true, then <span class="math">C</span> is
   also true.</li>
   <li>An impossibility constraint is satisfied when the formula
-  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒
+  <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒
   False</span> holds.  This is logically equivalent to <span class="math">∄
-  x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span>, that is, there exists no
-  substitution for <span class="math">x<sub>1</sub>...x<sub>n</sub></span> making <span class="math">A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> true.
+  x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span>, that is, there exists no
+  substitution for <span class="math">x<sub>1</sub>...x<sub>n</sub></span> making <span class="math">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> true.
 </ol>  
 
 <h4>Unification and Merging</h4>
@@ -1200,7 +1157,8 @@
   substitution; otherwise, the result is failure.  Unification is an
   essential concept in logic programming and automated reasoning,
 where terms can involve variables, constants and function symbols.  In PROV,
-  by comparison, unification only needs to deal with
+  by comparison, unification only needs to deal with variables,
+  constants and literals.
 </p>
 <p>
 Unifying two terms <span class="math">t,t'</span> results in either substitution <span class="math">S</span>
@@ -1306,7 +1264,7 @@
   tuple-generating and equality-generating dependencies, in the
   terminology of [[DBCONSTRAINTS]].  The termination of the remaining
   ordering, typing, and impossibility constraints is easy to show.  <a href="#termination">Appendix
-  C</a> gives a proof that the definitions, inferences, and uniqueness
+  A</a> gives a proof that the definitions, inferences, and uniqueness
   and key constraints are weakly acyclic and therefore terminating.
   </p>
   <p>
@@ -1515,7 +1473,9 @@
 type or relation involved.
 </p>
 
+<!--
 <div class="note">Table: work in progress; these entries might change when the document is updated.</div>
+-->
 
 <div id="prov-constraints-fig" style="text-align: left;">
 <table  class="thinborder" style="margin-left: auto; margin-right: auto; border-color: black;">
@@ -1792,11 +1752,11 @@
 
 <p>
   For the purpose of compliance, the normative sections of this document
-  are <a href="#compliance"
-class="sectionRef"></a>, <a href="#inferences"
-class="sectionRef"></a>, <a href="#constraints"
-class="sectionRef"></a>, and <a href="#normalization-validity-equivalence"
-class="sectionRef"></a>.  
+  are <a href="#compliance" class="sectionRef"></a>,
+<a href="#concepts" class="sectionRef"></a>,
+<a href="#inferences" class="sectionRef"></a>,
+<a href="#constraints" class="sectionRef"></a>, and
+<a href="#normalization-validity-equivalence" class="sectionRef"></a>.  
 
 
  To be compliant:
@@ -1848,6 +1808,17 @@
   <a href="#rationale">Section 2</a>.  
   </p>
 
+  <p>Many PROV relation statements have an identifier, identifying a
+  link between two or more related objects.  Identifiers can sometimes
+  be omitted in [[PROV-N]] notation.  For the purpose of inference and
+  validity checking, we generate special identifiers called
+  <dfn>variables</dfn> denoting the unknown values.
+  Generally, identifiers occurring in constraints and inferences are
+  variables.  Variables that are generated during inferences and
+  appear inside an instance are often called <dfn>existential
+  variables</dfn>, because they are implicitly existentially quantified.
+</p>
+  
   <p> A <dfn id="term">PROV term</dfn> is a constant identifier
   <span class="math">c</span>, a placeholder <span
   class="name">-</span>, a literal value, 
@@ -1858,7 +1829,7 @@
   the form <span class="math">p(t<sub>1</sub>,...,t<sub>n</sub>)</span> or <span class="math">p(id;t<sub>1</sub>,...,t<sub>n</sub>)</span> where
   <span class="math">id,t<sub>1</sub>,...,t<sub>n</sub></span> are
   PROV <a>term</a>s and <span class="math">p</span> is one of the
-  basic PROV relations. An arbitrary PROV statement is written  <span class="math">P</span>.</p>
+  basic PROV relations. An arbitrary PROV statement is written  <span class="math">A</span>.</p>
   
 <p>  A <dfn id="instance">PROV instance</dfn> is a set of PROV
   statements.  Two instances are considered to be the same if they
@@ -1873,33 +1844,33 @@
   or instance by replacing all occurrences of each of the variables
   <span class="math">x<sub>i</sub></span> with the corresponding <span class="math">t<sub>i</sub></span>.  Specifically, if <span class="math">S =
   [x<sub>1</sub>=t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span>
-  then the application of <span class="math">S</span> to a term, statement or instance, written <span class="math">S(t)</span>, <span class="math">S(P)</span> and
+  then the application of <span class="math">S</span> to a term, statement or instance, written <span class="math">S(t)</span>, <span class="math">S(A)</span> and
   <span class="math">S(I)</span> respectively, is defined as follows:</p>
-<ul><li><span class="math">S(c) = c</span> if <span class="math">c</span> is a constant identifie.r</li>
+<ul><li><span class="math">S(c) = c</span> if <span class="math">c</span> is a constant identifier.</li>
 <li><span class="math">S(x<sub>i</sub>) = t<sub>i</sub></span> if <span class="math">x<sub>i</sub></span> is one of the variables bound to a
   term <span class="math">t<sub>i</sub></span> in <span class="math">S</span>.</li>
 <li><span class="math">S(x) = x</span> if <span class="math">x</span> is a variable not bound in <span class="math">S</span>.</li>
-<li><span class="math">S(p(t<sub>1</sub>,...,t<sub>n</sub>) = p(S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.</li>
-<li><span class="math">S(p(id;t<sub>1</sub>,...,t<sub>n</sub>) = p(S(id);S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.</li>
-<li><span class="math">S(I) = { S(P) | P &isin; I } </span> if <span class="math">I</span> is an instance.</li>
+<li><span class="math">S(p(t<sub>1</sub>,...,t<sub>n</sub>)) = p(S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.</li>
+<li><span class="math">S(p(id;t<sub>1</sub>,...,t<sub>n</sub>)) = p(S(id);S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.</li>
+<li><span class="math">S(I) = { S(A) | A &isin; I } </span> if <span class="math">I</span> is an instance.</li>
 </ul>
 
-  <p>Suppose <span class="math">P</span> is a statement and <span class="math">I</span> is an
-  instance and <span class="math">S</span> a substitution.  We say that <span class="math">P</span> is
+  <p>Suppose <span class="math">A</span> is a statement and <span class="math">I</span> is an
+  instance and <span class="math">S</span> a substitution.  We say that <span class="math">A</span> is
   <dfn>satisfied</dfn> in <span class="math">I</span> by <span
-  class="math">S</span> if <span class="math">S(P) &isin; I</span>.  Likewise,
-  we say that a set of statements <span class="math">{P<sub>1</sub>,...,P<sub>n</sub>}</span> is satisfied in
+  class="math">S</span> if <span class="math">S(A) &isin; I</span>.  Likewise,
+  we say that a set of statements <span class="math">{A<sub>1</sub>,...,A<sub>n</sub>}</span> is satisfied in
   <span class="math">I</span> if each <span
-  class="math">P<sub>i</sub></span> is satisfied in <span
+  class="math">A<sub>i</sub></span> is satisfied in <span
   class="math">I</span> by <span class="math">S</span>. Finally, we
   say that a set of statements is <dfn>satisfiable</dfn>
-  in <span class="math">I</span> if there is soms substitution <span class="math">S</span> that satisfies the
+  in <span class="math">I</span> if there is some substitution <span class="math">S</span> that satisfies the
   statements in <span class="math">I</span>.
 </p>
  
     <p> <dfn>Unification</dfn> is an operation that can be applied
    to a pair of terms.
-   The result of unification is either a <dfn>unifier</dfn>, that is,name a substitution <span class="math">S</span> such that <span class="math">S(t)
+   The result of unification is either a <dfn>unifier</dfn>, that is, a substitution <span class="math">S</span> such that <span class="math">S(t)
    = S(t')</span>, or failure, indicating
    that there is no <a>unifier</a>. Unification of pairs of terms is defined as follows.</p>
 
@@ -1930,24 +1901,28 @@
 
 <div class="remark">Unification is analogous to unification in
   logic programming and theorem proving, restricted to flat terms with
-constants and variables but   no function symbols.  No occurs check is needed because there are no
+constants and variables but   no function symbols.  No "occurs check" is needed because there are no
   function symbols.</div>
 
+    <p>Two PROV instances <span class="math">I</span> and <span class="math">I'</span> are <dfn>isomorphic</dfn> if
+  there exists an invertible substitution <span class="math">S</span> that maps each
+  variable of <span class="math">I</span> to a distinct variable of <span class="math">I'</span> and such that
+  <span class="math">S(I) = I'</span>.</p>
+
 
 </section>
 <section id="inferences">
 <h2>Definitions and Inferences</h2>
 <p>
 This section  describes <a title="definition">definitions</a> and <a title="inference">inferences</a> that MAY be used on
-  provenance data, and preserve <a>equivalence</a> on <a>valid</a>
+  provenance data, and that preserve <a>equivalence</a> on <a>valid</a>
 PROV instances (as detailed in <a href="#normalization-validity-equivalence" class="sectionRef"></a>).
 A <dfn
   id="definition">definition</dfn> is a rule that can be applied to
-  PROV instances to replace defined expressions with definitions. An  <dfn id="inference">inference</dfn> is a rule that can be applied
+  PROV instances to replace defined statements with other statements. An  <dfn id="inference">inference</dfn> is a rule that can be applied
   to PROV instances to add new PROV statements.  A definition states that a
   provenance statement is equivalent to some other statements, whereas
-  an inference only states one direction of an implication; thus,
-  defined provenance statements can be replaced by their definitions.
+  an inference only states one direction of an implication.
 </p>
 
 
@@ -1978,7 +1953,7 @@
 
   <div class="remark">
     We use definitions primarily to expand the compact, concrete
-    PROV-N syntax, including short forms and optional parameters to the abstract syntax
+    PROV-N syntax, including short forms and optional parameters, to the abstract syntax
     implicitly used in PROV-DM.
   </div>
 
@@ -2004,7 +1979,7 @@
   class="name">a<sub>m</sub></span> for the existential variables.  These fresh
   identifiers might later be found to be equal to known identifiers;
   they play a similar role in PROV constraints to existential
-  variables in logic, to "labeled nulls" in database theory
+  variables in logic [[Logic]] or database theory
   [[DBCONSTRAINTS]].
   <!--,  or to blank nodes in [[!RDF]].-->
   In general, omitted optional parameters to
@@ -2031,33 +2006,19 @@
    href="#uniqueness-constraints">Uniqueness Constraints</a>.
   </p>
   
-<p>In a [definition|inference], term symbols such as <span class="name">id</span>, 
+<p>In a definition or inference, term symbols such as <span class="name">id</span>, 
 	<span class="name">start</span>, <span class="name">end</span>, <span class="name">e</span>, 
 	<span class="name">a</span>, <span class="name">attrs</span>,
 	are assumed to be variables unless otherwise specified.  These variables are scoped at 
-	the [definition|inference|constraint] level, so the rule is equivalent to any one-for-one 
-	renaming of the variable names.  When several rules are collected within a [definition|inference] 
+	the definition, inference, or constraint level, so the rule is equivalent to any one-for-one 
+	renaming of the variable names.  When several rules are
+	collected within a definition or inference 
 	as an ordered list, the scope of the variables in each rule is at the level of list elements, and so reuse of 
 	variable names in different rules does not affect the meaning.
 </p>
 <section>
   <h4>Optional Identifiers and Attributes</h4>
 
-  <p>Many PROV relation statements have an identifier, identifying a
-  link between two or more related objects.  Identifiers can sometimes
-  be omitted in [[PROV-O]] notation.  For the purpose of inference and
-  validity checking, we generate special identifiers called
-  <dfn>existential variables</dfn> denoting the unknown values.
-</p>
-<p>
-Existential variables can be <a title="substitution">substituted</a>
-  with other terms.  Specifically, a
-  <dfn>substitution</dfn> is a function from a set of existential
-  variables to identifiers, literals, the placeholder <span class="name">-</span>,
-  or other <a>existential variables</a>.  A substitution <span class="math">S</span> can be
-  applied to an instance <span class="math">I</span> by replacing all occurrences of existential
-  variables <span class="math">x</span> in the instance with <span class="math">S(x)</span>.  
-</p>
 
 
 <p>
@@ -2325,7 +2286,7 @@
    IF</span> there exists <span class="name">t1</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t2</span> MAY be a placeholder.
   </li>
 <li>  <span class="name">activity(id,t1,-,attrs)</span> <span  class="conditional">IF AND ONLY
-   IF</span> there exists <span class="name">t2</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t1</span> MUST NOT be a placeholder.
+   IF</span> there exists <span class="name">t2</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t1</span> MAY be a placeholder.
 </li>
 <!--
 <li>For each <span class="name">r</span> in {<span
@@ -2359,11 +2320,11 @@
     such that <span class="name">r(a<sub>0</sub>;...,a<sub>i-1</sub>,a',a<sub>i+1</sub>,...,a<sub>n</sub>)</span>.
     </li>
   <li>If <span class="name">a</span> is not the placeholder <span class="name">-</span>, and <span class="name">u</span> is any term, then the following definition holds:
-   <p> <span class="name">wasDerivedFrom(id;e2,e1,a,-,u,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">g</span>
+   <p> <span class="name">wasDerivedFrom(id; e2,e1,a,-,u,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">g</span>
     such that <span class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</span>.</li>
   <li>If <span class="name">a</span> is not the placeholder <span class="name">-</span>, and <span class="name">g</span> is any term,
     then the following definition holds:
-   <p> <span class="name">wasDerivedFrom(id;e2,e1,a,g,-,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">u</span>
+   <p> <span class="name">wasDerivedFrom(id; e2,e1,a,g,-,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">u</span>
     such that <span class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</span>.</li></ol>
     </div>
 
@@ -2868,7 +2829,8 @@
   
 <hr>
   <p id="alternate-reflexive_text">The relation <span
-  class='name'>alternateOf</span> is an <a>equivalence relation</a>: that is,
+  class='name'>alternateOf</span> is an <a>equivalence relation</a> on
+  entities: that is,
   it is <a>reflexive</a>,
   <a>transitive</a> and <a>symmetric</a>.  As a consequence, the
   following inferences can be applied:</p>
@@ -3001,7 +2963,7 @@
     patterns of statements in <a>valid</a> PROV instances.
     </ul>
   
-  <p>As in a [definition|inference], term symbols such as <span class="name">id</span>, 
+  <p>As in a definition or inference, term symbols such as <span class="name">id</span>, 
 	<span class="name">start</span>, <span class="name">end</span>, <span class="name">e</span>, 
 	<span class="name">a</span>, <span class="name">attrs</span> in a constraint,
 	are assumed to be variables unless otherwise specified.  These variables are scoped at 
@@ -3165,9 +3127,11 @@
   <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#association.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
   the <span class="name">wasAssociatedWith(id; a,ag,pl,attrs)</span> statement.
  </li>
-  <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#association.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
+<!--
+ <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#association.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
   the <span class="name">wasAssociatedWith(id; a,ag,-,attrs)</span> statement.
   </li>
+-->
   <li>The identifier field <a href="http://www.w3.org/TR/prov-dm/#delegation.id"><span class="name">id</span></a> is a <span class="conditional">KEY</span> for
   the <span class="name">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span> statement.
   </li>
@@ -3308,12 +3272,12 @@
 <hr />
 
 
+<!--
 <div class="note">
 <p>Note: The following constraint is associated with a feature "<a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">at risk</a>" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</p>
 </div>
   
 
-<!--
 <div id='unique-mention_text'>
 <p>An entity can be the subject of at most one mention relation.</p>
 </div>
@@ -3357,7 +3321,7 @@
 <p>Specifically, <dfn id="dfn-precedes">precedes</dfn> is a <a>preorder</a>
 between <a title="instantaneous event">instantaneous events</a>.  A
 constraint of the form
-<span class="name">e1</span> precedes <span
+<span class="name">e1</span> <a>precedes</a> <span
 class="name">e2</span> means that <span class="name">e1</span>
 happened at the same time as or before <span class="name">e2</span>.
 For symmetry, <dfn id="dfn-follows">follows</dfn> is defined as the
@@ -3447,13 +3411,17 @@
 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 class="note"> Miscellaneous suggestions about figures
-  (originally from Tim Lebo):
+
+<!--
+<div class="note"> Miscellaneous suggestions about figures
+  (originally from Tim Lebo):  NOW ADDRESSED
 <ul>
   <li>
     I think it would help if the "corresponding edges between entities and activities" where the same visual style as the vertical line marking the time the Usage, generation and derivation occurred. A matching visual style provides a Gestalt that matches the concept. I am looking at subfigures b and c in 5.2. </ul>
   </div>
 
+  -->
+  
   <div style="text-align: center;">
 
 <figure id="ordering-activity">
@@ -3659,7 +3627,9 @@
 <h3> Entity constraints</h3>
 
 
+<!--
 <div class="note">The figure(s) in this section should have vertical lines with visual styles that match the diagonal arrow that they go with. </div>
+-->
 
 <p>
 As with activities, entities have lifetimes: they are generated, then
@@ -3740,8 +3710,6 @@
 <span class="name">inv</span>.</p>
 </div>
 
-<hr />
-
 
 <hr />
 
@@ -3823,7 +3791,7 @@
 <div class='constraint'
   id='derivation-generation-generation-ordering'>
   <p>
-In this constraint, any <span class="name">_a</span>, <span
+In this constraint, any of <span class="name">_a</span>, <span
   class="name">_g</span>, <span class="name">_u</span> MAY be placeholders.</p>
 <p>
  <span class="conditional">IF</span>
@@ -4128,9 +4096,13 @@
 <section id="type-constraints">
 <h2>Type Constraints</h2>
 
-<p id='typing_text'>The following rule  establishes types denoted by identifiers from their use within expressions. 
+<p id='typing_text'>The following rules assign types to identifiers
+based on their use within statements. 
 The function <span class="name">typeOf</span> gives the set of types denoted by an identifier.
-That is,  <span class="name">typeOf(e)</span> returns the set of types associated with identifier  <span class="name">e</span>. The function <span class="name">typeOf</span> is not a term of PROV, but a construct introduced to validate PROV statements. 
+That is,  <span class="name">typeOf(e)</span> returns the set of types
+associated with identifier  <span class="name">e</span>. The function
+<span class="name">typeOf</span> is not a PROV statement, but a
+construct used only during validation PROV, similar to <a>precedes</a>.
 </p>
 
 
@@ -4554,8 +4526,9 @@
   <h2>Instances</h2>
   
 <div class="remark">
-  Implementations should decide up front what reasoning about
-  co-reference should be applied, and rewrite the instance (by
+  Before normalization or validation, implementations should expand
+  namespace prefixes and  perform any appropriate reasoning about
+  co-reference of identifiers, and rewrite the instance (by
   replacing co-referent identifiers with a single common identifier) to
   make this explicit, before doing validation, equivalence checking,
   or normalization.
@@ -4567,7 +4540,7 @@
 
 <p> We define the <dfn>normal form</dfn> of a PROV instance as the set
 of provenance statements resulting from applying all definitions,
-  inferences, and uniqueness constraints.</p>
+  inferences, and uniqueness constraints, obtained as follows:</p>
 
 
 
@@ -4593,18 +4566,19 @@
     <li>If no definitions, inferences, or uniqueness constraints can be applied to instance <span class="math">I<sub>3</sub></span>, then <span class="math">I<sub>3</sub></span> is the
     normal form of <span class="math">I</span>.</li>
     <li>Otherwise, the normal form of <span class="math">I</span> is the same as the normal form
-    of <span class="math">I<sub>3</sub></span> (that is, proceed by recursively normalizing <span class="math">I<sub>3</sub></span>).
+    of <span class="math">I<sub>3</sub></span> (that is, proceed by
+    normalizing <span class="math">I<sub>3</sub></span> at step 1).
  </ol>
  
 <p>Because of the potential interaction among definitions, inferences, and
-  constraints, the above algorithm is recursive.  Nevertheless,
+  constraints, the above algorithm is iterative.  Nevertheless,
   all of our constraints fall into a class of <a>tuple-generating
   dependencies</a> and <a>equality-generating dependencies</a> that
   satisfy a termination condition called <a>weak acyclicity</a> that
   has been studied in the context of relational databases
   [[DBCONSTRAINTS]].  Therefore, the above algorithm terminates, independently
   of the order in which inferences and constraints are applied.
-  <a href="#termination">Appendix C</a> gives a proof that normalization terminates and produces
+  <a href="#termination">Appendix A</a> gives a proof that normalization terminates and produces
   a unique (up to isomorphism) normal form.
 </p>
   
@@ -4616,7 +4590,8 @@
   validity:</p>
 
 <ol>
-  <li>Normalize the instance <span class="math">I</span>, obtaining normalized instance <span class="math">I'</span>.  If
+  <li>Normalize the instance <span class="math">I</span>, obtaining
+  normal form <span class="math">I'</span>.  If
   normalization fails, then <span class="math">I</span> is not <a>valid</a>.
   </li>
   <li>Apply all event ordering constraints to <span class="math">I'</span> to build a graph <span class="math">G</span> whose nodes
@@ -4640,10 +4615,6 @@
   constraint fails due to unification or merging failure. </p>
 
 
-  <p>Two PROV instances <span class="math">I</span> and <span class="math">I'</span> are <dfn>isomorphic</dfn> if
-  there exists an invertible substitution <span class="math">S</span> that maps each
-  variable of <span class="math">I</span> to a distinct variable of <span class="math">I'</span> and such that
-  <span class="math">S(I) = I'</span>.</p>
 
 <p>  Two <a>valid</a> PROV instances are <dfn>equivalent</dfn> if they
   have <a>isomorphic</a> normal forms.  That is, after applying all possible inference
@@ -4710,11 +4681,10 @@
 
 <p>The definitions, inferences, and constraints, and
 the resulting notions of normalization, validity and equivalence,
-assume a PROV document that consists only of a <a>toplevel
-instance</a>, containing all PROV statements in the top level of the
-document (that is, not enclosed in a named <a>bundle</a>).  In this
+work on a single PROV instance.  In this
 section, we describe how to deal with general PROV
-documents, possibly including multiple named bundles.  Briefly, each bundle is
+documents, possibly including multiple named bundles as well as a
+toplevel instance.  Briefly, each bundle is
 handled independently; there is no interaction between bundles from
 the perspective of applying definitions, inferences, or constraints,
 computing normal forms, or checking validity or equivalence.</p>
@@ -4722,38 +4692,39 @@
 <p> We model a general PROV document, containing <span class="name">n</span> named bundles
 <span class="name">b<sub>1</sub>...b<sub>n</sub></span>, as a tuple
 <span
-class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,b<sub>n</sub>=B<sub>n</sub>])</span>
-where <span class="name">B<sub>0</sub></span> is the set of
-statements of the <a>toplevel instance</a>, and for each <span class="name">i</span>, <span class="name">B<sub>i</sub></span> is the set of
-statements of bundle <span class="name">b<sub>i</sub></span>.  Names <span class="name">b<sub>1</sub>...b<sub>n</sub></span> are assumed to be distinct.  This notation is shorthand for the
+class="name">(I<sub>0</sub>,[b<sub>1</sub>=I<sub>1</sub>,...,b<sub>n</sub>=I<sub>n</sub>])</span>
+where <span class="name">I<sub>0</sub></span> is the toplevel
+instance, and for each <span class="name">i</span>, <span
+class="name">I<sub>i</sub></span> is the instance associated with
+bundle <span class="name">b<sub>i</sub></span>.   This notation is shorthand for the
 following PROV-N syntax:</p>
 
 <div class="name">
 document<br />
-&nbsp;&nbsp;&nbsp;B<sub>0</sub><br />
+&nbsp;&nbsp;&nbsp;I<sub>0</sub><br />
 &nbsp;&nbsp;&nbsp;bundle b<sub>1</sub><br />
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;B<sub>1</sub><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;I<sub>1</sub><br />
 &nbsp;&nbsp;&nbsp;endBundle<br />
 &nbsp;&nbsp;&nbsp;...<br />
 &nbsp;&nbsp;&nbsp;bundle b<sub>n</sub><br />
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;B<sub>n</sub><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;I<sub>n</sub><br />
 &nbsp;&nbsp;&nbsp;endBundle<br />
 endDocument
 </div>
 
 <p> The <a>normal form</a> of a PROV document
-<span class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,[b<sub>n</sub>=B<sub>n</sub>])</span> is <span class="name">(B'<sub>0</sub>,[b<sub>1</sub>=B'<sub>1</sub>,...,b<sub>n</sub>=B'<sub>n</sub>])</span>
-where <span class="name">B'<sub>i</sub></span> is the normal
-form of <span class="name">B<sub>i</sub></span> for each <span class="name">i</span> between 0 and <span class="name">n</span>.  </p>
-
-<p>A PROV document is <a>valid</a> if each of the bundles <span class="name">B<sub>0</sub></span>,
-..., <span class="name">B<sub>n</sub></span> are valid and none of the bundle identifiers <span class="name">b<sub>i</sub></span> are repeated.</p>
-
-<p>Two (valid) PROV documents <span class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,b<sub>n</sub>=B<sub>n</sub>])</span> and
-<span class="name">(B'<sub>0</sub>,[b<sub>1</sub>'=B'<sub>1</sub>,...,b'<sub>m</sub>=B'<sub>m</sub>])</span> are <a>equivalent</a> if <span class="name">B<sub>0</sub></span> is
-equivalent to <span class="name">B'<sub>0</sub></span> and <span class="name">n = m</span> and
+<span class="name">(I<sub>0</sub>,[b<sub>1</sub>=I<sub>1</sub>,...,[b<sub>n</sub>=I<sub>n</sub>])</span> is <span class="name">(I'<sub>0</sub>,[b<sub>1</sub>=I'<sub>1</sub>,...,b<sub>n</sub>=I'<sub>n</sub>])</span>
+where <span class="name">I'<sub>i</sub></span> is the normal
+form of <span class="name">I<sub>i</sub></span> for each <span class="name">i</span> between 0 and <span class="name">n</span>.  </p>
+
+<p>A PROV document is <a>valid</a> if each of the bundles <span class="name">I<sub>0</sub></span>,
+..., <span class="name">I<sub>n</sub></span> are valid and none of the bundle identifiers <span class="name">b<sub>i</sub></span> are repeated.</p>
+
+<p>Two (valid) PROV documents <span class="name">(I<sub>0</sub>,[b<sub>1</sub>=I<sub>1</sub>,...,b<sub>n</sub>=I<sub>n</sub>])</span> and
+<span class="name">(I'<sub>0</sub>,[b<sub>1</sub>'=I'<sub>1</sub>,...,b'<sub>m</sub>=I'<sub>m</sub>])</span> are <a>equivalent</a> if <span class="name">I<sub>0</sub></span> is
+equivalent to <span class="name">I'<sub>0</sub></span> and <span class="name">n = m</span> and
 there exists a permutation <span class="name">P : {1..n} -> {1..n}</span> such that for each <span class="name">i</span>, <span class="name">b<sub>i</sub> =
-b'<sub>P(i)</sub></span> and <span class="name">B<sub>i</sub></span> is equivalent to <span class="name">B'<sub>P(i)</sub></span>.
+b'<sub>P(i)</sub></span> and <span class="name">I<sub>i</sub></span> is equivalent to <span class="name">I'<sub>P(i)</sub></span>.
 </p>
 
 </section> <!-- bundle-constraints-->
@@ -4784,15 +4755,15 @@
        <a>transitive</a>.</li>
        <li> <dfn>irreflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a>irreflexive</a> if
       for <span class="math">x R x</span> does not hold for any element <span class="math">x</span> of <span class="math">X</span>.</li>
-        <li> <dfn>reflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a>reflexive</a> if
-      for any element <span class="math">x</span> of <span class="math">X</span>, we have <span class="math">x R x</span>.</li>
-      <li><dfn>partial order</dfn>: A partial order is a relation
+     <li><dfn>partial order</dfn>: A partial order is a relation
       that is <a>reflexive</a>, <a>antisymmetric</a>, and <a>transitive</a>.</li>
       <li><dfn>preorder</dfn>: A preorder is a relation that is
       <a>reflexive</a> and <a>transitive</a>.  (It is not necessarily antisymmetric,
       meaning there can be cycles of distinct elements <span
        class="math">x<sub>1</sub> R x<sub>2</sub> R ... R
       x<sub>n</sub> R x<sub>1</sub>.</span></li>
+        <li> <dfn>reflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a>reflexive</a> if
+      for any element <span class="math">x</span> of <span class="math">X</span>, we have <span class="math">x R x</span>.</li>
     <li><dfn>strict partial order</dfn>: A strict partial order is a
       relation that is <a>irreflexive</a>, <a>asymmetric</a> and <a>transitive</a>.</li>
       <li><dfn>strict preorder</dfn>: A strict preorder is a relation
@@ -4849,15 +4820,16 @@
 	</tr>
 	<tr>
 	  <td>1</td>
-	  <td>19, 20, 21, 22</td>
-	  <td class="name">specializationOf, mentionOf</td>  <!-- TODO remove mention -->
+	  <td>19, 20, 21</td>
+	  <td class="name">specializationOf</td>  <!-- TODO remove mention -->
 	  <td class="name">specializationOf, entity</td>
 	</tr>
 	<tr>
 	  <td>2</td>
 	  <td>7, 8, 13, 14</td>
 	  <td class="name">entity, activity, wasAttributedTo, actedOnBehalfOf</td>
-	  <td class="name">wasInvalidatedBy, wasStartedBy, wasEndedBy</td>
+	  <td class="name">wasInvalidatedBy, wasStartedBy, wasEndedBy,
+	wasAssociatedWith</td>
 	</tr>	
 	<tr>
 	  <td>3</td>
@@ -5003,7 +4975,8 @@
   <li>Added "document" and "endDocument" to sec. 6.2.</li>
   <li>Added sentence of explanation of purpose to beginning.</li>
   <li>Moved "mention" to a separate note. </li>
-  
+  <li>Added <a href="#concepts">Section 4: Basic Concepts</a>.</li>
+  <li>Miscellaneous final cleanup prior to CR staging.</li>
 </ul>
 
 </section>
@@ -5126,5 +5099,21 @@
  -->
 <!--  LocalWords:  Altintas Reza B'Far Belhajjame Informatics Coppens IBBT Nies
  -->
-<!--  LocalWords:  Corsar Cresswell Deus DERI Galway
+<!--  LocalWords:  Corsar Cresswell Deus DERI Galway satisfiable namespace Kai
  -->
+<!--  LocalWords:  endDocument Dobson Doerr Hellas Eckert EVAIN EBU UER Frew de
+ -->
+<!--  LocalWords:  Irini Fundulaki Garijo Universidad Politécnica Vrije Hartig
+ -->
+<!--  LocalWords:  Universiteit Hau NCI Sandro Hawke Jörn Hees DFKI Gmbh Hua da
+ -->
+<!--  LocalWords:  Hodgson TopQuadrant Trung Huynh Klyne Revelytix Rensselaer
+ -->
+<!--  LocalWords:  McCusker McGuinness Paolo Missier Luc Moreau Vinh Edoardo
+ -->
+<!--  LocalWords:  Pignotti Paulo Pinheiro Geospatial Retter Runnegar Satya
+ -->
+<!--  LocalWords:  Sahoo Schaengold Schutzer FSTC Yogesh Simmhan Theodoridou
+ -->
+<!--  LocalWords:  Thibodeau OpenLink Tilmes Zednik Zhao Yuting
+ -->