
diff -r 26e44bcddb5b -r 3e71af53cedb Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Apr 02 13:12:10 2010 +0200
+++ b/Paper/Paper.thy	Fri Apr 02 15:28:55 2010 +0200
@@ -213,7 +213,7 @@
   The scope of the binding is indicated by labels given to the types, for
   example @{text "s::trm"}, and a binding clause, in this case
   \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
-  clause states to bind in @{text s} all the names the function call @{text
+  clause states to bind in @{text s} all the names the function @{text
   "bn(as)"} returns.  This style of specifying terms and bindings is heavily
   inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
@@ -554,7 +554,13 @@
  
   \noindent
   From property \eqref{equivariancedef} and the definition of @{text supp}, we 
-  can be easily deduce that equivariant functions have empty support.
+  can be easily deduce that equivariant functions have empty support. There is
+  also a similar notion for equivariant relations, say @{text R}, namely the property
+  that
+  %
+  \begin{center}
+  @{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+  \end{center}
 
   Finally, the nominal logic work provides us with convenient means to rename 
   binders. While in the older version of Nominal Isabelle, we used extensively 
@@ -925,9 +931,9 @@
 
   \begin{center}
   \begin{tabular}{l}
-  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\
-  \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\
-  \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+  \isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\
+  \isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\
+  \isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\
   \end{tabular}
   \end{center}
 
@@ -1114,10 +1120,10 @@
 
 
   The datatype definition can be obtained by stripping off the 
-  binding clauses and the labels on the types. We also have to invent
+  binding clauses and the labels from the types. We also have to invent
   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
   given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
-  But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
+  But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is defined over alpha-equivalence classes and leave it out 
   for the corresponding notion defined on the ``raw'' level. So for example 
   we have
@@ -1143,12 +1149,6 @@
   @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
   \end{equation}
   
-  % TODO: we did not define permutation types
-  %\noindent
-  %From this definition we can easily show that the raw datatypes are 
-  %all permutation types (Def ??) by a simple structural induction over
-  %the @{text "ty"}s.
-
   The first non-trivial step we have to perform is the generation free-variable 
   functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
   we need to define free-variable functions
@@ -1160,7 +1160,7 @@
   \noindent
   We define them together with auxiliary free-variable functions for
   the binding functions. Given binding functions 
-  @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we need to define
+  @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
   %
   \begin{center}
   @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
@@ -1168,7 +1168,7 @@
 
   \noindent
   The reason for this setup is that in a deep binder not all atoms have to be
-  bound, as we shall see in an example below. We need therefore a function
+  bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
   that calculates those unbound atoms. 
 
   While the idea behind these
@@ -1177,7 +1177,7 @@
   somewhat involved.
   Given a term-constructor @{text "C"} of type @{text ty} with argument types
   \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
-  @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
+  @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values, @{text v},
   calculated below for each argument. 
   First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, 
   we can determine whether the argument is a shallow or deep
@@ -1187,10 +1187,10 @@
   \begin{equation}\label{deepbinder}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-  $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+  $\bullet$ & @{term "v = {}"} provided @{text "x\<^isub>i"} is a shallow binder\\
+  $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
       non-recursive binder with the auxiliary binding function @{text "bn"}\\
-  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
+  $\bullet$ & @{text "v = fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
       a deep recursive binder with the auxiliary binding function @{text "bn"}
   \end{tabular}}
   \end{equation}
@@ -1215,14 +1215,14 @@
   \begin{equation}\label{deepbody}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
-  $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
-  $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
-  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
+  $\bullet$ & @{text "v = {atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
+  $\bullet$ & @{text "v = (atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
+  $\bullet$ & @{text "v = (atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
+  $\bullet$ & @{text "v = (fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
      corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
 %     with a free-variable function @{text "fv\<^isup>\<alpha>"}\\
-  $\bullet$ & @{term "{}"} otherwise
+  $\bullet$ & @{term "v = {}"} otherwise
   \end{tabular}}
   \end{equation}
 
@@ -1249,9 +1249,9 @@
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-   $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
+   $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
     recursive call @{text "bn x\<^isub>i"}\medskip\\
-  $\bullet$ & @{term "{}"} provided @{text "rhs"} contains
+  $\bullet$ & @{term "v = {}"} provided @{text "rhs"} contains
     @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
   \end{tabular}
   \end{center}
@@ -1438,7 +1438,7 @@
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
   \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
-  {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}\medskip\\
+  {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
   \end{tabular}
   \end{center}
 
@@ -1446,7 +1446,7 @@
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
   \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
-  {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\medskip\\
+  {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
   \end{tabular}
   \end{center}
 
@@ -1455,7 +1455,7 @@
   $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of 
   the components in an assignment that are \emph{not} bound. Therefore we have
   a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is 
-  a non-recursive binder). The reason is that the terms inside an assignment are not meant 
+  a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant 
   to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 
   because there everything from the assignment is under the binder. 
 *}
@@ -1541,21 +1541,21 @@
   In fact we can from now on lift facts from the raw level to the alpha-equated level
   as long as they contain raw term-constructors only. The 
   induction principles derived by the datatype package in Isabelle/HOL for the types @{text
-  "ty\<AL>\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
+  "ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
   induction principles that establish
 
   \begin{center}
-  @{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "}
+  @{text "P\<^bsub>ty\<AL>\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^isub>n\<^esub> y\<^isub>n "}
   \end{center} 
 
   \noindent
-  for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties
+  for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^isub>i\<^esub>"} stand for properties
   defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of 
   these induction principles look
   as follows
 
   \begin{center}
-  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 
+  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<AL>\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 
   \end{center}
 
   \noindent
@@ -1606,7 +1606,7 @@
 
   \noindent
   are alpha-equivalent. This gives us conditions when the corresponding
-  alpha-equated terms are equal, namely
+  alpha-equated terms are \emph{equal}, namely
 
   \begin{center}
   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}
@@ -1617,7 +1617,7 @@
   we have to lift in the next section, we completed
   the lifting part of establishing the reasoning infrastructure. 
 
-  Working bow completely on the alpha-equated level, we can first show that 
+  By working now completely on the alpha-equated level, we can first show that 
   the free-variable functions and binding functions
   are equivariant, namely
 
@@ -1763,17 +1763,17 @@
   \noindent
   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 
   The problem with this implication is that in general it is not easy to establish it.
-  The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"} 
+  The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"} 
   (for example we cannot assume the variable convention for them).
 
   In \cite{UrbanTasson05} we introduced a method for automatically
   strengthening weak induction principles for terms containing single
   binders. These stronger induction principles allow the user to make additional
-  assumptions about binders when proving the induction hypotheses. 
+  assumptions about binders. 
   These additional assumptions amount to a formal
   version of the informal variable convention for binders. A natural question is
   whether we can also strengthen the weak induction principles involving
-  general binders. We will indeed be able to so, but for this we need an 
+  the general binders presented here. We will indeed be able to so, but for this we need an 
   additional notion for permuting deep binders. 
 
   Given a binding function @{text "bn"} we define an auxiliary permutation 
@@ -1796,7 +1796,7 @@
   \end{center}
   
   \noindent
-  Using the quotient package again we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
+  Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
   alpha-equated terms. We can then prove the following two facts
 
   \begin{lemma}\label{permutebn} 
@@ -1806,7 +1806,7 @@
   \end{lemma}
 
   \begin{proof} 
-  By induction on @{text x}. The equation follow by simple unfolding 
+  By induction on @{text x}. The equations follow by simple unfolding 
   of the definitions. 
   \end{proof}
 
@@ -1822,19 +1822,19 @@
   \eqref{letpat} this means for a permutation @{text "r"}:
   %
   \begin{equation}\label{renaming}
-  \mbox{if @{term "supp (Abs_lst (bn p) t)  \<sharp>* r"} 
-  then @{text "Let p t = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (r \<bullet> t)"}}
+  \begin{array}{l}
+  \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
+  \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+  \end{array}
   \end{equation}
 
   \noindent
-  This fact will be used when establishing the strong induction principles. 
-  
-
+  This fact will be crucial when establishing the strong induction principles. 
   In our running example about @{text "Let"}, they state that instead 
   of establishing the implication 
 
   \begin{center}
-  @{text "\<forall>p t. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t)"}
+  @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
   \end{center}
 
   \noindent
@@ -1842,9 +1842,10 @@
   %
   \begin{equation}\label{strong}
   \mbox{\begin{tabular}{l}
-  @{text "\<forall>p t c."}\\
-  \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t)"}\\
-  \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
+  @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
+  \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
+  \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
+  \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
   \end{tabular}}
   \end{equation}
 
@@ -1865,54 +1866,59 @@
   \end{equation} 
 
   \noindent
-  For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t)"} 
-  assuming \eqref{hyps} as induction hypotheses. By Property~\ref{avoiding} we
+  For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} 
+  assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). 
+  By Property~\ref{avoiding} we
   obtain a permutation @{text "r"} such that 
   %
   \begin{equation}\label{rprops}
   @{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
-  @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t)) \<sharp>* r"}
+  @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
   \end{equation}
 
   \noindent
   hold. The latter fact and \eqref{renaming} give us
 
   \begin{center}
-  @{text "Let (q \<bullet> p) (q \<bullet> t) = Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t))"}
+  \begin{tabular}{l}
+  @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
+  \hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
+  \end{tabular}
   \end{center}
 
   \noindent
-  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t)"}, we are can equally
+  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we are can equally
   establish
 
   \begin{center}
-  @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t)))"}
+  @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}
   \end{center}
 
   \noindent
   To do so, we will use the implication \eqref{strong} of the strong induction
   principle, which requires us to discharge
-  the following three proof obligations:
+  the following four proof obligations:
 
   \begin{center}
   \begin{tabular}{rl}
   {\it i)} &   @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
   {\it ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
-  {\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t))"}\\
+  {\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+  {\it iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
   \end{tabular}
   \end{center}
 
   \noindent
   The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it i)}; the 
-  second and third from the induction hypotheses in \eqref{hyps} (in the latter case
-  we have to use the fact that @{term "(r \<bullet> (q \<bullet> t)) = (r + q) \<bullet> t"}).
+  others from the induction hypotheses in \eqref{hyps} (in the fourth case
+  we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
 
   Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
   we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
   This completes the proof showing that the strong induction principle derives from
   the weak induction principle. At the moment we can derive the difficult cases of 
   the strong induction principles only by hand, but they are very schematically 
-  so that with little effort we can even derive the strong induction principle for 
+  so that with little effort we can even derive them for 
   Core-Haskell given in Figure~\ref{nominalcorehas}. 
 *}
 
@@ -1930,8 +1936,8 @@
   approach to binding \cite{chargueraud09}.  There, de-Bruijn indices consist
   of two numbers, one referring to the place where a variable is bound and the
   other to which variable is bound. The reasoning infrastructure for both
-  representations of bindings comes for free in the theorem provers Isabelle/HOL and
-  Coq, for example, as the corresponding term-calculi can be implemented as ``normal''
+  representations of bindings comes for free in the theorem provers, like Isabelle/HOL or
+  Coq, as the corresponding term-calculi can be implemented as ``normal''
   datatypes.  However, in both approaches it seems difficult to achieve our
   fine-grained control over the ``semantics'' of bindings (i.e.~whether the
   order of binders should matter, or vacuous binders should be taken into
@@ -1980,7 +1986,7 @@
   Because of how we set up our definitions, we had to impose restrictions,
   like excluding overlapping deep binders, that are not present in Ott. Our
   expectation is that we can still cover many interesting term-calculi from
-  programming language research, for example Core-Haskell. For prviding support
+  programming language research, for example Core-Haskell. For providing support
   of neat features in Ott, such as subgrammars, the existing datatype
   infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the
   other hand, we are not aware that Ott can make the distinction between our
@@ -2058,7 +2064,7 @@
   This suggest there should be an approriate notion of alpha-equivalence.
 
   Another interesting line of investigation is whether we can go beyond the 
-  simple-minded form of binding function we adopted from Ott. At the moment, binding
+  simple-minded form for binding functions that we adopted from Ott. At the moment, binding
   functions can only return the empty set, a singleton atom set or unions
   of atom sets (similarly for lists). It remains to be seen whether 
   properties like \eqref{bnprop} provide us with means to support more interesting




