# HG changeset patch
# User urbanc
# Date 1315224436 0
# Node ID e2dc11e12e0b3d414ec0ae8b789e35d960b36096
# Parent  114064363ef0c90dd188e996fedbd7163b8fe952
added section about SUBSEQ and SUPSEQ

diff -r 114064363ef0 -r e2dc11e12e0b Closures2.thy
--- a/Closures2.thy	Sun Sep 04 07:28:48 2011 +0000
+++ b/Closures2.thy	Mon Sep 05 12:07:16 2011 +0000
@@ -1,4 +1,4 @@
-theory Closure2
+theory Closures2
 imports 
   Closures
   Higman
@@ -29,6 +29,7 @@
 
 hide_const A
 hide_const B
+hide_const R
 
 (*
 inductive 
@@ -255,14 +256,12 @@
 definition
   minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
 where
-  "minimal x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
+  "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
 
 lemma main_lemma:
-  shows "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M"
+  shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"
 proof -
   def M \<equiv> "{x \<in> A. minimal x A}"
-  have "M \<subseteq> A" unfolding M_def minimal_def by auto
-  moreover
   have "finite M"
     unfolding M_def minimal_def
     by (rule Higman_antichains) (auto simp add: emb_antisym)
@@ -278,14 +277,14 @@
     then have "z \<in> M"
       unfolding M_def minimal_def
       by (auto intro: emb_trans)
-    with b show "x \<in> SUPSEQ M"
+    with b(2) show "x \<in> SUPSEQ M"
       by (auto simp add: SUPSEQ_def)
   qed
   moreover
   have "SUPSEQ M \<subseteq> SUPSEQ A"
     by (auto simp add: SUPSEQ_def M_def)
   ultimately
-  show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast
+  show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast
 qed
 
 lemma closure_SUPSEQ:
diff -r 114064363ef0 -r e2dc11e12e0b Journal/Paper.thy
--- a/Journal/Paper.thy	Sun Sep 04 07:28:48 2011 +0000
+++ b/Journal/Paper.thy	Mon Sep 05 12:07:16 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Closures" "../Attic/Prefix_subtract" 
+imports "../Closures2" "../Attic/Prefix_subtract" 
 begin
 
 declare [[show_question_marks = false]]
@@ -36,6 +36,7 @@
 abbreviation "TIMES \<equiv> Times"
 abbreviation "TIMESS \<equiv> Timess"
 abbreviation "STAR \<equiv> Star"
+abbreviation "ALLREG \<equiv> Allreg"
 
 definition
   Delta :: "'a lang \<Rightarrow> 'a lang"
@@ -63,7 +64,7 @@
   Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
   Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
   
-  uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
+  uminus ("\<^raw:\ensuremath{\overline{\isa{>_\<^raw:}}}>" [100] 100) and
   tag_Plus ("+tag _ _" [100, 100] 100) and
   tag_Plus ("+tag _ _ _" [100, 100, 100] 100) and
   tag_Times ("\<times>tag _ _" [100, 100] 100) and
@@ -87,7 +88,10 @@
   derivs ("ders") and
   pderiv ("pder") and
   pderivs ("pders") and
-  pderivs_set ("pderss")
+  pderivs_set ("pderss") and
+  SUBSEQ ("Subseq") and
+  SUPSEQ ("Supseq") and
+  UP ("'(_')\<up>")
   
   
 lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union
@@ -124,6 +128,16 @@
   shows "X = \<Union> (lang_trm `  rhs)"
 using assms l_eq_r_in_eqs by (simp)
 
+abbreviation
+  notprec ("_ \<^raw:\mbox{$\not\preceq$}>_")
+where
+ "notprec x y \<equiv> \<not>(x \<preceq> y)"
+
+abbreviation
+  minimal_syn ("min\<^bsub>_\<^esub> _")
+where
+  "minimal_syn A x \<equiv> minimal x A"   
+
 
 (* THEOREMS *)
 
@@ -180,6 +194,9 @@
     by (simp only: length_append)
 qed
 
+
+
+
 (*>*)
 
 
@@ -200,7 +217,7 @@
   that allows quantification over predicate variables. Its type system is
   based on Church's Simple Theory of Types \cite{Church40}.  Although many
   mathematical concepts can be conveniently expressed in HOL, there are some
-  limitations that hurt badly, if one attempts a simple-minded formalisation
+  limitations that hurt badly when attempting a simple-minded formalisation
   of regular languages in it. 
 
   The typical approach (for example \cite{HopcroftUllman69,Kozen97}) to
@@ -361,23 +378,23 @@
   larger formalisations of automata theory are carried out in Nuprl
   \cite{Constable00} and in Coq, e.g.~\cite{Filliatre97,Almeidaetal10}.
 
-  Also one might consider automata theory and regular languages as a meticulously
-  researched subject where everything is crystal clear. However, paper proofs about
-  automata often involve subtle side-conditions which are easily overlooked,
-  but which make formal reasoning rather painful. For example Kozen's proof of
-  the Myhill-Nerode theorem requires that automata do not have inaccessible
-  states \cite{Kozen97}. Another subtle side-condition is completeness of
-  automata, that is automata need to have total transition functions and at
-  most one `sink' state from which there is no connection to a final state
-  (Brzozowski mentions this side-condition in the context of state complexity
-  of automata \cite{Brzozowski10}). Such side-conditions mean that if we
-  define a regular language as one for which there exists \emph{a} finite
-  automaton that recognises all its strings (see Definition~\ref{baddef}), then we
-  need a lemma which ensures that another equivalent one can be found
-  satisfying the side-condition, and also need to make sure our operations on
-  automata preserve them. Unfortunately, such `little' and `obvious'
-  lemmas make a formalisation of automata theory a hair-pulling experience.
-
+  Also one might consider that automata are convenient `vehicles' for
+  establishing properties about regular languages.  However, paper proofs
+  about automata often involve subtle side-conditions which are easily
+  overlooked, but which make formal reasoning rather painful. For example
+  Kozen's proof of the Myhill-Nerode theorem requires that automata do not
+  have inaccessible states \cite{Kozen97}. Another subtle side-condition is
+  completeness of automata, that is automata need to have total transition
+  functions and at most one `sink' state from which there is no connection to
+  a final state (Brzozowski mentions this side-condition in the context of
+  state complexity of automata \cite{Brzozowski10}). Such side-conditions mean
+  that if we define a regular language as one for which there exists \emph{a}
+  finite automaton that recognises all its strings (see
+  Definition~\ref{baddef}), then we need a lemma which ensures that another
+  equivalent one can be found satisfying the side-condition, and also need to
+  make sure our operations on automata preserve them. Unfortunately, such
+  `little' and `obvious' lemmas make a formalisation of automata theory a
+  hair-pulling experience.
 
   In this paper, we will not attempt to formalise automata theory in
   Isabelle/HOL nor will we attempt to formalise automata proofs from the
@@ -405,7 +422,9 @@
   regular expressions. This theorem gives necessary and sufficient conditions
   for when a language is regular. As a corollary of this theorem we can easily
   establish the usual closure properties, including complementation, for
-  regular languages.\medskip
+  regular languages. We also use in one example the continuation lemma, which
+  is based on Myhill-Nerode, for establishing non-regularity of languages 
+  \cite{rosenberg06}.\medskip
   
   \noindent 
   {\bf Contributions:} There is an extensive literature on regular languages.
@@ -704,7 +723,7 @@
   equivalence classes and only finitely many characters.
   The term @{text "\<lambda>(ONE)"} in the first equation acts as a marker for the initial state, that
   is the equivalence class
-  containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
+  containing the empty string @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
   single `initial' state in the equational system, which is different from
   the method by Brzozowski \cite{Brzozowski64}, where he marks the
   `terminal' states. We are forced to set up the equational system in our
@@ -1141,6 +1160,13 @@
   Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} 
   as the regular expression that is needed in the theorem.
   \end{proof}
+
+  \noindent
+  Note that solving our equational system also gives us a method for
+  calculating the regular expression for a complement of a regular language:
+  similar to the construction on automata, if we combine all regular
+  expressions corresponding to equivalence classes not in @{term "finals A"},
+  we obtain a regular expression for the complement @{term "- A"}.
 *}
 
 
@@ -2001,7 +2027,9 @@
   holds for any strings @{text "s\<^isub>1"} and @{text
   "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"}
   give rise to the same partitions. So if one is finite, the other is too, and
-  vice versa. Proving the existence of such a regular expression via
+  vice versa. As noted earlier, our algorithm for solving equational systems
+  actually calculates the regular expression. Calculating this regular expression 
+  via
   automata using the standard method would be quite involved. It includes the
   steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
   "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
@@ -2080,6 +2108,152 @@
   the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pderivs_lang B
   r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that
   @{term "Deriv_lang B A"} is regular.
+
+  Even more surprising is the fact that for every language @{text A}, the language
+  consisting of all substrings of @{text A} is regular \cite{Shallit08, Gasarch09}. 
+  A substring can be obtained
+  by striking out zero or more characters from a string. This can be defined 
+  inductively by the following three rules:
+
+  \begin{center}
+  @{thm[mode=Axiom] emb0[where bs="x"]}\hspace{10mm} 
+  @{thm[mode=Rule] emb1[where as="x" and b="c" and bs="y"]}\hspace{10mm} 
+  @{thm[mode=Rule] emb2[where as="x" and a="c" and bs="y"]}
+  \end{center}
+
+  \noindent
+  It can be easily proved that @{text "\<preceq>"} is a partial order. Now define the 
+  language of substrings and superstrings of a language @{text A}:
+
+  \begin{center}
+  \begin{tabular}{l}
+  @{thm SUBSEQ_def}\\
+  @{thm SUPSEQ_def}
+  \end{tabular}
+  \end{center}
+  
+  \noindent
+  We like to establish
+
+  \begin{lmm}\label{subseqreg}
+  For any language @{text A}, the languages @{term "SUBSEQ A"} and @{term "SUPSEQ A"}
+  are regular.
+  \end{lmm}
+
+  \noindent
+  Our proof follows the one given in \cite[92--95]{Shallit08}, except that we use
+  Higman's lemma, which is already proved in the Isabelle/HOL library. Higman's
+  lemma allows us to prove that every set @{text A} of antichains, namely
+
+  \begin{equation}\label{higman}
+  @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"}
+  \end{equation} 
+
+  \noindent
+  is finite.
+
+  It is straightforward to prove the following properties of @{term SUPSEQ}
+
+  \begin{equation}\label{supseqprops}
+  \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{thm (lhs) SUPSEQ_simps(1)} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_simps(1)}\\  
+  @{thm (lhs) SUPSEQ_simps(2)} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_simps(2)}\\ 
+  @{thm (lhs) SUPSEQ_atom} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_atom}\\ 
+  @{thm (lhs) SUPSEQ_union} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_union}\\
+  @{thm (lhs) SUPSEQ_conc} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_conc}\\
+  @{thm (lhs) SUPSEQ_star} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_star}
+  \end{tabular}}
+  \end{equation}
+
+  \noindent
+  whereby the last equation follows from the fact that @{term "A\<star>"} contains the
+  empty string. With these properties at our disposal we can establish the lemma
+
+  \begin{lmm}
+  If @{text A} is regular, then also @{term "SUBSEQ A"}.
+  \end{lmm}
+
+  \begin{proof}
+  Since our alphabet is finite, we can find a regular expression, written @{const Allreg}, that
+  matches every single-character string. With this regular expression we can inductively define
+  the operation @{text "r\<up>"} over regular expressions
+
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{thm (lhs) UP.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(1)}\\  
+  @{thm (lhs) UP.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(2)}\\ 
+  @{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(3)}\\ 
+  @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & 
+     @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & 
+     @{text "\<equiv>"} & @{thm (rhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) UP.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(6)}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  and using \eqref{supseqprops} establish that @{thm lang_UP}. This shows
+  that @{term "SUBSEQ A"} is regular provided @{text A} is.
+  \end{proof}
+
+  \noindent
+  Now we can prove the main lemma, namely
+
+  \begin{lmm}\label{mset}
+  For every language @{text A}, there exists a finite language @{text M} such that
+  \begin{center}
+  \mbox{@{term "SUPSEQ M = SUPSEQ A"}}\;.
+  \end{center}
+  \end{lmm}
+
+  \begin{proof}
+  For @{text M} we take the set of all minimal elements of @{text A}. An element @{text x} 
+  is minimal in @{text A} provided
+
+  \begin{center}
+  @{thm minimal_def}
+  \end{center}
+
+  \noindent
+  By Higman's lemma \eqref{higman} we know
+  that @{text "M"} is finite, since every minimal element is incomparable, 
+  except with itself.
+  It is also straightforward to show that @{term "SUPSEQ M \<subseteq> SUPSEQ A"}. For
+  the other direction we have  @{term "x \<in> SUPSEQ A"}. From this we can obtain 
+  a @{text y} such that @{term "y \<in> A"} and @{term "y \<preceq> x"}. Since we know that
+  the relation \mbox{@{term "{(y, x). y \<preceq> x \<and> x \<noteq> y}"}} is well-founded, there must
+  be a minimal element @{text "z"} such that @{term "z \<in> A"} and @{term "z \<preceq> y"}, 
+  and hence by transitivity also \mbox{@{term "z \<preceq> x"}} (here we deviate from the argument 
+  given in \cite{Shallit08}, because Isabelle/HOL provides already an extensive infrastructure
+  for reasoning about well-foundedness). Since @{term "z"} is
+  minimal and in @{term A}, we also know that @{term z} is in @{term M}.
+  From this together with @{term "z \<preceq> x"}, we can infer that @{term x} is in 
+  @{term "SUPSEQ M"} as required.
+  \end{proof}
+
+  \noindent
+  This lemma allows us to establish the second part of Lemma~\ref{subseqreg}.
+
+  \begin{proof}[The Second Part of Lemma~\ref{subseqreg}]
+  Given any language @{text A}, by Lemma~\ref{mset} we know there exists
+  a finite, and thus regular, language @{text M}. We further have @{term "SUPSEQ M = SUPSEQ A"},
+  which establishes the second part.    
+  \end{proof}
+
+  \noindent
+  In order to establish the first part of Lemma~\ref{subseqreg} we use the
+  property proved in \cite{Shallit08}
+
+  \begin{equation}\label{compl}
+  @{thm SUBSEQ_complement}
+  \end{equation}
+
+  \begin{proof}[The First Part of Lemma~\ref{subseqreg}]
+  By the second part of Lemma~\ref{subseqreg}, we know the right-hand side of \eqref{compl}
+  is regular, which means the complement of @{term "SUBSEQ A"} is regular. But since
+  we established already that regularity is preserved under complement, also @{term "SUBSEQ A"}
+  must be regular. 
+  \end{proof}
 *}
 
 
diff -r 114064363ef0 -r e2dc11e12e0b Journal/ROOT.ML
--- a/Journal/ROOT.ML	Sun Sep 04 07:28:48 2011 +0000
+++ b/Journal/ROOT.ML	Mon Sep 05 12:07:16 2011 +0000
@@ -1,4 +1,4 @@
-no_document use_thy "../Closures";
+no_document use_thy "../Closures2";
 no_document use_thy "../Attic/Prefix_subtract";
 
 use_thy "Paper"
\ No newline at end of file
diff -r 114064363ef0 -r e2dc11e12e0b Journal/document/mathpartir.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/mathpartir.sty	Mon Sep 05 12:07:16 2011 +0000
@@ -0,0 +1,388 @@
+%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+%  Copyright (C) 2001, 2002, 2003 Didier Rémy
+%
+%  Author         : Didier Remy 
+%  Version        : 1.1.1
+%  Bug Reports    : to author
+%  Web Site       : http://pauillac.inria.fr/~remy/latex/
+% 
+%  WhizzyTeX is free software; you can redistribute it and/or modify
+%  it under the terms of the GNU General Public License as published by
+%  the Free Software Foundation; either version 2, or (at your option)
+%  any later version.
+%  
+%  Mathpartir is distributed in the hope that it will be useful,
+%  but WITHOUT ANY WARRANTY; without even the implied warranty of
+%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%  GNU General Public License for more details 
+%  (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%  File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+    [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+\newdimen \mpr@tmpdim
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing 
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+  \edef \MathparNormalpar
+     {\noexpand \lineskiplimit \the\lineskiplimit
+      \noexpand \lineskip \the\lineskip}%
+  }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+  \let \and \mpr@andcr
+  \let \par \mpr@andcr
+  \let \\\mpr@cr
+  \let \eqno \mpr@eqno
+  \let \hva \mpr@hva
+  } 
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+     \noindent $\displaystyle\fi
+     \MathparBindings}
+  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
+  \vbox \bgroup \tabskip 0em \let \+ \cr
+  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+  \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \+\qquad $#1$}\ifnum \wd0 < \hsize
+      \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\+{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\+{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \+#1\+#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\+#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+   \mpr@lista {\+}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
+   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+     \mpr@flatten \mpr@all \mpr@to \mpr@one
+     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+     \mpr@all \mpr@stripend  
+     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+     \ifx 1\mpr@isempty
+   \repeat
+}
+
+%% Part III -- Type inference rules
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+   \def \+##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+   \setbox \mpr@hlist
+      \hbox {\strut
+             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+             \unhbox \mpr@hlist}%
+   \setbox \mpr@vlist
+      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+             \else \unvbox \mpr@vlist \box \mpr@hlist
+             \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+%    \setbox \mpr@hlist
+%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+%    \setbox \mpr@vlist
+%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+%              \else \unvbox \mpr@vlist \box \mpr@hlist
+%              \fi}%
+% }
+
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+  \bgroup
+  \ifx #1T\@premissetrue
+  \else \ifx #1B\@premissefalse
+  \else
+     \PackageError{mathpartir}
+       {Premisse orientation should either be P or B}
+       {Fatal error in Package}%
+  \fi \fi
+  \def \@test {#2}\ifx \@test \mpr@blank\else
+  \setbox \mpr@hlist \hbox {}%
+  \setbox \mpr@vlist \vbox {}%
+  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+  \let \@hvlist \empty \let \@rev \empty
+  \mpr@tmpdim 0em
+  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+  \def \+##1{%
+     \def \@test {##1}\ifx \@test \empty
+        \mpr@htovlist
+        \mpr@tmpdim 0em %%% last bug fix not extensively checked
+     \else
+      \setbox0 \hbox{$\displaystyle {##1}$}\relax
+      \advance \mpr@tmpdim by \wd0
+      %\mpr@tmpdim 1.02\mpr@tmpdim
+      \ifnum \mpr@tmpdim < \hsize
+         \ifnum \wd\mpr@hlist > 0
+           \if@premisse
+             \setbox \mpr@hlist 
+                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+           \else
+             \setbox \mpr@hlist
+                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
+           \fi
+         \else 
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+         \fi
+      \else
+         \ifnum \wd \mpr@hlist > 0
+            \mpr@htovlist 
+            \mpr@tmpdim \wd0
+         \fi
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+      \fi
+      \advance \mpr@tmpdim by \mpr@sep
+   \fi
+   }%
+   \@rev
+   \mpr@htovlist
+   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+   \fi
+   \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+    \let\@@over\over % fallback if amsmath is not loaded
+    \let\@@overwithdelims\overwithdelims
+    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+  }{}
+
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\@@over #2}$}}
+\let \mpr@fraction \mpr@@fraction
+\def \mpr@@reduce #1#2{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+  {\bgroup
+     \ifnum \linewidth<\hsize \hsize \linewidth\fi
+     \mpr@rulelineskip
+     \let \and \qquad
+     \let \hva \mpr@hva
+     \let \@rulename \mpr@empty
+     \let \@rule@options \mpr@empty
+     \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+  {\everymath={\displaystyle}%       
+   \def \@test {#2}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+   \else 
+   \def \@test {#3}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+   \else
+   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+   \fi \fi
+   \def \@test {#1}\ifx \@test\empty \box0
+   \else \vbox 
+%%% Suggestion de Francois pour les etiquettes longues
+%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+      {\hbox {\RefTirName {#1}}\box0}\fi
+   \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \+
+% Each \+ produces a break, attempting horizontal breaks if possible, 
+% and  vertical breaks if needed. 
+% 
+% An empty element obtained by \+\+ produces a vertical break in all cases. 
+%
+% The former rule is aligned on the fraction bar. 
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+% 
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%       
+%  width                set the width of the rule to val
+%  narrower             set the width of the rule to val\hsize
+%  before               execute val at the beginning/left
+%  lab                  put a label [Val] on top of the rule
+%  lskip                add negative skip on the right
+%  left                 put a left label [Val]
+%  Left                 put a left label [Val],  ignoring its width 
+%  right                put a right label [Val]
+%  Right                put a right label [Val], ignoring its width
+%  leftskip             skip negative space on the left-hand side
+%  rightskip            skip negative space on the right-hand side
+%  vdots                lift the rule by val and fill vertical space with dots
+%  after                execute val at the end/right
+%  
+%  Note that most options must come in this order to avoid strange
+%  typesetting (in particular  leftskip must preceed left and Left and
+%  rightskip must follow Right or right; vdots must come last 
+%  or be only followed by rightskip. 
+%  
+
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\def \mprset #1{\setkeys{mprset}{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newdimen \rule@dimen
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+         \setbox \mpr@right \hbox{}%
+         $\setkeys{mpr}{#1}%
+          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+          \box \mpr@right \mpr@vdots$}
+  \setbox1 \hbox {\strut}
+  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
+  \raise \rule@dimen \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode 
+    \let \@do \mpr@inferstar@
+  \else 
+    \let \@do \mpr@err@skipargs
+    \PackageError {mathpartir}
+      {\string\inferrule* can only be used in math mode}{}%
+  \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \tir@name #1{\hbox {\small \sc #1}}
+\let \TirName \tir@name
+\let \RefTirName \tir@name
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
diff -r 114064363ef0 -r e2dc11e12e0b Journal/document/root.bib
--- a/Journal/document/root.bib	Sun Sep 04 07:28:48 2011 +0000
+++ b/Journal/document/root.bib	Mon Sep 05 12:07:16 2011 +0000
@@ -1,3 +1,26 @@
+@article{Gasarch09,
+  author    = {S.~A.~Fenner and W.~I.~Gasarch and B.~Postow},
+  title     = {{T}he {C}omplexity of {F}inding {SUBSEQ(A)}},
+  journal   = {Theory Computing Systems},
+  volume    = {45},
+  number    = {3},
+  year      = {2009},
+  pages     = {577-612}
+}
+
+@Book{Shallit08,
+  author = 	 {J.~Shallit},
+  title = 	 {{A} {S}econd {C}ourse in {F}ormal {L}anguages and {A}utomata {T}heory},
+  publisher = 	 {Cambridge University Press},
+  year = 	 {2008}
+}
+
+@Unpublished{Rosenberg06,
+  author = 	 {A.~L.~Rosenberg},
+  title = 	 {{A} {B}ig {I}deas {A}pproach to the {T}heory of {C}omputation},
+  note = 	 {Course notes for CMPSCI 401 at the University of Massachusetts},
+  year = 	 {2006}
+}
 
 @incollection{myhillnerodeafp11,
   author =       {C.~Wu and X.~Zhang and C.~Urban},
diff -r 114064363ef0 -r e2dc11e12e0b Journal/document/root.tex
--- a/Journal/document/root.tex	Sun Sep 04 07:28:48 2011 +0000
+++ b/Journal/document/root.tex	Mon Sep 05 12:07:16 2011 +0000
@@ -15,7 +15,7 @@
 %%\usepackage{proof}
 %%\usepackage{mathabx}
 \usepackage{stmaryrd}
-
+\usepackage{mathpartir}
 
 \urlstyle{rm}
 \isabellestyle{it}