--- a/rdf-mt/index.html	Wed Oct 30 22:20:55 2013 +0100
+++ b/rdf-mt/index.html	Wed Oct 30 19:38:21 2013 -0500
@@ -1210,25 +1210,25 @@
 
 <section class="informative appendix"><h2 id="proofs">Proofs of some results (Informative)</h2>
 
-<p class="fact"> The <a>empty graph</a> is entailed by
-  any graph, and does not entail any graph except itself.
+<p class="fact"> The <a>empty graph</a> is simply entailed by
+  any graph, and does not simply entail any graph except itself.
 <!-- <a href="#emptygraphlemmaprf" class="termref">[Proof]</a> -->
 </p>
 
 <p>The empty graph is true in all simple interpretations, so is entailed by any graph. If G contains a triple &lt;a b c&gt;, then any simple interpretation I with IEXT(I(b))={ } makes G false; so the empty graph does not entail G. QED.</p>
 
-<p class="fact"> A graph entails all its subgraphs.
+<p class="fact"> A graph simply entails all its subgraphs.
 <!-- <a href="#subglemprf" class="termref">[Proof]</a> -->
 </p>
 <p>If I satisfies G then it satisfies every triple in G, hence every triple in any subset of G. QED.</p>
 
 <p class="fact"> A graph
-  is entailed by any of its <a>instance</a>s.
+  is simply entailed by any of its <a>instance</a>s.
 <!-- <a href="#instlemprf" class="termref"> [Proof]</a> -->
 </p>
 <p>Suppose H is an instance of G with the instantiation mapping M, and that I satisfies H. For blank nodes n in G which are not in H define A(n)=I(M(n)); then I+A satisfies G, so I satisfies G. QED.</p>
 
-<p class="fact">Every graph is satisfiable.</p>
+<p class="fact">Every graph is simply satisfiable.</p>
 <p>Consider the simple interpretation with universe {x}, IEXT(x)= &lt;x,x &gt; and I(aaa)=x for any IRI aaa. This interpretation satisfies every RDF graph. QED.</p>
 
 <p class="fact">
@@ -1237,12 +1237,12 @@
 
 <p>If a subgraph E' of G is an instance of E then G entails E' which entails E, so G entails E. Now suppose G entails E, and consider the <a href="http://en.wikipedia.org/wiki/Herbrand_interpretation">Herbrand interpretation</a> I of G defined as follows.  IR contains the <a>name</a>s and blank nodes which occur in the graph, with I(n)=n for each <a>name</a> n; n is in IP and &lt;a, b&gt; in IEXT(n) just when the triple &lt;a n b&gt; is in the graph. (For IRIs which do not occur in the graph, assign them values in IR at random.) I satisfies every triple &lt;s p o&gt; in E; that is, for some mapping A from the blank nodes of E to the vocabulary of G, the triple &lt;[I+A](s) I(p) [I+A](o)&gt; occurs in G. But this is an instance of &lt;s p o&gt; under the instance mapping A; so an instance of E is a subgraph of G. QED.</p>
 
-<p class="fact">if E is lean and E' is a proper instance of E, then E does not entail E'.</p>
+<p class="fact">if E is lean and E' is a proper instance of E, then E does not simply entail E'.</p>
 <p>Suppose E entails E', then a subgraph of E is an instance of E', which is a proper instance of E; so a subgraph of E is a proper instance of E, so E is not lean. QED.</p>
-<p class="fact">If E contains an IRI which does not occur in S, then S does not entail E.</p>
+<p class="fact">If E contains an IRI which does not occur in S, then S does not simply entail E.</p>
 <p>IF S entails E then a subgraph of S is an instance of E, so every IRI in E must occur in that subgraph, so must occur in S. QED.</p>
 
-<p class="fact">For any graph H, if sk(G) entails H there there is a graph H' such that G entails H' and H=sk(H').</p>
+<p class="fact">For any graph H, if sk(G) simply entails H there there is a graph H' such that G entails H' and H=sk(H').</p>
 <p>The skolemization mapping sk substitutes a unique new IRI for each blank node, so it is 1:1, so has an inverse. Define ks to be the inverse mapping which replaces each skolem IRI by the blank node it replaced. Since sk(G) entails H, a subgraph of sk(G) is an instance of H, say A(H) for some instance mapping A on the blank nodes in H. Then ks(A(H)) is a subgraph of G; and ks(A(H))=A(ks(H)) since the domains of A and ks are disjoint. So ks(H) has an instance which is a subgraph of G, so is entailed by G; and H=sk(ks(H)). QED.</p>
 
 <p class="fact">For any graph H which does not contain any of the "new" IRIs introduced into sk(G), sk(G) simply entails H if and only if G simply entails H.</p>