
diff -r 71f4ecc08849 -r 702ed601349b thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Fri Mar 11 21:21:09 2016 +0000
+++ b/thys/Paper/Paper.thy	Sun Mar 13 01:07:34 2016 +0000
@@ -1,6 +1,9 @@
 (*<*)
 theory Paper
-imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar"
+imports 
+   "../ReStar"
+   "../Sulzmann" 
+   "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 declare [[show_question_marks = false]]
@@ -23,7 +26,7 @@
   STAR ("_\<^sup>\<star>" [1000] 78) and
   
   val.Void ("'(')" 79) and
-  val.Char ("Char _" [1000] 79) and
+  val.Char ("Char _" [1000] 78) and
   val.Left ("Left _" [79] 78) and
   val.Right ("Right _" [79] 78) and
   val.Seq ("Seq _ _" [79,79] 78) and
@@ -36,7 +39,7 @@
   Sequ ("_ @ _" [78,77] 63) and
   injval ("inj _ _ _" [79,77,79] 76) and 
   mkeps ("mkeps _" [79] 76) and 
-  length ("len _" [78] 73) and
+  length ("len _" [73] 73) and
  
   Prf ("_ : _" [75,75] 75) and  
   Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
@@ -50,7 +53,10 @@
   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and
   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
-  slexer ("lexer\<^sup>+ _ _" [78,78] 77)
+  slexer ("lexer\<^sup>+ _ _" [78,78] 77) and
+
+  ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and
+  ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
 
 definition 
   "match r s \<equiv> nullable (ders s r)"
@@ -897,8 +903,8 @@
 section {* The Correctness Argument by Sulzmmann and Lu *}
 
 text {*
-  \newcommand{\greedy}{\succcurlyeq_{gr}}
-  \newcommand{\posix}{>}
+%  \newcommand{\greedy}{\succcurlyeq_{gr}}
+ \newcommand{\posix}{>}
 
   An extended version of \cite{Sulzmann2014} is available at the website of
   its first author; this includes some ``proofs'', claimed in
@@ -909,198 +915,179 @@
   rules (slightly adapted to fit our notation):
 
 \begin{center}  
-\begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}		 
-$\infer{v_{1} \posix_{r_{1}} v'_{1}} 
-       {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v'_{1}\,v'_{2}}(C2)$
-&
-$\infer{v_{2} \posix_{r_{2}} v'_{2}} 
-       {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$
-\smallskip\\
-		
-		
-$\infer{ len |v_{2}| > len |v_{1}|} 
-       {Right \; v_{2} \posix_{r_{1}+r_{2}} Left \; v_{1}}(A1)$ 
-&
-$\infer{ len |v_{1}| \geq len |v_{2}|} 
-       {Left \; v_{1} \posix_{r_{1}+r_{2}} Right \; v_{2}} (A2)$ 
-\smallskip\\	
+\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	
+@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]}(C2) &
+@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}(C1)\smallskip\\
+
+@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}(A1) &
+@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}(A2)\smallskip\\
 
-$\infer{ v_{2} \posix_{r_{2}} v'_{2}} 
-       {Right \; v_{2} \posix_{r_{1}+r_{2}} Right \; v'_{2}}(A3)$ & 
-
-$\infer{ v_{1} \posix_{r_{1}} v'_{1}} 
-       {Left \; v_{1} \posix_{r_{1}+r_{2}} Left \; v'_{1}}(A4)$ 
-\smallskip\\
+@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}(A3) &
+@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}(A4)\smallskip\\
 
- $\infer{|v :: vs| = []} {Stars\,[] \posix_{r^{\star}} Stars\,(v :: vs)}(K1)$ & 
- $\infer{|v :: vs| \neq []} {Stars\,(v :: vs) \posix_{r^{\star}} Stars\,[]}(K2)$
-\smallskip\\
-	
-$\infer{ v_{1} \posix_{r} v_{2}} 
-       {Stars\,(v_{1} :: vs_{1}) \posix_{r^{\star}} Stars\,(v_{2} :: vs_{2})}(K3)$ & 
-$\infer{ Stars\,vs_{1} \posix_{r^{\star}} Stars\,vs_{2}} 
-       {Stars\,(v :: vs_{1}) \posix_{r^{\star}} Stars\,(v :: vs_{2})}(K4)$	
+@{thm[mode=Rule] K1[of "v" "vs" "r"]}(K1) &
+@{thm[mode=Rule] K2[of "v" "vs" "r"]}(K2)\smallskip\\
+
+@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}(K3) &
+@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}(K4)
 \end{tabular}
 \end{center}
 
-  \noindent
-  The idea behind the rules $(A1)$ and $(A2)$, for example, is that a $Left$-value is
-  bigger than a $Right$-value, if the underlying string of the $Left$-value is
-  longer or of equal length to the underlying string of the $Right$-value. The order
-  is reversed, however, if the $Right$-value can match longer string than a $Left$-value.
-  In this way the POSIX value is supposed to be the biggest value
-  for a given string and regular expression.
+  \noindent The idea behind the rules (A1) and (A2), for example, is that a
+  @{text Left}-value is bigger than a @{text Right}-value, if the underlying
+  string of the @{text Left}-value is longer or of equal length to the
+  underlying string of the @{text Right}-value. The order is reversed,
+  however, if the @{text Right}-value can match a longer string than a
+  @{text Left}-value. In this way the POSIX value is supposed to be the
+  biggest value for a given string and regular expression.
 
   Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch
   and Cardelli from where they have taken the idea for their correctness
-  proof. Frisch and Cardelli introduced a
-  similar ordering for GREEDY matching and they show that their GREEDY
-  matching algorithm always produces a maximal element according to this
-  ordering (from all possible solutions). The only difference between their
-  GREEDY ordering and the ``ordering'' by Sulzmann and Lu is that GREEDY, if
-  possible, always prefers a $Left$-value over a $Right$-value, no matter
-  what the underlying string is. This seems to be only a very minor
-  difference, but it has drastic consequences in terms of what
-  properties both orderings enjoy. What is interesting for our purposes is
-  that the properties reflexivity, totality and transitivity for this GREEDY
-  ordering can be proved relatively easily by induction.
+  proof. Frisch and Cardelli introduced a similar ordering for GREEDY
+  matching and they showed that their GREEDY matching algorithm always
+  produces a maximal element according to this ordering (from all possible
+  solutions). The only difference between their GREEDY ordering and the
+  ``ordering'' by Sulzmann and Lu is that GREEDY always prefers a @{text
+  Left}-value over a @{text Right}-value, no matter what the underlying
+  string is. This seems to be only a very minor difference, but it has
+  drastic consequences in terms of what properties both orderings enjoy.
+  What is interesting for our purposes is that the properties reflexivity,
+  totality and transitivity for this GREEDY ordering can be proved
+  relatively easily by induction.
 
   These properties of GREEDY, however, do not transfer to the POSIX
-  ``ordering'' by Sulzmann and Lu. To start with, $v \geq_r v'$ is not
-  defined inductively, but as $v = v'$ or $v >_r v' \wedge |v| = |v'|$. This
-  means that $v >_r v'$ does not imply $v \geq_r v'$. Moreover, transitivity
-  does not hold in the ``usual'' formulation, for example:
+  ``ordering'' by Sulzmann and Lu. To start with, @{text "v\<^sub>1 \<ge>r v\<^sub>2"} is
+  not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r
+  v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1
+  >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)
+  (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
+  formulation, for example:
+
+  \begin{proposition}
+  Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.
+  If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
+  then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
+  \end{proposition}
+
+  \noindent If formulated in this way, then there are various counter
+  examples: For example let @{term r} be @{text "a + ((a + a)\<cdot>(a + \<zero>))"}
+  then the @{term "v\<^sub>1"}, @{term "v\<^sub>2"} and @{term "v\<^sub>3"} below are values
+  of @{term r}:
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{term "v\<^sub>1"} & $=$ & @{term "Left(Char a)"}\\
+  @{term "v\<^sub>2"} & $=$ & @{term "Right(Seq (Left(Char a)) (Right Void))"}\\
+  @{term "v\<^sub>3"} & $=$ & @{term "Right(Seq (Right(Char a)) (Left(Char a)))"}
+  \end{tabular}
+  \end{center}
 
-\begin{proposition}
-Suppose $v_1 : r$, $v_2 : r$ and $v_3 : r$.
-If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$
-then $v_1 \posix_r v_3$.
-\end{proposition}
+  \noindent Moreover @{term "v\<^sub>1 >(r::rexp) v\<^sub>2"} and @{term "v\<^sub>2 >(r::rexp)
+  v\<^sub>3"}, but \emph{not} @{term "v\<^sub>1 >(r::rexp) v\<^sub>3"}! The reason is that
+  although @{term "v\<^sub>3"} is a @{text "Right"}-value, it can match a longer
+  string, namely @{term "flat v\<^sub>3 = [a,a]"}, while @{term "flat v\<^sub>1"} (and
+  @{term "flat v\<^sub>2"}) matches only @{term "[a]"}. So transitivity in this
+  formulation does not hold---in this example actually @{term "v\<^sub>3
+  >(r::rexp) v\<^sub>1"}!
+
+  Sulzmann and Lu ``fix'' this problem by weakening the transitivity
+  property. They require in addition that the underlying strings are of the
+  same length. This excludes the counter example above and any
+  counter-example we were able to find (by hand and by machine). Thus the
+  transitivity lemma should be formulated as:
 
-\noindent If formulated in this way, then there are various counter examples:
-For example let $r$ be $a + ((a + a)\cdot (a + \textbf{0}))$ then the $v_1$,
-$v_2$ and $v_3$ below are values of $r$:
+  \begin{proposition}
+  Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"},
+  and also @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}.\\
+  If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
+  then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
+  \end{proposition}
+
+  \noindent While we agree with Sulzmann and Lu that this property
+  probably(!) holds, proving it seems not so straightforward: although one
+  begins with the assumption that the values have the same flattening, this
+  cannot be maintained as one descends into the induction. This is a problem
+  that occurs in a number of places in the proofs by Sulzmann and Lu.
+
+  Although they do not give an explicit proof of the transitivity property,
+  they give a closely related property about the existence of maximal
+  elements. They state that this can be verified by an induction on $r$. We
+  disagree with this as we shall show next in case of transitivity. The case
+  where the reasoning breaks down is the sequence case, say @{term "SEQ r\<^sub>1 r\<^sub>2"}.
+  The induction hypotheses in this case are
 
 \begin{center}
-\begin{tabular}{lcl}
- $v_1$ & $=$ & $Left(Char\;a)$\\
- $v_2$ & $=$ & $Right((Left(Char\;a), Right()))$\\
- $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$
-\end{tabular}
-\end{center}
-
-\noindent Moreover $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$,
-but \emph{not} $v_1 \posix_r v_3$! The reason is that although
-$v_3$ is a $Right$-value, it can match a longer string, namely
-$|v_3| = [a,a]$, while $|v_1|$ (and $|v_2|$) matches only $[a]$. So
-transitivity in this formulation does not hold---in this
-example actually $v_3 \posix_r v_1$!
-
-Sulzmann and Lu ``fix'' this problem by weakening the
-transitivity property. They require in addition that the
-underlying strings are of the same length. This excludes the
-counter example above and any counter-example we were able 
-to find (by hand and by machine). Thus the transitivity 
-lemma should be formulated as:
-
-\begin{proposition}
-Suppose $v_1 : r$, $v_2 : r$ and 
-$v_3 : r$, and also $|v_1|=|v_2|=|v_3|$.\\
-If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$
-then $v_1 \posix_r v_3$.
-\end{proposition}
-
-\noindent While we agree with Sulzmann and Lu that this property probably(!)
-holds, proving it seems not so straightforward: although one begins with the
-assumption that the values have the same flattening, this
-cannot be maintained as one descends into the induction. This is 
-a problem that occurs in a number of places in the proofs by Sulzmann and Lu.
-
-Although they do not give an explicit proof
-of the transitivity property, they give a closely related
-property about the existence of maximal elements. They state
-that this can be verified by an induction on $r$. We disagree
-with this as we shall show next in case of transitivity.
-The case where the reasoning breaks down is the sequence case,
-say $r_1\cdot r_2$. The induction hypotheses in this case
-are
-
-\begin{center}
-\begin{tabular}{@ {}cc@ {}}
-\begin{tabular}{@ {}ll@ {}}
-IH $r_1$:\\
-$\forall v_1, v_2, v_3.$ 
-  & $v_1 : r_1\;\wedge$
-    $v_2 : r_1\;\wedge$
-    $v_3 : r_1\;\wedge$\\
-  & $|v_1|=|v_2|=|v_3|\;\wedge$\\
-  & $v_1 \posix_{r_1} v_2\;\wedge\; v_2 \posix_{r_1} v_3$\medskip\\
-  & $\;\;\Rightarrow v_1 \posix_{r_1} v_3$
+\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}
+IH @{term "r\<^sub>1"}:\\
+@{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."} \\
+  & @{term "\<turnstile> v\<^sub>1 : r\<^sub>1"}\;@{text "\<and>"}
+    @{term "\<turnstile> v\<^sub>2 : r\<^sub>1"}\;@{text "\<and>"}
+    @{term "\<turnstile> v\<^sub>3 : r\<^sub>1"}\\
+  & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
+  & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>1::rexp) v\<^sub>3"}\medskip\\
+  & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>3"}
 \end{tabular} &
-\begin{tabular}{@ {}ll@ {}}
-IH $r_2$:\\
-$\forall v_1, v_2, v_3.$ 
-  & $v_1 : r_2\;\wedge$
-    $v_2 : r_2\;\wedge$
-    $v_3 : r_2\;\wedge$\\
-  & $|v_1|=|v_2|=|v_3|\;\wedge$\\
-  & $v_1 \posix_{r_2} v_2\;\wedge\; v_2 \posix_{r_2} v_3$\medskip\\
-  & $\;\;\Rightarrow v_1 \posix_{r_2} v_3$
+\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}
+IH @{term "r\<^sub>2"}:\\
+@{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."}\\ 
+  & @{term "\<turnstile> v\<^sub>1 : r\<^sub>2"}\;@{text "\<and>"}
+    @{term "\<turnstile> v\<^sub>2 : r\<^sub>2"}\;@{text "\<and>"}
+    @{term "\<turnstile> v\<^sub>3 : r\<^sub>2"}\\
+  & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
+  & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>2::rexp) v\<^sub>3"}\medskip\\
+  & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>3"}
 \end{tabular}
 \end{tabular}
 \end{center} 
 
-\noindent
-We can assume that 
-
-\begin{equation}
-Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} Seq\,v_{2l}\, v_{2r}
-\qquad\textrm{and}\qquad
-Seq\,v_{2l}\, v_{2r} \posix_{r_1\cdot r_2} Seq\,v_{3l}\, v_{3r}
-\label{assms}
-\end{equation}
+  \noindent We can assume that
+  %
+  \begin{equation}
+  @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}
+  \qquad\textrm{and}\qquad
+  @{term "(Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}
+  \label{assms}
+  \end{equation}
 
-\noindent
-hold, and furthermore that the values have equal length, 
-namely:
+  \noindent hold, and furthermore that the values have equal length, namely:
+  %
+  \begin{equation}
+  @{term "flat (Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) = flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}
+  \qquad\textrm{and}\qquad
+  @{term "flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) = flat (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}
+  \label{lens}
+  \end{equation} 
 
-\begin{equation}
-|Seq\,v_{1l}\, v_{1r}| = |Seq\,v_{2l}\, v_{2r}|
-\qquad\textrm{and}\qquad
-|Seq\,v_{2l}\, v_{2r}| = |Seq\,v_{3l}\, v_{3r}|
-\label{lens}
-\end{equation}
-
-\noindent We need to show that $Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2}
-Seq\, v_{3l}\, v_{3r}$ holds. We can proceed by analysing how the
-assumptions in \eqref{assms} have arisen. There are four cases. Let us
-assume we are in the case where we know
+  \noindent We need to show that @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2)
+  (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} holds. We can proceed by analysing how the
+  assumptions in \eqref{assms} have arisen. There are four cases. Let us
+  assume we are in the case where we know
 
-\[
-v_{1l} \posix_{r_1} v_{2l}
-\qquad\textrm{and}\qquad
-v_{2l} \posix_{r_1} v_{3l}
-\]
+  \[
+  @{term "v\<^sub>1\<^sub>l >(r\<^sub>1::rexp) v\<^sub>2\<^sub>l"}
+  \qquad\textrm{and}\qquad
+  @{term "v\<^sub>2\<^sub>l >(r\<^sub>1::rexp) v\<^sub>3\<^sub>l"}
+  \]
 
-\noindent and also know the corresponding inhabitation judgements.
-This is exactly a case where we would like to apply the
-induction hypothesis IH~$r_1$. But we cannot! We still need to
-show that $|v_{1l}| = |v_{2l}|$ and $|v_{2l}| = |v_{3l}|$. We
-know from \eqref{lens} that the lengths of the sequence values
-are equal, but from this we cannot infer anything about the
-lengths of the component values. Indeed in general they will
-be unequal, that is 
+  \noindent and also know the corresponding inhabitation judgements. This is
+  exactly a case where we would like to apply the induction hypothesis
+  IH~$r_1$. But we cannot! We still need to show that @{term "flat (v\<^sub>1\<^sub>l) =
+  flat(v\<^sub>2\<^sub>l)"} and @{term "flat(v\<^sub>2\<^sub>l) = flat(v\<^sub>3\<^sub>l)"}. We know from
+  \eqref{lens} that the lengths of the sequence values are equal, but from
+  this we cannot infer anything about the lengths of the component values.
+  Indeed in general they will be unequal, that is
 
-\[
-|v_{1l}| \not= |v_{2l}|  
-\qquad\textrm{and}\qquad
-|v_{1r}| \not= |v_{2r}|
-\]
+  \[
+  @{term "flat(v\<^sub>1\<^sub>l) \<noteq> flat(v\<^sub>2\<^sub>l)"}  
+  \qquad\textrm{and}\qquad
+  @{term "flat(v\<^sub>1\<^sub>r) \<noteq> flat(v\<^sub>2\<^sub>r)"}
+  \]
 
-\noindent but still \eqref{lens} will hold. Now we are stuck,
-since the IH does not apply. As said, this problem where the
-induction hypothesis does not apply arises in several places in
-the proof of Sulzmann and Lu, not just for proving transitivity.
+  \noindent but still \eqref{lens} will hold. Now we are stuck, since the IH
+  does not apply. As said, this problem where the induction hypothesis does
+  not apply arises in several places in the proof of Sulzmann and Lu, not
+  just for proving transitivity.
 
 *}
 




