--- a/model/prov-constraints.html	Wed Aug 08 15:25:01 2012 +0200
+++ b/model/prov-constraints.html	Wed Aug 08 14:45:26 2012 +0100
@@ -544,13 +544,13 @@
 concept called <a title="normal form">normalization</a>.  Definitions, inferences,
 and uniqueness constraints can be applied to <a title="normal
 form">normalize</a> PROV instances, and event ordering, typing, and
-impossibility constraints are checked on the normal form to determine
+impossibility constraints can be checked on the normal form to determine
 <a title="valid">validity</a>.  Equivalence of two PROV 
 instances can be determined by comparing their normal forms.
 </p>
 <p>
 This document outlines an algorithm for validity checking based on
-<a title="normal form">noramlization</a>.  Applications MAY implement
+<a title="normal form">normalization</a>.  Applications MAY implement
 validity and equivalence checking using normalization, as suggested
 here, or in
 any other way as long as the same instances are considered valid or
@@ -1498,7 +1498,7 @@
   missing activity, generation, and usage. In the latter form, it is not specified
   if one or more activities are involved in the derivation. </p>
 
- <p>Let us consider a system, in which a derivation is underpinned by multiple activities. Conceptually, one could also model such a system with a new activity that encompasses the two original activities and underpins the derivation.   The infererences defined in this specification do not allow the latter modelling to be inferred from the former. Hence, the two  modellings of the same system are regarded as different in the context of this specification.</p>
+ <p>Let us consider a system, in which a derivation is underpinned by multiple activities. Conceptually, one could also model such a system with a new activity that encompasses the two original activities and underpins the derivation.   The inferences defined in this specification do not allow the latter modelling to be inferred from the former. Hence, the two  modellings of the same system are regarded as different in the context of this specification.</p>
     </div>
 </section>
     
@@ -1578,7 +1578,7 @@
   nontermination.  For example, once we have an activity we can yse
   activity-start-end-inference and start-type-inference forever to
   infer an infinite chain of activities, each starting the next.
-  Similarly, we can use inverence-activity-start-end,
+  Similarly, we can use inference-activity-start-end,
 start-type-inference, entity-generation-invalidation-inference,
   and generation-type-inference forever to infer an infinite chain of
   entities generated by activities that were started by entities that
@@ -1725,7 +1725,7 @@
 <div class="remark" id="derivation-generation-use-inference-remark">
   <p>
  <a class="rule-text" href="#derivation-use-inference"><span>TBD</span></a> allows "-" to be replaced by existential variables in a <span
-  class="name">wasDerivedFrom</span>, when an activity is explict, and a generation known.</p>
+  class="name">wasDerivedFrom</span>, when an activity is explicit, and a generation known.</p>
 
 <p> However, a derivation without explicit generation and usage cannot be normalized even when a generation and usage hold.   
 <span class='conditional'>IF</span> 
@@ -2199,7 +2199,7 @@
   whether the constraint can be satisfied by instantiating some existential
   variables with other terms.  For key constraints, this is the same
   as merging pairs of statements whose keys are equal and whose
-  coresponding arguments are compatible, because after
+  corresponding arguments are compatible, because after
   merging respective arguments and attribute lists, the two statements
   become equal and one can be omitted. </p>
   
@@ -2535,7 +2535,7 @@
 rectangle, or intersecting usage and generation edges).  The ordering
 constraints are represented by triangles: an occurrence of a triangle between two <a title="instantaneous event">instantaneous event</a> vertical dotted lines represents that the event denoted by the left
 line precedes the event denoted by the right line.</p>
-  <div class="note"> Miscellanous suggestions about figures
+  <div class="note"> Miscellaneous suggestions about figures
   (originally from Tim Lebo):
 <ul>
   <li>
@@ -3526,8 +3526,8 @@
 <div class="remark">
 
   Implementations should decide up front what reasoning about
-  coreference should be applied, and rewrite the instance (by
-  replacing coreferent identifiers with a single common identifier) to
+  co-reference should be applied, and rewrite the instance (by
+  replacing co-referent identifiers with a single common identifier) to
   make this explicit, before doing validation, equivalence checking,
   or normalization.
   All of the following definitions assume that the application has
@@ -3786,11 +3786,25 @@
  -->
 <!--  LocalWords:  disambiguating lifecycle conformant minimalistic Lamport fo
  -->
-<!--  LocalWords:  reflexivity antisymmetry timelines timespan WG concl inv
+<!--  LocalWords:  reflexivity antisymmetry timelines timespan WG concl inv TBD
  -->
-<!--  LocalWords:  continuant occurrent modalities toyota womanInRedDress
+<!--  LocalWords:  continuant occurrent modalities toyota womanInRedDress provn
  -->
 <!--  LocalWords:  customerInChairAt manWithGlasses customerInChair irreflexive
  -->
-<!--  LocalWords:  wasStartedByActivity antisymmetric wasInvalidatedBy
+<!--  LocalWords:  wasStartedByActivity antisymmetric wasInvalidatedBy stmt CHR
  -->
+<!--  LocalWords:  DBCONSTRAINTS formalisms URIs wasInfluencedBy definitional
+ -->
+<!--  LocalWords:  wasInvalidated th  nontermination  implementability att evt
+ -->
+<!--  LocalWords:  Irreflexivity mentionOf preorder equalities unsatisfiable
+ -->
+<!--  LocalWords:  Lebo subfigures pre del irreflexivity superproperty typeOf
+ -->
+<!--  LocalWords:  disjointness inferrable subtyping subtype subtypes hadMember
+ -->
+<!--  LocalWords:  hasMember toplevel sameAs tuple acyclicity isomorphism
+ -->
+<!--  LocalWords:  endBundle
+ -->