--- a/model/prov-constraints.html	Thu Jun 07 09:07:58 2012 +0100
+++ b/model/prov-constraints.html	Thu Jun 07 09:53:00 2012 +0100
@@ -2039,6 +2039,129 @@
   Do the insertion/removal derivation steps imply wasDerivedFrom,
   wasVersionOf, alternateOf?
   </div>
+  
+
+<section id="collections-and-contents">
+
+  
+<h4>Collections and Contents</h4>
+
+<p>We model the contents of a dictionary <span class="name">d</span> with a function contents, which can have the possible values:
+<ul>
+<li>contents(d,<em>k</em>)=<em>e</em>:  there is an entry with key <em>k</em> and entity <em>e</em> in <span class="name">d</span>;
+<li>contents(d,<em>k</em>)=&#8869:  there is no entry with key <em>k</em> in <span class="name">d</span>;
+
+<li>contents(d,<em>k</em>)=?:  it is not known if there is an entry with key <em>k</em> in <span class="name">d</span>.
+</ul>
+
+<p id="contents-empty-dictionary_text">The contents of an EmptyDictionary  is defined as the empty set.</p>
+
+       <div class='inference' id="contents-empty-dictionary">
+<p>
+    For any dictionary <span class="name">d</span>, 
+<span class='conditional'>IF</span>
+<span class="name">entity(d, [prov:type='prov:EmptyDictionary'])</span>,
+ <span class='conditional'>THEN</span>:</p>
+<ul>
+<li> <span class="name">contents(d,<em>k</em>)=&#8869</span> for any <em>k</em>.
+</ul>
+</div> 
+
+
+<p id="contents-unspecified-dictionary_text">By default, the contents of a dictionary is unknown.</p>
+
+       <div class='inference' id="contents-unspecified-dictionary">
+<p>
+    For any dictionary <span class="name">d</span>, 
+<span class='conditional'>IF</span>
+<span class="name">entity(d, [prov:type='prov:Dictionary'])</span>,
+ <span class='conditional'>THEN</span>:</p>
+<ul>
+<li> <span class="name">contents(d,<em>k</em>)=?</span> for any <em>k</em>.
+</ul>
+</div> 
+
+<p id="contents-after-insertion_text">The contents of a dictionary after insertion is defined as follows.</p>
+    
+       <div class='inference' id="contents-after-insertion">
+<p>
+    For any dictionaries <span class="name">d1</span> and <span class="name">d2</span>, 
+<span class='conditional'>IF</span>
+<span class="name">derivedByInsertionFrom(d2, d1, {(<em>k1</em>, <em>e1</em>) ... (<em>kn</em>, <em>en</em>)})</span>,
+ <span class='conditional'>THEN</span>:</p>
+<ul>
+<li> <span class="name">contents(d2,<em>k</em>)=contents(d1,<em>k</em>)</span> if <em>k</em> is not in <em>k1</em>, ..., <em>kn</em>;
+<li> <span class="name">contents(d2,<em>ki</em>)=<em>ei</em></span>  if <em>k</em> is in <em>k1</em>, ..., <em>kn</em>;
+</ul>
+</div> 
+
+
+<p id="contents-after-removal_text">The contents of a dictionary after removal is defined as follows.</p>
+    
+       <div class='inference' id="contents-after-removal">
+<p>
+    For any dictionaries <span class="name">d1</span> and <span class="name">d2</span>, 
+<span class='conditional'>IF</span>
+<span class="name">derivedByRemovalFrom(d2, d1, {<em>k1</em> ... <em>kn</em>})</span>,
+ <span class='conditional'>THEN</span>:</p>
+<ul>
+<li> <span class="name">contents(d2,<em>k</em>)=contents(d1,<em>k</em>)</span> if <em>k</em> is not in <em>k1</em>, ..., <em>kn</em>;
+<li> <span class="name">contents(d2,<em>ki</em>)=&#8869</span>  if <em>k</em> is in <em>k1</em>, ..., <em>kn</em>.
+</ul>
+</div> 
+
+
+<p id="contents-after-membership_text">The contents of a dictionary after membership is defined as follows.</p>
+    
+       <div class='inference' id="contents-after-membership">
+<p>
+    For any dictionary <span class="name">d</span>, 
+<span class='conditional'>IF</span>
+<span class="name">memberOf(d, {(<em>k1</em>, <em>e1</em>) ... (<em>kn</em>, <em>en</em>)})</span>,
+ <span class='conditional'>THEN</span>:</p>
+<ul>
+<li> <span class="name">contents(d,<em>k</em>)='?'</span> if <em>k</em> is not in <em>k1</em>, ..., <em>kn</em>;
+<li> <span class="name">contents(d,<em>ki</em>)=<em>ei</em></span>  if <em>k</em> is in <em>k1</em>, ..., <em>kn</em>.
+</ul>
+</div> 
+
+
+
+<p id="contents-after-complete-membership_text">The contents of a dictionary after complete membership is defined as follows.</p>
+    
+       <div class='inference' id="contents-after-complete-membership">
+<p>
+    For any dictionary <span class="name">d</span>, 
+<span class='conditional'>IF</span>
+<span class="name">memberOf(d, {(<em>k1</em>, <em>e1</em>) ... (<em>kn</em>, <em>en</em>)}, true)</span>,
+ <span class='conditional'>THEN</span>:</p>
+<ul>
+<li> <span class="name">contents(d,<em>k</em>)='&#8869'</span> if <em>k</em> is not in <em>k1</em>, ..., <em>kn</em>;
+<li> <span class="name">contents(d,<em>ki</em>)=<em>ei</em></span>  if <em>k</em> is in <em>k1</em>, ..., <em>kn</em>.
+</ul>
+</div> 
+
+
+
+
+<p id="contents-after-complete-membership_text">Looking up a key in a dictionary results in an entity, which is an alternate of an entity known to be in the contents. </p>
+    
+       <div class='inference' id="lookup-and-membership">
+<p>
+<span class='conditional'>IF</span>
+<span class="name">wasDerivedFrom(e2,d,[prov:key=<em>k</em>, prov:type='prov:Lookup'])</span>, and
+<span class="name">contents(d,<em>k</em>)=e1</em></span>
+ <span class='conditional'>THEN</span>: <span class="name">alternateOf(e2,e1)</span>.
+
+</div> 
+
+
+
+
+
+
+</section>
+
  
 </section> <!-- collection-constraints -->