--- a/model/working-copy/wd6-collections-constraints.html	Sat Jun 09 16:25:30 2012 +0100
+++ b/model/working-copy/wd6-collections-constraints.html	Sat Jun 09 18:14:31 2012 +0100
@@ -275,7 +275,7 @@
 <section id="dictionaries-and-contents-2">
 
   
-<h4>Collections and Contents take 2</h4>
+<h4>Collections and Contents</h4>
 
 The interpretation of Collection statements is defined by the following axioms. 
 
@@ -283,9 +283,9 @@
 <ol>
 <li><span class="name">entity(c, [prov:type='prov:EmptyCollection'])</span> &rArr; Contents(c) = &empty;
 
-<li> <span class="name">derivedByInsertionFrom(c2, c1, E)</span>   &rArr; Contents(c) &sup; Contents(c1) &cup; E;
+<li> <span class="name">derivedByInsertionFrom(c2, c1, E)</span>   &rArr; Contents(c) = Contents(c1) &cup; E;
 
-<li> <span class="name">derivedByRemovalFrom(c2, c1, E)</span>    &rArr; Contents(c) &sup; Contents(c1) \ E;
+<li> <span class="name">derivedByRemovalFrom(c2, c1, E)</span>    &rArr; Contents(c) = Contents(c1) \ E;
 
 <li> <span class="name">memberOf(c, E)</span> &rArr; Contents(c) &sup; E
 
@@ -293,38 +293,108 @@
   
 </ol>
 
-Note that a chain of insertions and removals that starts from statements of the form (1) or (5) leads to a precise characterisation of the contents of the resulting collection, for example:
+<h4>Some consequences of these axioms</h4>
 
-<span class="name">
+The following examples illustrate how these axioms can be used, and  in particular one can decide whether or not  a set of statements is consistent.  
+
+<div class="anexample">
+A chain of insertions and removals that starts from statements of the form (1) or (5) leads to a complete characterisation of the contents of the final collection.
+
+<pre class="codeexample">
  entity(c, [prov:type='prov:EmptyCollection']),
  derivedByInsertionFrom(c1, c, E1),
  derivedByInsertionFrom(c2, c1, E2) 
-</span>
-        &rArr;   Contents(c2) = E1 &cup; E2
+</pre>
+From these statements, one entails: Contents(c2) = E1 &cup; E2
+
 
 <p/>Similarly: <p/>
-<span class="name">
+<pre class="codeexample">
  entity(c, [prov:type='prov:EmptyCollection'])
  memberOf(c, E, true)
  derivedByInsertionFrom(c1, c, E1)
  derivedByInsertionFrom(c2, c1, E2) 
-</span>
-        &rArr;   Contents(c2) = E &cup; E1 &cup; E2
+</pre>
+Contents(c2) = E &cup; E1 &cup; E2
 
-<p/>But in other cases, the presence of additional unknown content cannot be excluded, for instance: <p/>
-<span class="name">
+</div>
+
+<div class="anexample">
+Incomplete characterisation  of the contents of the final collection:
+<pre class="codeexample">
  entity(c, [prov:type='prov:Collection'])
  memberOf(c, E)
  derivedByInsertionFrom(c1, c, E1)
-</span>
-        &rArr;   Contents(c1) &sup; E &cup; E1
+</pre>
+This entails:
+        Contents(c1) &sup; E &cup; E1
+</div>
 
 
+<div class="anexample">
+Use of multiple memberOf statements, with no complete flag: 
 
+<pre class="codeexample">
+memberOf(c, E1)
+memberOf(c, E2)
+</pre>
+Contents(c) &sup; E1 &cup; E2
+</div>
+
+<div class="anexample">
+Use of multiple memberOf statements, with one or more complete flags: 
+
+<pre class="codeexample">
+1) memberOf(c, E1, true)  
+2) memberOf(c, E2)
+</pre>
+From (1): Contents(c) = E1   <br/>
+From (2): Contents(c) &sup; E2  <p/>
+
+This is inconsistent unless E2 &sub; E1. In other words, any memberOf statement that adds to an existing "complete" memberOf statement must be contained by the latter. 
+
+<p/>Example:
+
+<pre class="codeexample">
+memberOf(todays-us-supreme-court, {<http://dbpedia.org/resource/John_Glover_Roberts,_Jr.>})   # todays-us-supreme-court  contains at least JGR Jr
+memberOf(todays-us-supreme-court, {Paolo}, true)   # todays-us-supreme-court  contains at least Paolo
+</pre>
+this is inconsistent.  <p/>
+
+<pre class="codeexample">
+(1) memberOf(todays-us-supreme-court, {<http://dbpedia.org/resource/John_Glover_Roberts,_Jr.>})                # todays-us-supreme-court  contains at least JGR Jr
+(2) memberOf(todays-us-supreme-court, {<http://dbpedia.org/resource/John_Glover_Roberts,_Jr.>, Paolo}, true)   # todays-us-supreme-court  contains  Paolo and another dude
+</pre>
+this is consistent because (2) contains (1).<p/>
+</div>
+
+<div class="anexample">
+Multiple derivation statements regarding the same collection.<p/>
+
+Case 1: the deriving collection is the same in both statements. This leads to an inconsistency (except in the trivial case in which the inserted sets are identical).
+
+<pre class="codeexample">
+(1) derivedByInsertionFrom(c1, c, E1)
+(2) derivedByInsertionFrom(c1, c, E2) 
+</pre>
+From (1): Contents(c1) = c &cup; E1   <br/>
+From (2): Contents(c1) = c &cup; E2  <p/>
+
+Case 2: two different deriving collections:
+
+<pre class="codeexample">
+(1) derivedByInsertionFrom(c3, c1, E1)
+(2) derivedByInsertionFrom(c3, c2, E2) 
+</pre>
+From (1): Contents(c3) = c1 &cup; E1   <br/>
+From (2): Contents(c3) = c2 &cup; E2  <p/>
+
+ This is not necessarily an inconsistency.
 </section>
 
 <section id="dictionaries-and-contents">
 
+<!-- PM commented out to avoid confusion to readers in the group 9/6/12 
   
 <h4>Dictionaries and Contents</h4>
 
@@ -450,7 +520,7 @@
 
 </section>
 
-
+-->
 
 <div id="glossary_div" class="remove">
 <!-- glossary loaded from glossary.js will be hooked up here,