lexing: comparison thys/Paper/Paper.thy

equal deleted inserted replaced

-:44fec0bfffe5
+:ac831326441c
 \noindent
 We can assume that
 \begin{equation}
-(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{2l}, v_{2r})
+Seq\,v_{1l}\, v_{1r}) \posix_{r_1\,r_2} Seq\,v_{2l}\, v_{2r})
 \qquad\textrm{and}\qquad
-(v_{2l}, v_{2r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})
+Seq\,v_{2l}\, v_{2r}) \posix_{r_1\,r_2} Seq\,v_{3l}\, v_{3r})
 \label{assms}
 \end{equation}
 \noindent
 hold, and furthermore that the values have equal length,
 \noindent
 We need to show that
 \[
-(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})
+(v_{1l}, v_{1r}) \posix_{r_1\,r_2} (v_{3l}, v_{3r})
 \]
 \noindent 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}
+v_{1l} \posix_{r_1} v_{2l}
 \qquad\textrm{and}\qquad
-v_{2l} \posix^{r_1} v_{3l}
+v_{2l} \posix_{r_1} v_{3l}
 \]
 \noindent and also know the corresponding typing 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
 \qquad\textrm{and}\qquad
 |v_{1r}| \not= |v_{2r}|
 \]
 \noindent but still \eqref{lens} will hold. Now we are stuck,
-since the IH does not apply. Sulzmann and Lu overlook this
+since the IH does not apply.
-fact and just apply the IHs. Obviously nothing which a
-theorem prover allows us to do.
 *}
 section {* Conclusion *}