--- a/model/working-copy/wd6-collections-constraints.html Fri Jun 08 11:12:06 2012 -0400
+++ b/model/working-copy/wd6-collections-constraints.html Fri Jun 08 20:14:53 2012 +0100
@@ -271,6 +271,50 @@
-->
+
+<section id="dictionaries-and-contents-2">
+
+
+<h4>Collections and Contents take 2</h4>
+
+The interpretation of Collection statements is defined by the following axioms.
+
+Function Contents: C → ℘(E) maps a collection entity c ∈ C to a finite set {e1, … en} ⊂ ℘(E) of entities, where C is the set of all Entities of type Collection, and E is the set of all Entities.
+<ol>
+<li><span class="name">entity(c, [prov:type='prov:EmptyCollection'])</span> ⇒ Contents(c) = ∅
+
+<li> <span class="name">derivedByInsertionFrom(c2, c1, E)</span> ⇒ Contents(c) ⊃ Contents(c1) ∪ E;
+
+<li> <span class="name">derivedByRemovalFrom(c2, c1, E)</span> ⇒ Contents(c) ⊃ Contents(c1) \ E;
+
+<li> <span class="name">memberOf(c, E)</span> ⇒ Contents(c) ⊃ E
+
+<li> <span class="name">memberOf(c, E, true)</span> ⇒ Contents(c) = E
+
+</ol>
+
+Note that a chain of insertions and removals that starts from statements of the form (1) or (2) leads to a precise characterisation of the contents of the resulting collection, for example:
+
+<span class="name">
+ entity(c, [prov:type='prov:EmptyCollection']),
+ derivedByInsertionFrom(c1, c, E1),
+ derivedByInsertionFrom(c2, c1, E2)
+</span>
+ ⇒ Contents(c2) = E1 ∪ E2
+
+<p/>Similarly: <p/>
+<span class="name">
+ entity(c, [prov:type='prov:Collection'])
+ memberOf(c, E, true)
+ derivedByInsertionFrom(c1, c, E1)
+ derivedByInsertionFrom(c2, c1, E2)
+</span>
+ ⇒ Contents(c2) = E ∪ E1 ∪ E2
+
+
+
+</section>
+
<section id="dictionaries-and-contents">