--- a/dictionary/Overview.html	Mon Apr 15 16:17:29 2013 +0200
+++ b/dictionary/Overview.html	Mon Apr 15 17:35:10 2013 +0200
@@ -867,7 +867,7 @@
 <p>
 An Insertion relation <span class="name">prov:derivedByInsertionFrom(id; d2, d1,  {(key_1, e_1), ..., (key_n, e_n)})</span> states that  <span class="name">d2</span> is the dictionary
 following the insertion of key-entity pairs <span class="name">(key_1, e_1)</span>, ..., <span class="name">(key_n, e_n)</span> into dictionary  <span class="name">d1</span>. In other words, the set of key-entity pairs <span class="name">{(key_1, e_1), ...,(key_n, e_n)}</span> is to be seen as the difference between <span class="name">d1</span> and <span class="name">d2</span>.
-Note that this key-entity-set is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary derived by an insertion relation. This is formalized in <a href="#insertion-removal-membership-inference">Inference D8</a>.</p>
+Note that this key-entity-set is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary derived by an insertion relation. This is formalized in <a href="#membership-insertion-membership-inference">Inference D4</a>.</p>
 
 <div class="anexample">
 <pre class="codeexample">
@@ -933,7 +933,7 @@
 </div>
 
 <p>A Removal relation <span class="name">prov:derivedByRemovalFrom(id; d2,d1, {key_1, ..., key_n})</span> states that  <span class="name">d2</span> is  the  dictionary following the removal of the set of pairs corresponding to keys  <span class="name">key_1...key_n</span> from  <span class="name">d1</span>. 
-  In other words, the key-set <span class="name">{key_1,...,key_n}</span> is to be seen as the difference in keys and corresponding entities between <span class="name">d1</span> and <span class="name">d2</span>. Note that this key-set is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary derived by a removal relation. This is formalized in <a href="#insertion-removal-membership-inference">Inference D8</a>. 
+  In other words, the key-set <span class="name">{key_1,...,key_n}</span> is to be seen as the difference in keys and corresponding entities between <span class="name">d1</span> and <span class="name">d2</span>. Note that this key-set is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary derived by a removal relation. This is formalized in <a href="#membership-removal-membership-inference">Inference D5</a>. 
 </p>
 
 <div class="anexample">
@@ -2702,8 +2702,7 @@
    <span class='conditional'>THEN</span> <span class="name">e1 = e2</span>
 </p></div>
 
-<p id="membership-insertion-membership-inference_text">If a dictionary was derived from another dictionary by an insertion, then the former holds all key-entity pairs of the latter, except those updated by the insertion. 
-  Similarly, all members of a dictionary that was derived from another dictionary by an insertion were also members of the latter dictionary, except those added or updated by the insertion.</p>
+<p id="membership-insertion-membership-inference_text">No key-entity pairs were added to or removed from a dictionary derived by insertion, except those added or updated by the insertion.</p>
 	 <div class='inference' id='membership-insertion-membership-inference'>
 	<span class='ruleTitle'><a class="internalDFN" href="#membership-insertion-membership-inference">Inference D4 (membership-insertion-membership)</a></span>
 <p>Here, KV1 is a set of key-entity pairs and K1 is the key-set of KV1.</p>
@@ -2716,10 +2715,33 @@
    and <span class="name">prov:derivedByInsertionFrom(d2, d1, KV1)</span> and <span class="name">k</span> &notin; <span class="name">K1</span>
    <span class='conditional'>THEN</span> <span class="name">prov:hadDictionaryMember(d1, e, k)</span></li>
   </ol></div>
-
+  
+  <p id="membership-removal-membership_text">No key-entity pairs were added to or removed from a dictionary derived by removal, except those specified by the removal.</p>
+	 <div class='inference' id='membership-removal-membership-inference'>
+	<span class='ruleTitle'><a class="internalDFN" href="#membership-removal-membership-inference">Inference D5 (membership-removal-membership)</a></span>
+  <p>Here, K1 is a set of keys.</p>
+  <ol>
+<li><span class="conditional">IF</span>  <span class="name">prov:hadDictionaryMember(d1, e, k)</span>
+   and <span class="name">prov:derivedByRemovalFrom(d2, d1, K1)</span> and <span class="name">k</span> &notin; <span class="name">K1</span>
+   <span class='conditional'>THEN</span> <span class="name">prov:hadDictionaryMember(d2, e, k)</span></li>
+   
+<li><span class="conditional">IF</span>  <span class="name">prov:hadDictionaryMember(d2, e, k)</span>
+   and <span class="name">prov:derivedByRemovalFrom(d2, d1, K1)</span>
+   <span class='conditional'>THEN</span> <span class="name">prov:hadDictionaryMember(d1, e, k)</span></li>
+  </ol>
+</div>
+
+  <div class="remark">
+  Note that inferences  <a class="internalDFN" href="#membership-insertion-membership-inference">D4</a> and  
+  <a class="internalDFN" href="#membership-removal-membership-inference">D5</a>, together with constraints 
+  <a class="internalDFN" href="#impossible-removal-insertion-constraint">D9</a>, <a class="internalDFN" href="#unique-insertion-constraint">D10</a> 
+ , <a class="internalDFN" href="#unique-insertion-constraint">D11</a> and <a class="internalDFN" href="#unique-removal-constraint">D12</a>, and the fact that an EmptyDictionary does not contain any key-entity pairs (as formalized in <a href="http://www.w3.org/TR/2013/PR-prov-constraints-20130312/#membership-empty-collection">PROV-Constraints</a>), 
+  guarantee <b>completeness</b> of a dictionary, if it can be traced back to an EmptyDictionary through insertions and removals.
+  Here, completeness means that all key-entity pairs of the dictionary are known through a hadDictionaryMember statement.
+	  </div>
 <p id="insertion-membership-inference_text">A dictionary that was derived by an insertion of key-entity pairs, holds all these specified key-entity pairs. This inference also means that Insertion provides an "update semantics" for the keys that are already present in a dictionary.</p>
 	 <div class='inference' id='insertion-membership-inference'>
-	<span class='ruleTitle'><a class="internalDFN" href="#insertion-membership-inference">Inference D5 (insertion-membership)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#insertion-membership-inference">Inference D6 (insertion-membership)</a></span>
  <p>Here, KV1 is a set of key-entity pairs.</p>
   <p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByInsertionFrom(d2, d1, KV1)</span> 
@@ -2728,14 +2750,14 @@
 
 <p id="insertion-derivation-inference_text">Insertion and removal are special cases of derivation.</p>
 	 <div class='inference' id='insertion-derivation-inference'>
-	<span class='ruleTitle'><a class="internalDFN" href="#insertion-derivation-inference">Inference D6 (insertion-derivation)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#insertion-derivation-inference">Inference D7 (insertion-derivation)</a></span>
  <p>Here, KV1 is a set of key-entity pairs.</p>
  <p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByInsertionFrom(d2, d1, KV1)</span> 
    <span class='conditional'>THEN</span> <span class="name">prov:wasDerivedFrom(d2, d1)</span>
 </p></div>
 	 <div class='inference' id='removal-derivation-inference'>
-	<span class='ruleTitle'><a class="internalDFN" href="#removal-derivation-inference">Inference D7 (removal-derivation)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#removal-derivation-inference">Inference D8 (removal-derivation)</a></span>
    <p>Here, K1 is a set of keys.</p>
 <p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByRemovalFrom(d2, d1, K1)</span> 
@@ -2743,27 +2765,6 @@
 </p></div>
 
 
-<p id="insertion-removal-membership-inference_text">Insertions and removals do not introduce any new key-entity pairs, other than those specified.</p>
-	 <div class='inference' id='insertion-removal-membership-inference'>
-	<span class='ruleTitle'><a class="internalDFN" href="#insertion-removal-membership-inference">Inference D8 (insertion-removal-membership)</a></span>
-<ol>
-	<li>
-	<span class="conditional">IF</span> <span class="name">prov:derivedByInsertionFrom(d2, d1, {("k1", e1)})</span> and 
-	<span class="name">prov:derivedByRemovalFrom(d3, d2, {"k1"})</span> and <span class="name">prov:hadDictionaryMember(d1, e2, "k2")</span> and 
-	<span class="name">k1 &ne; k2</span> <span class='conditional'>THEN</span>  <span class="name">prov:hadDictionaryMember(d3, e2, "k2")</span>
-	</li>
-	<li>
-	<span class="conditional">IF</span> <span class="name">prov:derivedByInsertionFrom(d2, d1, {("k1", e1)})</span> and 
-	<span class="name">prov:derivedByRemovalFrom(d3, d2, {"k1"})</span> and <span class="name">prov:hadDictionaryMember(d3, e2, "k2")</span> and 
-	<span class="name">k1 &ne; k2</span> <span class='conditional'>THEN</span>  <span class="name">prov:hadDictionaryMember(d1, e2, "k2")</span>
-	</li>
-</ol>
-</div>
-  <div class="remark">
-  Note that this inference, together with constraints <a class="internalDFN" href="#impossible-removal-insertion-constraint">D9</a>, <a class="internalDFN" href="#unique-insertion-constraint">D10</a> and <a class="internalDFN" href="#unique-removal-constraint">D11</a>, and the fact that an EmptyDictionary does not contain any key-entity pairs, guarantees <b>completeness</b> of a dictionary, if it can be traced back to an EmptyDictionary through insertions and removals.
-  Here, completeness means that all key-entity pairs of the dictionary are known through a hadDictionaryMember statement.
-	  </div>
-
 </section>
 	<!-- end inferences -->