--- a/Quotient-Paper/Paper.thy	Thu May 27 16:06:43 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu May 27 16:33:10 2010 +0200
@@ -376,20 +376,40 @@
   by appropriate aggregate relations. It is defined as follows:
 
   \begin{itemize}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
+  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
+  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
   \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
   \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
   \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
-  \item @{text "REG (_, v) = v"}
-  \item @{text "REG (_, c) = c"}
+  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
+  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
   \end{itemize}
 
   Existential quantifiers and unique existential quantifiers are defined
   similarily to the universal one.
 
+  The function that gives the statment of the injected theorem
+  takes the statement of the regularized theorems and the statement
+  of the lifted theorem both as terms.
+
+  \begin{itemize}
+  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
+  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
+  \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
+  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
+  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
+  \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
+  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
+  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
+  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
+  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
+  \end{itemize}
+
+  For existential quantifiers and unique existential quantifiers it is
+  defined similarily to the universal one.
+
 *}
 
 subsection {* Proof of Regularization *}