--- a/Quotient-Paper/Paper.thy Fri Aug 27 16:00:19 2010 +0800
+++ b/Quotient-Paper/Paper.thy Fri Aug 27 19:06:30 2010 +0800
@@ -16,10 +16,6 @@
- explain how Quotient R Abs Rep is proved (j-version)
- give an example where precise specification helps (core Haskell in nominal?)
- - Quote from Peter:
-
- One might think quotient have been studied to death, but
-
- Mention Andreas Lochbiler in Acknowledgements and 'desceding'.
*)
@@ -29,16 +25,17 @@
pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
"op -->" (infix "\<longrightarrow>" 100) and
"==>" (infix "\<Longrightarrow>" 100) and
- fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
- fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
+ fun_map ("_ \<singlearr> _" 51) and
+ fun_rel ("_ \<doublearr> _" 51) and
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
fempty ("\<emptyset>") and
funion ("_ \<union> _") and
finsert ("{_} \<union> _") and
Cons ("_::_") and
concat ("flat") and
- fconcat ("\<Union>")
-
+ fconcat ("\<Union>") and
+ Quotient ("Quot _ _ _")
+
ML {*
@@ -358,7 +355,8 @@
we can get back to \eqref{adddef}.
In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
of the type-constructor @{text \<kappa>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
- type of @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. For example @{text "map_list"}
+ type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}.
+ For example @{text "map_list"}
has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
In our implementation we maintain
a database of these map-functions that can be dynamically extended.
@@ -390,7 +388,7 @@
An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
\end{definition}
- \begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}
+ \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
@{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
\end{definition}
@@ -402,28 +400,32 @@
Given a relation $R$, an abstraction function $Abs$
and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
holds if and only if
- \begin{enumerate}
- \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
- \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
- \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
- \end{enumerate}
+ \begin{isabelle}\ \ \ \ \ %%%%
+ \begin{tabular}{rl}
+ (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R", no_vars]}\end{isa}\\
+ (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R", no_vars]}\end{isa}\\
+ (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R", no_vars]}\end{isa}\\
+ \end{tabular}
+ \end{isabelle}
\end{definition}
\noindent
- The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can
- often be proved in terms of the validity of @{text "Quotient"} over the constituent
+ The value of this definition lies in the fact that validity of @{term "Quotient R Abs Rep"} can
+ often be proved in terms of the validity of @{term "Quot"} over the constituent
types of @{text "R"}, @{text Abs} and @{text Rep}.
For example Homeier proves the following property for higher-order quotient
types:
\begin{proposition}\label{funquot}
+ \begin{isa}
@{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
+ \end{isa}
\end{proposition}
\noindent
As a result, Homeier is able to build an automatic prover that can nearly
- always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+ always discharge a proof obligation involving @{text "Quot"}. Our quotient
package makes heavy
use of this part of Homeier's work including an extension
for dealing with compositions of equivalence relations defined as follows:
@@ -431,7 +433,7 @@
%%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
%%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
- \begin{definition}[Composition of Relations]
+ \begin{definition}%%[Composition of Relations]
@{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
composition defined by
@{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
@@ -450,11 +452,15 @@
with @{text R} being an equivalence relation, then
\begin{isabelle}\ \ \ \ \ %%%
- @{text "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ @{text "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
+ & @{text "(Abs_fset \<circ> map_list Abs)"}\\
+ & @{text "(map_list Rep \<circ> Rep_fset)"}\\
+ \end{tabular}
\end{isabelle}
*}
-section {* Quotient Types and Quotient Definitions\label{sec:type} *}
+section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
text {*
The first step in a quotient construction is to take a name for the new
@@ -521,7 +527,7 @@
(for the proof see \cite{Homeier05}).
\begin{proposition}
- @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
+ @{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
\end{proposition}
The next step in a quotient construction is to introduce definitions of new constants
@@ -568,20 +574,19 @@
%
\begin{center}
\hfill
- \begin{tabular}{rcl}
- \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
- @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
- @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
- @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
- @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
- @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
- @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
- \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\\
- @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
- @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
+ \begin{tabular}{@ {\hspace{2mm}}l@ {}}
+ \multicolumn{1}{@ {}l}{equal types:}\\
+ @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+ @{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
+ \multicolumn{1}{@ {}l}{function types:}\\
+ @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+ @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
+ \multicolumn{1}{@ {}l}{equal type constructors:}\\
+ @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
+ @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
+ \multicolumn{1}{@ {}l}{unequal type constructors:}\\
+ @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
+ @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
\end{tabular}\hfill\numbered{ABSREP}
\end{center}
%
@@ -597,7 +602,7 @@
type as follows:
%
\begin{center}
- \begin{tabular}{rcl}
+ \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
@{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
@{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
@@ -640,7 +645,10 @@
the abstraction function
\begin{isabelle}\ \ \ \ \ %%%
- @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+ \begin{tabular}{l}
+ @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\
+ \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}
+ \end{tabular}
\end{isabelle}
\noindent
@@ -705,7 +713,7 @@
\end{proof}
*}
-section {* Respectfulness and Preservation \label{sec:resp} *}
+section {* Respectfulness and\\ Preservation \label{sec:resp} *}
text {*
The main point of the quotient package is to automatically ``lift'' theorems
@@ -717,10 +725,12 @@
notable is the bound variable function, that is the constant @{text bn}, defined
for raw lambda-terms as follows
- \begin{isabelle}\ \ \ \ \ %%%
+ \begin{isabelle}
+ \begin{center}
@{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
- @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
+ @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\smallskip\\
@{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+ \end{center}
\end{isabelle}
\noindent
@@ -744,20 +754,19 @@
\begin{center}
\hfill
- \begin{tabular}{rcl}
- \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
- @{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
- @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
- \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\smallskip\\
- @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
+ \begin{tabular}{l}
+ \multicolumn{1}{@ {}l}{equal types:}\\
+ @{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+ \multicolumn{1}{@ {}l}{equal type constructors:}\\
+ @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+ \multicolumn{1}{@ {}l}{unequal type constructors:}\\
+ @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
\end{tabular}\hfill\numbered{REL}
\end{center}
\noindent
The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
- we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
+ again we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
@{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching
@{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
@@ -957,27 +966,27 @@
the structure of @{text "raw_thm"} and @{text "quot_thm"} as follows:
\begin{center}
- \begin{tabular}{rcl}
- \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
- @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ &
+ \begin{tabular}{l}
+ \multicolumn{1}{@ {}l}{abstractions:}\smallskip\\
+ @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\smallskip\\
\\
- \multicolumn{3}{@ {}l}{universal quantifiers:}\\
- @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ &
+ \multicolumn{1}{@ {}l}{universal quantifiers:}\\
+ @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\smallskip\\
- \multicolumn{3}{@ {}l}{equality:}\smallskip\\
+ \multicolumn{1}{@ {}l}{equality:}\smallskip\\
%% REL of two equal types is the equality so we do not need a separate case
- @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
- \multicolumn{3}{@ {}l}{applications, variables and constants:}\\
- @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
- @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
- @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
+ @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
+ \multicolumn{1}{@ {}l}{applications, variables and constants:}\\
+ @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} $\dn$ @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
+ @{text "REG (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
+ @{text "REG (c\<^isub>1, c\<^isub>2)"} $\dn$ @{text "c\<^isub>1"}\\
\end{tabular}
\end{center}
%
@@ -991,26 +1000,26 @@
terms) and returns @{text "inj_thm"}:
\begin{center}
- \begin{tabular}{rcl}
- \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
- @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ &
- $\begin{cases}
+ \begin{tabular}{l}
+ \multicolumn{1}{@ {}l}{abstractions:}\\
+ @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
+ \hspace{18mm}$\begin{cases}
@{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
- \end{cases}$\\
- @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$
- & @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
- @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\
- @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
- @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
- @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+ \end{cases}$\smallskip\\
+ @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
+ \hspace{18mm}@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+ \multicolumn{1}{@ {}l}{universal quantifiers:}\\
+ @{text "INJ (\<forall> t, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s)"}\\
+ @{text "INJ (\<forall> t \<in> R, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+ \multicolumn{1}{@ {}l}{applications, variables and constants:}\smallskip\\
+ @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} $\dn$ @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
+ @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} $\dn$
$\begin{cases}
@{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
\end{cases}$\\
- @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+ @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} $\dn$
$\begin{cases}
@{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\