--- a/Paper/Paper.thy	Wed Mar 31 05:44:24 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 12:30:17 2010 +0200
@@ -5,7 +5,8 @@
 
 consts
   fv :: "'a \<Rightarrow> 'b"
-  abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
+  abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
+  alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 definition
  "equal \<equiv> (op =)" 
@@ -28,7 +29,9 @@
   Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
   Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
-  supp_gen ("aux _" [1000] 10)
+  supp_gen ("aux _" [1000] 10) and
+  alpha_bn ("_ \<approx>bn _")
+
 (*>*)
 
 
@@ -1367,8 +1370,6 @@
 section {* The Lifting of Definitions and Properties *}
 
 text {*
-%%% TODO Fix 'Andrew Pitts' in bibliography
-
   To define the quotient types we first need to show that the defined
   relations are equivalence relations.
 
@@ -1436,7 +1437,7 @@
   introduced the term has the support equal to @{text "{x}"}. 
 
   To show the support equations for the lifted types we want to use the
-  Lemma \ref{suppabs}, so we start with showing that they have a finite
+  Theorem \ref{suppabs}, so we start with showing that they have a finite
   support.
 
   \begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support.
@@ -1450,6 +1451,7 @@
   sets is finite thus the support of the constructor is finite.
   \end{proof}
 
+% Very vague...
   \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}
    of this type:
   \begin{center}
@@ -1457,9 +1459,31 @@
   \end{center}
   \end{lemma}
   \begin{proof}
-  By induction on the lifted types, together with the equations that characterize
-  @{term "fv_bn"} in terms of @{term "supp"}...
+  We will show this by induction together with equations that characterize
+  @{term "fv_bn\<^isup>\<alpha>\<^isub>"} in terms of @{term "alpha_bn\<^isup>\<alpha>"}. For each of @{text "fv_bn\<^isup>\<alpha>"}
+  functions this equaton is:
+  \begin{center}
+  @{term "{a. infinite {b. \<not> alpha_bn\<^isup>\<alpha> ((a \<rightleftharpoons> b) \<bullet> x) x}} = fv_bn\<^isup>\<alpha> x"}
+  \end{center}
+
+  In the induction we need to show these equations together with the goal
+  for the appropriate constructors. We first transform the right hand sides.
+  The free variable functions are applied to theirs respective constructors
+  so we can apply the lifted free variable defining equations to obtain
+  free variable functions applied to subterms minus binders. Using the
+  induction hypothesis we can replace free variable functions applied to
+  subterms by support. Using Theorem \ref{suppabs} we replace the differences
+  by supports of appropriate abstractions.
+
+  Unfolding the definition of supports on both sides of the equations we
+  obtain by simple calculations the equalities.
   \end{proof}
+
+  With the above equations we can substitute free variables for support in
+  the lifted free variable equations, which gives us the support equations
+  for the term constructors. With this we can show that for each binding in
+  a constructors the bindings can be renamed. 
+
 *}
 
 text {*