# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1354806769 0
# Node ID a04084de4946144aba278765d721e9338affd641
# Parent  c4783e4ef43f5ffd7e2e826465733e1f0798c723
added

diff -r c4783e4ef43f -r a04084de4946 IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IsaMakefile	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,51 @@
+
+## targets
+
+default: itp
+all: session itp slides1
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+
+USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
+
+
+## Slides
+
+session1: Slides/ROOT1.ML \
+	Slides/document/root* \
+	Slides/Slides1.thy
+	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
+
+slides1: session1
+	rm -f Slides/generated/*.aux # otherwise latex will fall over
+	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
+
+# main files                        
+
+session: ./ROOT.ML ./*.thy
+	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
+
+
+# itp paper
+
+itp: Paper/*.thy Paper/*.ML 
+	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
+	rm -f Paper/generated/*.aux # otherwise latex will fall over  
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
+	cd Paper/generated ; bibtex root
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+	cp Paper/generated/root.pdf paper.pdf 
+
+
+slides: Slides/ROOT1.ML Slides/*.thy 
+	@$(USEDIR) -D generated -f ROOT1.ML Prio Slides
+	rm -f Slides/generated/*.aux # otherwise latex will fall over
+	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
+
diff -r c4783e4ef43f -r a04084de4946 Paper/Paper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/Paper.thy	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,1345 @@
+(*<*)
+theory Paper
+imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
+begin
+
+(*
+find_unused_assms CpsG 
+find_unused_assms ExtGG 
+find_unused_assms Moment 
+find_unused_assms Precedence_ord 
+find_unused_assms PrioG 
+find_unused_assms PrioGDef
+*)
+
+ML {*
+  open Printer;
+  show_question_marks_default := false;
+  *}
+
+notation (latex output)
+  Cons ("_::_" [78,77] 73) and
+  vt ("valid'_state") and
+  runing ("running") and
+  birthtime ("last'_set") and
+  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+  Prc ("'(_, _')") and
+  holding ("holds") and
+  waiting ("waits") and
+  Th ("T") and
+  Cs ("C") and
+  readys ("ready") and
+  depend ("RAG") and 
+  preced ("prec") and
+  cpreced ("cprec") and
+  dependents ("dependants") and
+  cp ("cprec") and
+  holdents ("resources") and
+  original_priority ("priority") and
+  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
+
+(*abbreviation
+ "detached s th \<equiv> cntP s th = cntV s th"
+*)
+(*>*)
+
+section {* Introduction *}
+
+text {*
+  Many real-time systems need to support threads involving priorities and
+  locking of resources. Locking of resources ensures mutual exclusion
+  when accessing shared data or devices that cannot be
+  preempted. Priorities allow scheduling of threads that need to
+  finish their work within deadlines.  Unfortunately, both features
+  can interact in subtle ways leading to a problem, called
+  \emph{Priority Inversion}. Suppose three threads having priorities
+  $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
+  $H$ blocks any other thread with lower priority and the thread itself cannot
+  be blocked indefinitely by threads with lower priority. Alas, in a naive
+  implementation of resource locking and priorities this property can
+  be violated. For this let $L$ be in the
+  possession of a lock for a resource that $H$ also needs. $H$ must
+  therefore wait for $L$ to exit the critical section and release this
+  lock. The problem is that $L$ might in turn be blocked by any
+  thread with priority $M$, and so $H$ sits there potentially waiting
+  indefinitely. Since $H$ is blocked by threads with lower
+  priorities, the problem is called Priority Inversion. It was first
+  described in \cite{Lampson80} in the context of the
+  Mesa programming language designed for concurrent programming.
+
+  If the problem of Priority Inversion is ignored, real-time systems
+  can become unpredictable and resulting bugs can be hard to diagnose.
+  The classic example where this happened is the software that
+  controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
+  Once the spacecraft landed, the software shut down at irregular
+  intervals leading to loss of project time as normal operation of the
+  craft could only resume the next day (the mission and data already
+  collected were fortunately not lost, because of a clever system
+  design).  The reason for the shutdowns was that the scheduling
+  software fell victim to Priority Inversion: a low priority thread
+  locking a resource prevented a high priority thread from running in
+  time, leading to a system reset. Once the problem was found, it was
+  rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
+  \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
+  Inheritance Protocol} \cite{Sha90} and others sometimes also call it
+  \emph{Priority Boosting} or \emph{Priority Donation}.} in the scheduling software.
+
+  The idea behind PIP is to let the thread $L$ temporarily inherit
+  the high priority from $H$ until $L$ leaves the critical section
+  unlocking the resource. This solves the problem of $H$ having to
+  wait indefinitely, because $L$ cannot be blocked by threads having
+  priority $M$. While a few other solutions exist for the Priority
+  Inversion problem, PIP is one that is widely deployed and
+  implemented. This includes VxWorks (a proprietary real-time OS used
+  in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
+  ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
+  example in libraries for FreeBSD, Solaris and Linux. 
+
+  One advantage of PIP is that increasing the priority of a thread
+  can be dynamically calculated by the scheduler. This is in contrast
+  to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
+  solution to the Priority Inversion problem, which requires static
+  analysis of the program in order to prevent Priority
+  Inversion. However, there has also been strong criticism against
+  PIP. For instance, PIP cannot prevent deadlocks when lock
+  dependencies are circular, and also blocking times can be
+  substantial (more than just the duration of a critical section).
+  Though, most criticism against PIP centres around unreliable
+  implementations and PIP being too complicated and too inefficient.
+  For example, Yodaiken writes in \cite{Yodaiken02}:
+
+  \begin{quote}
+  \it{}``Priority inheritance is neither efficient nor reliable. Implementations
+  are either incomplete (and unreliable) or surprisingly complex and intrusive.''
+  \end{quote}
+
+  \noindent
+  He suggests avoiding PIP altogether by designing the system so that no 
+  priority inversion may happen in the first place. However, such ideal designs may 
+  not always be achievable in practice.
+
+  In our opinion, there is clearly a need for investigating correct
+  algorithms for PIP. A few specifications for PIP exist (in English)
+  and also a few high-level descriptions of implementations (e.g.~in
+  the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
+  with actual implementations. That this is a problem in practice is
+  proved by an email by Baker, who wrote on 13 July 2009 on the Linux
+  Kernel mailing list:
+
+  \begin{quote}
+  \it{}``I observed in the kernel code (to my disgust), the Linux PIP
+  implementation is a nightmare: extremely heavy weight, involving
+  maintenance of a full wait-for graph, and requiring updates for a
+  range of events, including priority changes and interruptions of
+  wait operations.''
+  \end{quote}
+
+  \noindent
+  The criticism by Yodaiken, Baker and others suggests another look
+  at PIP from a more abstract level (but still concrete enough
+  to inform an implementation), and makes PIP a good candidate for a
+  formal verification. An additional reason is that the original
+  presentation of PIP~\cite{Sha90}, despite being informally
+  ``proved'' correct, is actually \emph{flawed}. 
+
+  Yodaiken \cite{Yodaiken02} points to a subtlety that had been
+  overlooked in the informal proof by Sha et al. They specify in
+  \cite{Sha90} that after the thread (whose priority has been raised)
+  completes its critical section and releases the lock, it ``returns
+  to its original priority level.'' This leads them to believe that an
+  implementation of PIP is ``rather straightforward''~\cite{Sha90}.
+  Unfortunately, as Yodaiken points out, this behaviour is too
+  simplistic.  Consider the case where the low priority thread $L$
+  locks \emph{two} resources, and two high-priority threads $H$ and
+  $H'$ each wait for one of them.  If $L$ releases one resource
+  so that $H$, say, can proceed, then we still have Priority Inversion
+  with $H'$ (which waits for the other resource). The correct
+  behaviour for $L$ is to switch to the highest remaining priority of
+  the threads that it blocks. The advantage of formalising the
+  correctness of a high-level specification of PIP in a theorem prover
+  is that such issues clearly show up and cannot be overlooked as in
+  informal reasoning (since we have to analyse all possible behaviours
+  of threads, i.e.~\emph{traces}, that could possibly happen).\medskip
+
+  \noindent
+  {\bf Contributions:} There have been earlier formal investigations
+  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
+  checking techniques. This paper presents a formalised and
+  mechanically checked proof for the correctness of PIP (to our
+  knowledge the first one).  In contrast to model checking, our
+  formalisation provides insight into why PIP is correct and allows us
+  to prove stronger properties that, as we will show, can help with an
+  efficient implementation of PIP in the educational PINTOS operating
+  system \cite{PINTOS}.  For example, we found by ``playing'' with the
+  formalisation that the choice of the next thread to take over a lock
+  when a resource is released is irrelevant for PIP being correct---a
+  fact that has not been mentioned in the literature and not been used
+  in the reference implementation of PIP in PINTOS.  This fact, however, is important
+  for an efficient implementation of PIP, because we can give the lock
+  to the thread with the highest priority so that it terminates more
+  quickly.
+*}
+
+section {* Formal Model of the Priority Inheritance Protocol *}
+
+text {*
+  The Priority Inheritance Protocol, short PIP, is a scheduling
+  algorithm for a single-processor system.\footnote{We shall come back
+  later to the case of PIP on multi-processor systems.} 
+  Following good experience in earlier work \cite{Wang09},  
+  our model of PIP is based on Paulson's inductive approach to protocol
+  verification \cite{Paulson98}. In this approach a \emph{state} of a system is
+  given by a list of events that happened so far (with new events prepended to the list). 
+  \emph{Events} of PIP fall
+  into five categories defined as the datatype:
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
+  \isacommand{datatype} event 
+  & @{text "="} & @{term "Create thread priority"}\\
+  & @{text "|"} & @{term "Exit thread"} \\
+  & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\
+  & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
+  & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
+  \end{tabular}}
+  \end{isabelle}
+
+  \noindent
+  whereby threads, priorities and (critical) resources are represented
+  as natural numbers. The event @{term Set} models the situation that
+  a thread obtains a new priority given by the programmer or
+  user (for example via the {\tt nice} utility under UNIX).  As in Paulson's work, we
+  need to define functions that allow us to make some observations
+  about states.  One, called @{term threads}, calculates the set of
+  ``live'' threads that we have seen so far:
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{lcl}
+  @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & 
+    @{thm (rhs) threads.simps(1)}\\
+  @{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) threads.simps(2)[where thread="th"]}\\
+  @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) threads.simps(3)[where thread="th"]}\\
+  @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
+  \end{tabular}}
+  \end{isabelle}
+
+  \noindent
+  In this definition @{term "DUMMY # DUMMY"} stands for list-cons.
+  Another function calculates the priority for a thread @{text "th"}, which is 
+  defined as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{lcl}
+  @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
+  @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
+  @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
+  @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
+  \end{tabular}}
+  \end{isabelle}
+
+  \noindent
+  In this definition we set @{text 0} as the default priority for
+  threads that have not (yet) been created. The last function we need 
+  calculates the ``time'', or index, at which time a process had its 
+  priority last set.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{lcl}
+  @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
+  @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
+  @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
+  @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
+  \end{tabular}}
+  \end{isabelle}
+
+  \noindent
+  In this definition @{term "length s"} stands for the length of the list
+  of events @{text s}. Again the default value in this function is @{text 0}
+  for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a 
+  state @{text s} is the pair of natural numbers defined as
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm preced_def[where thread="th"]}
+  \end{isabelle}
+
+  \noindent
+  The point of precedences is to schedule threads not according to priorities (because what should
+  we do in case two threads have the same priority), but according to precedences. 
+  Precedences allow us to always discriminate between two threads with equal priority by 
+  taking into account the time when the priority was last set. We order precedences so 
+  that threads with the same priority get a higher precedence if their priority has been 
+  set earlier, since for such threads it is more urgent to finish their work. In an implementation
+  this choice would translate to a quite natural FIFO-scheduling of processes with 
+  the same priority.
+
+  Next, we introduce the concept of \emph{waiting queues}. They are
+  lists of threads associated with every resource. The first thread in
+  this list (i.e.~the head, or short @{term hd}) is chosen to be the one 
+  that is in possession of the
+  ``lock'' of the corresponding resource. We model waiting queues as
+  functions, below abbreviated as @{text wq}. They take a resource as
+  argument and return a list of threads.  This allows us to define
+  when a thread \emph{holds}, respectively \emph{waits} for, a
+  resource @{text cs} given a waiting queue function @{text wq}.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm cs_holding_def[where thread="th"]}\\
+  @{thm cs_waiting_def[where thread="th"]}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  In this definition we assume @{text "set"} converts a list into a set.
+  At the beginning, that is in the state where no thread is created yet, 
+  the waiting queue function will be the function that returns the
+  empty list for every resource.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{abbrev all_unlocked}\hfill\numbered{allunlocked}
+  \end{isabelle}
+
+  \noindent
+  Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} 
+  (RAG), which represent the dependencies between threads and resources.
+  We represent RAGs as relations using pairs of the form
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
+  @{term "(Cs cs, Th th)"}
+  \end{isabelle}
+
+  \noindent
+  where the first stands for a \emph{waiting edge} and the second for a 
+  \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a 
+  datatype for vertices). Given a waiting queue function, a RAG is defined 
+  as the union of the sets of waiting and holding edges, namely
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cs_depend_def}
+  \end{isabelle}
+
+  \noindent
+  Given four threads and three resources, an instance of a RAG can be pictured 
+  as follows:
+
+  \begin{center}
+  \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
+  \begin{tikzpicture}[scale=1]
+  %%\draw[step=2mm] (-3,2) grid (1,-1);
+
+  \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
+  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
+  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
+  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
+  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+  \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
+  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+
+  \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);
+  \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);
+  \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);
+  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);
+  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);
+  \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);
+  \end{tikzpicture}
+  \end{center}
+
+  \noindent
+  The use of relations for representing RAGs allows us to conveniently define
+  the notion of the \emph{dependants} of a thread using the transitive closure
+  operation for relations. This gives
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cs_dependents_def}
+  \end{isabelle}
+
+  \noindent
+  This definition needs to account for all threads that wait for a thread to
+  release a resource. This means we need to include threads that transitively
+  wait for a resource being released (in the picture above this means the dependants
+  of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"}, 
+  but also @{text "th\<^isub>3"}, 
+  which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
+  in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies 
+  in a RAG, then clearly
+  we have a deadlock. Therefore when a thread requests a resource,
+  we must ensure that the resulting RAG is not circular. In practice, the 
+  programmer has to ensure this.
+
+
+  Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
+  state @{text s}. It is defined as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cpreced_def2}\hfill\numbered{cpreced}
+  \end{isabelle}
+
+  \noindent
+  where the dependants of @{text th} are given by the waiting queue function.
+  While the precedence @{term prec} of a thread is determined statically 
+  (for example when the thread is
+  created), the point of the current precedence is to let the scheduler increase this
+  precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
+  given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 
+  threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
+  defined as the transitive closure of all dependent threads, we deal correctly with the 
+  problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
+  lowered prematurely.
+  
+  The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
+  by recursion on the state (a list of events); this function returns a \emph{schedule state}, which 
+  we represent as a record consisting of two
+  functions:
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
+  \end{isabelle}
+
+  \noindent
+  The first function is a waiting queue function (that is, it takes a
+  resource @{text "cs"} and returns the corresponding list of threads
+  that lock, respectively wait for, it); the second is a function that
+  takes a thread and returns its current precedence (see
+  the definition in \eqref{cpreced}). We assume the usual getter and setter methods for
+  such records.
+
+  In the initial state, the scheduler starts with all resources unlocked (the corresponding 
+  function is defined in \eqref{allunlocked}) and the
+  current precedence of every thread is initialised with @{term "Prc 0 0"}; that means 
+  \mbox{@{abbrev initial_cprec}}. Therefore
+  we have for the initial shedule state
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ 
+  \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
+  we calculate the waiting queue function of the (previous) state @{text s}; 
+  this waiting queue function @{text wq} is unchanged in the next schedule state---because
+  none of these events lock or release any resource; 
+  for calculating the next @{term "cprec_fun"}, we use @{text wq} and 
+  @{term cpreced}. This gives the following three clauses for @{term schs}:
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ 
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\smallskip\\
+  @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
+  @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ 
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent 
+  More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
+  we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
+  the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} 
+  appended to the end of that list (remember the head of this list is assigned to be in the possession of this
+  resource). This gives the clause
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ 
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function
+  so that the thread that possessed the lock is deleted from the corresponding thread list. For this 
+  list transformation, we use
+  the auxiliary function @{term release}. A simple version of @{term release} would
+  just delete this thread and return the remaining threads, namely
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}lcl}
+  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
+  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  In practice, however, often the thread with the highest precedence in the list will get the
+  lock next. We have implemented this choice, but later found out that the choice 
+  of which thread is chosen next is actually irrelevant for the correctness of PIP.
+  Therefore we prove the stronger result where @{term release} is defined as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}lcl}
+  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
+  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
+  choice for the next waiting list. It just has to be a list of distinctive threads and
+  contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
+ 
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
+  \end{tabular}
+  \end{isabelle}
+
+  Having the scheduler function @{term schs} at our disposal, we can ``lift'', or
+  overload, the notions
+  @{term waiting}, @{term holding}, @{term depend} and @{term cp} to operate on states only.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}rcl}
+  @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
+  @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\
+  @{thm (lhs) s_depend_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\
+  @{thm (lhs) cp_def}        & @{text "\<equiv>"} & @{thm (rhs) cp_def}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  With these abbreviations in place we can introduce 
+  the notion of a thread being @{term ready} in a state (i.e.~threads
+  that do not wait for any resource) and the running thread.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm readys_def}\\
+  @{thm runing_def}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  In the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
+  Note that in the initial state, that is where the list of events is empty, the set 
+  @{term threads} is empty and therefore there is neither a thread ready nor running.
+  If there is one or more threads ready, then there can only be \emph{one} thread
+  running, namely the one whose current precedence is equal to the maximum of all ready 
+  threads. We use sets to capture both possibilities.
+  We can now also conveniently define the set of resources that are locked by a thread in a
+  given state and also when a thread is detached that state (meaning the thread neither 
+  holds nor waits for a resource):
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm holdents_def}\\
+  @{thm detached_def}
+  \end{tabular}
+  \end{isabelle}
+
+  %\noindent
+  %The second definition states that @{text th}  in @{text s}.
+  
+  Finally we can define what a \emph{valid state} is in our model of PIP. For
+  example we cannot expect to be able to exit a thread, if it was not
+  created yet. 
+  These validity constraints on states are characterised by the
+  inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
+  for @{term step} relating a state and an event that can happen next.
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
+  @{thm[mode=Rule] thread_exit[where thread=th]}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The first rule states that a thread can only be created, if it is not alive yet.
+  Similarly, the second rule states that a thread can only be terminated if it was
+  running and does not lock any resources anymore (this simplifies slightly our model;
+  in practice we would expect the operating system releases all locks held by a
+  thread that is about to exit). The event @{text Set} can happen
+  if the corresponding thread is running. 
+
+  \begin{center}
+  @{thm[mode=Rule] thread_set[where thread=th]}
+  \end{center}
+
+  \noindent
+  If a thread wants to lock a resource, then the thread needs to be
+  running and also we have to make sure that the resource lock does
+  not lead to a cycle in the RAG. In practice, ensuring the latter
+  is the responsibility of the programmer.  In our formal
+  model we brush aside these problematic cases in order to be able to make
+  some meaningful statements about PIP.\footnote{This situation is
+  similar to the infamous \emph{occurs check} in Prolog: In order to say
+  anything meaningful about unification, one needs to perform an occurs
+  check. But in practice the occurs check is omitted and the
+  responsibility for avoiding problems rests with the programmer.}
+
+ 
+  \begin{center}
+  @{thm[mode=Rule] thread_P[where thread=th]}
+  \end{center}
+ 
+  \noindent
+  Similarly, if a thread wants to release a lock on a resource, then
+  it must be running and in the possession of that lock. This is
+  formally given by the last inference rule of @{term step}.
+ 
+  \begin{center}
+  @{thm[mode=Rule] thread_V[where thread=th]}
+  \end{center}
+
+  \noindent
+  A valid state of PIP can then be conveniently be defined as follows:
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Axiom] vt_nil}\hspace{1cm}
+  @{thm[mode=Rule] vt_cons}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  This completes our formal model of PIP. In the next section we present
+  properties that show our model of PIP is correct.
+*}
+
+section {* The Correctness Proof *}
+
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
+text {* 
+  Sha et al.~state their first correctness criterion for PIP in terms
+  of the number of low-priority threads \cite[Theorem 3]{Sha90}: if
+  there are @{text n} low-priority threads, then a blocked job with
+  high priority can only be blocked a maximum of @{text n} times.
+  Their second correctness criterion is given
+  in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are
+  @{text m} critical resources, then a blocked job with high priority
+  can only be blocked a maximum of @{text m} times. Both results on their own, strictly speaking, do
+  \emph{not} prevent indefinite, or unbounded, Priority Inversion,
+  because if a low-priority thread does not give up its critical
+  resource (the one the high-priority thread is waiting for), then the
+  high-priority thread can never run.  The argument of Sha et al.~is
+  that \emph{if} threads release locked resources in a finite amount
+  of time, then indefinite Priority Inversion cannot occur---the high-priority
+  thread is guaranteed to run eventually. The assumption is that
+  programmers must ensure that threads are programmed in this way.  However, even
+  taking this assumption into account, the correctness properties of
+  Sha et al.~are
+  \emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken
+  \cite{Yodaiken02} pointed out: If a low-priority thread possesses
+  locks to two resources for which two high-priority threads are
+  waiting for, then lowering the priority prematurely after giving up
+  only one lock, can cause indefinite Priority Inversion for one of the
+  high-priority threads, invalidating their two bounds.
+
+  Even when fixed, their proof idea does not seem to go through for
+  us, because of the way we have set up our formal model of PIP.  One
+  reason is that we allow critical sections, which start with a @{text P}-event
+  and finish with a corresponding @{text V}-event, to arbitrarily overlap
+  (something Sha et al.~explicitly exclude).  Therefore we have
+  designed a different correctness criterion for PIP. The idea behind
+  our criterion is as follows: for all states @{text s}, we know the
+  corresponding thread @{text th} with the highest precedence; we show
+  that in every future state (denoted by @{text "s' @ s"}) in which
+  @{text th} is still alive, either @{text th} is running or it is
+  blocked by a thread that was alive in the state @{text s} and was waiting 
+  for or in the possession of a lock in @{text s}. Since in @{text s}, as in
+  every state, the set of alive threads is finite, @{text th} can only
+  be blocked a finite number of times. This is independent of how many
+  threads of lower priority are created in @{text "s'"}. We will actually prove a
+  stronger statement where we also provide the current precedence of
+  the blocking thread. However, this correctness criterion hinges upon
+  a number of assumptions about the states @{text s} and @{text "s' @
+  s"}, the thread @{text th} and the events happening in @{text
+  s'}. We list them next:
+
+  \begin{quote}
+  {\bf Assumptions on the states {\boldmath@{text s}} and 
+  {\boldmath@{text "s' @ s"}:}} We need to require that @{text "s"} and 
+  @{text "s' @ s"} are valid states:
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{l}
+  @{term "vt s"}, @{term "vt (s' @ s)"} 
+  \end{tabular}
+  \end{isabelle}
+  \end{quote}
+
+  \begin{quote}
+  {\bf Assumptions on the thread {\boldmath@{text "th"}:}} 
+  The thread @{text th} must be alive in @{text s} and 
+  has the highest precedence of all alive threads in @{text s}. Furthermore the
+  priority of @{text th} is @{text prio} (we need this in the next assumptions).
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{l}
+  @{term "th \<in> threads s"}\\
+  @{term "prec th s = Max (cprec s ` threads s)"}\\
+  @{term "prec th s = (prio, DUMMY)"}
+  \end{tabular}
+  \end{isabelle}
+  \end{quote}
+  
+  \begin{quote}
+  {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot
+  be blocked indefinitely. Of course this can happen if threads with higher priority
+  than @{text th} are continuously created in @{text s'}. Therefore we have to assume that  
+  events in @{text s'} can only create (respectively set) threads with equal or lower 
+  priority than @{text prio} of @{text th}. We also need to assume that the
+  priority of @{text "th"} does not get reset and also that @{text th} does
+  not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. 
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{l}
+  {If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
+  {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
+  {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
+  \end{tabular}
+  \end{isabelle}
+  \end{quote}
+
+  \noindent
+  The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}.
+  Under these assumptions we shall prove the following correctness property:
+
+  \begin{theorem}\label{mainthm}
+  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+  the thread @{text th} and the events in @{text "s'"},
+  if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
+  @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and 
+  @{term "cp (s' @ s) th' = prec th s"}.
+  \end{theorem}
+
+  \noindent
+  This theorem ensures that the thread @{text th}, which has the
+  highest precedence in the state @{text s}, can only be blocked in
+  the state @{text "s' @ s"} by a thread @{text th'} that already
+  existed in @{text s} and requested or had a lock on at least 
+  one resource---that means the thread was not \emph{detached} in @{text s}. 
+  As we shall see shortly, that means there are only finitely 
+  many threads that can block @{text th} in this way and then they 
+  need to run with the same current precedence as @{text th}.
+
+  Like in the argument by Sha et al.~our
+  finite bound does not guarantee absence of indefinite Priority
+  Inversion. For this we further have to assume that every thread
+  gives up its resources after a finite amount of time. We found that
+  this assumption is awkward to formalise in our model. Therefore we
+  leave it out and let the programmer assume the responsibility to
+  program threads in such a benign manner (in addition to causing no 
+  circularity in the @{text RAG}). In this detail, we do not
+  make any progress in comparison with the work by Sha et al.
+  However, we are able to combine their two separate bounds into a
+  single theorem improving their bound.
+
+  In what follows we will describe properties of PIP that allow us to prove 
+  Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 
+  It is relatively easy to see that
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
+  @{thm[mode=IfThen]  finite_threads}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The second property is by induction of @{term vt}. The next three
+  properties are 
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
+  @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
+  @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The first property states that every waiting thread can only wait for a single
+  resource (because it gets suspended after requesting that resource); the second 
+  that every resource can only be held by a single thread; 
+  the third property establishes that in every given valid state, there is
+  at most one running thread. We can also show the following properties 
+  about the @{term RAG} in @{text "s"}.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\
+  \hspace{5mm}@{thm (concl) acyclic_depend},
+  @{thm (concl) finite_depend} and
+  @{thm (concl) wf_dep_converse},\\
+  \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}
+  and\\
+  \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The acyclicity property follows from how we restricted the events in
+  @{text step}; similarly the finiteness and well-foundedness property.
+  The last two properties establish that every thread in a @{text "RAG"}
+  (either holding or waiting for a resource) is a live thread.
+
+  The key lemma in our proof of Theorem~\ref{mainthm} is as follows:
+
+  \begin{lemma}\label{mainlem}
+  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+  the thread @{text th} and the events in @{text "s'"},
+  if @{term "th' \<in> threads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
+  then @{text "th' \<notin> running (s' @ s)"}.
+  \end{lemma}
+
+  \noindent
+  The point of this lemma is that a thread different from @{text th} (which has the highest
+  precedence in @{text s}) and not holding any resource, cannot be running 
+  in the state @{text "s' @ s"}.
+
+  \begin{proof}
+  Since thread @{text "th'"} does not hold any resource, no thread can depend on it. 
+  Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence
+  @{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the 
+  state @{text "(s' @ s)"} and precedences are distinct among threads, we have
+  @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this 
+  we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
+  Since @{text "prec th (s' @ s)"} is already the highest 
+  @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by 
+  definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
+  Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
+  By defintion of @{text "running"}, @{text "th'"} can not be running in state
+  @{text "s' @ s"}, as we had to show.\qed
+  \end{proof}
+
+  \noindent
+  Since @{text "th'"} is not able to run in state @{text "s' @ s"}, it is not able to 
+  issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
+  one step further, @{text "th'"} still cannot hold any resource. The situation will 
+  not change in further extensions as long as @{text "th"} holds the highest precedence.
+
+  From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be 
+  blocked by a thread @{text th'} that
+  held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
+  that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the 
+  precedence of @{text th} in @{text "s"}.
+  We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
+  This theorem gives a stricter bound on the threads that can block @{text th} than the
+  one obtained by Sha et al.~\cite{Sha90}:
+  only threads that were alive in state @{text s} and moreover held a resource.
+  This means our bound is in terms of both---alive threads in state @{text s}
+  and number of critical resources. Finally, the theorem establishes that the blocking threads have the
+  current precedence raised to the precedence of @{text th}.
+
+  We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"}
+  by showing that @{text "running (s' @ s)"} is not empty.
+
+  \begin{lemma}
+  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+  the thread @{text th} and the events in @{text "s'"},
+  @{term "running (s' @ s) \<noteq> {}"}.
+  \end{lemma}
+
+  \begin{proof}
+  If @{text th} is blocked, then by following its dependants graph, we can always 
+  reach a ready thread @{text th'}, and that thread must have inherited the 
+  precedence of @{text th}.\qed
+  \end{proof}
+
+
+  %The following lemmas show how every node in RAG can be chased to ready threads:
+  %\begin{enumerate}
+  %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
+  %  @   {thm [display] chain_building[rule_format]}
+  %\item The ready thread chased to is unique (@{text "dchain_unique"}):
+  %  @   {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+  %\end{enumerate}
+
+  %Some deeper results about the system:
+  %\begin{enumerate}
+  %\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
+  %@  {thm [display] max_cp_eq}
+  %\item There must be one ready thread having the max @{term "cp"}-value 
+  %(@{text "max_cp_readys_threads"}):
+  %@  {thm [display] max_cp_readys_threads}
+  %\end{enumerate}
+
+  %The relationship between the count of @{text "P"} and @{text "V"} and the number of 
+  %critical resources held by a thread is given as follows:
+  %\begin{enumerate}
+  %\item The @{term "V"}-operation decreases the number of critical resources 
+  %  one thread holds (@{text "cntCS_v_dec"})
+  %   @  {thm [display]  cntCS_v_dec}
+  %\item The number of @{text "V"} never exceeds the number of @{text "P"} 
+  %  (@  {text "cnp_cnv_cncs"}):
+  %  @  {thm [display]  cnp_cnv_cncs}
+  %\item The number of @{text "V"} equals the number of @{text "P"} when 
+  %  the relevant thread is not living:
+  %  (@{text "cnp_cnv_eq"}):
+  %  @  {thm [display]  cnp_cnv_eq}
+  %\item When a thread is not living, it does not hold any critical resource 
+  %  (@{text "not_thread_holdents"}):
+  %  @  {thm [display] not_thread_holdents}
+  %\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 
+  %  thread does not hold any critical resource, therefore no thread can depend on it
+  %  (@{text "count_eq_dependents"}):
+  %  @  {thm [display] count_eq_dependents}
+  %\end{enumerate}
+
+  %The reason that only threads which already held some resoures
+  %can be runing and block @{text "th"} is that if , otherwise, one thread 
+  %does not hold any resource, it may never have its prioirty raised
+  %and will not get a chance to run. This fact is supported by 
+  %lemma @{text "moment_blocked"}:
+  %@   {thm [display] moment_blocked}
+  %When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
+  %resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 
+  %any thread which is running after @{text "th"} became the highest must have already held
+  %some resource at state @{text "s"}.
+
+
+  %When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 
+  %if a thread releases all its resources at some moment in @{text "t"}, after that, 
+  %it may never get a change to run. If every thread releases its resource in finite duration,
+  %then after a while, only thread @{text "th"} is left running. This shows how indefinite 
+  %priority inversion can be avoided. 
+
+  %All these assumptions are put into a predicate @{term "extend_highest_gen"}. 
+  %It can be proved that @{term "extend_highest_gen"} holds 
+  %for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
+  %@   {thm [display] red_moment}
+  
+  %From this, an induction principle can be derived for @{text "t"}, so that 
+  %properties already derived for @{term "t"} can be applied to any prefix 
+  %of @{text "t"} in the proof of new properties 
+  %about @{term "t"} (@{text "ind"}):
+  %\begin{center}
+  %@   {thm[display] ind}
+  %\end{center}
+
+  %The following properties can be proved about @{term "th"} in @{term "t"}:
+  %\begin{enumerate}
+  %\item In @{term "t"}, thread @{term "th"} is kept live and its 
+  %  precedence is preserved as well
+  %  (@{text "th_kept"}): 
+  %  @   {thm [display] th_kept}
+  %\item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among 
+  %  all living threads
+  %  (@{text "max_preced"}): 
+  %  @   {thm [display] max_preced}
+  %\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
+  %  among all living threads
+  %  (@{text "th_cp_max_preced"}): 
+  %  @   {thm [display] th_cp_max_preced}
+  %\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current 
+  %  precedence among all living threads
+  %  (@{text "th_cp_max"}): 
+  %  @   {thm [display] th_cp_max}
+  %\item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment 
+  %  @{term "s"}
+  %  (@{text "th_cp_preced"}): 
+  %  @   {thm [display] th_cp_preced}
+  %\end{enumerate}
+
+  %The main theorem of this part is to characterizing the running thread during @{term "t"} 
+  %(@{text "runing_inversion_2"}):
+  %@   {thm [display] runing_inversion_2}
+  %According to this, if a thread is running, it is either @{term "th"} or was
+  %already live and held some resource 
+  %at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
+
+  %Since there are only finite many threads live and holding some resource at any moment,
+  %if every such thread can release all its resources in finite duration, then after finite
+  %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
+  %then.
+  *}
+(*<*)
+end
+(*>*)
+
+section {* Properties for an Implementation\label{implement} *}
+
+text {*
+  While our formalised proof gives us confidence about the correctness of our model of PIP, 
+  we found that the formalisation can even help us with efficiently implementing it.
+
+  For example Baker complained that calculating the current precedence
+  in PIP is quite ``heavy weight'' in Linux (see the Introduction).
+  In our model of PIP the current precedence of a thread in a state @{text s}
+  depends on all its dependants---a ``global'' transitive notion,
+  which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
+  We can however improve upon this. For this let us define the notion
+  of @{term children} of a thread @{text th} in a state @{text s} as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm children_def2}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  where a child is a thread that is only one ``hop'' away from the thread
+  @{text th} in the @{term RAG} (and waiting for @{text th} to release
+  a resource). We can prove the following lemma.
+
+  \begin{lemma}\label{childrenlem}
+  @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
+  \begin{center}
+  @{thm (concl) cp_rec}.
+  \end{center}
+  \end{lemma}
+  
+  \noindent
+  That means the current precedence of a thread @{text th} can be
+  computed locally by considering only the children of @{text th}. In
+  effect, it only needs to be recomputed for @{text th} when one of
+  its children changes its current precedence.  Once the current 
+  precedence is computed in this more efficient manner, the selection
+  of the thread with highest precedence from a set of ready threads is
+  a standard scheduling operation implemented in most operating
+  systems.
+
+  Of course the main work for implementing PIP involves the
+  scheduler and coding how it should react to events.  Below we
+  outline how our formalisation guides this implementation for each
+  kind of events.\smallskip
+*}
+
+(*<*)
+context step_create_cps
+begin
+(*>*)
+text {*
+  \noindent
+  \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and 
+  the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
+  is allowed to occur). In this situation we can show that
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm eq_dep},\\
+  @{thm eq_cp_th}, and\\
+  @{thm[mode=IfThen] eq_cp}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  This means in an implementation we do not have recalculate the @{text RAG} and also none of the
+  current precedences of the other threads. The current precedence of the created
+  thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
+  \smallskip
+  *}
+(*<*)
+end
+context step_exit_cps
+begin
+(*>*)
+text {*
+  \noindent
+  \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 
+  the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm eq_dep}, and\\
+  @{thm[mode=IfThen] eq_cp}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  This means again we do not have to recalculate the @{text RAG} and
+  also not the current precedences for the other threads. Since @{term th} is not
+  alive anymore in state @{term "s"}, there is no need to calculate its
+  current precedence.
+  \smallskip
+*}
+(*<*)
+end
+context step_set_cps
+begin
+(*>*)
+text {*
+  \noindent
+  \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and 
+  @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm[mode=IfThen] eq_dep}, and\\
+  @{thm[mode=IfThen] eq_cp_pre}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The first property is again telling us we do not need to change the @{text RAG}. 
+  The second shows that the @{term cp}-values of all threads other than @{text th} 
+  are unchanged. The reason is that @{text th} is running; therefore it is not in 
+  the @{term dependants} relation of any other thread. This in turn means that the 
+  change of its priority cannot affect other threads.
+
+  %The second
+  %however states that only threads that are \emph{not} dependants of @{text th} have their
+  %current precedence unchanged. For the others we have to recalculate the current
+  %precedence. To do this we can start from @{term "th"} 
+  %and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
+  %the @{term "cp"} of every 
+  %thread encountered on the way. Since the @{term "depend"}
+  %is assumed to be loop free, this procedure will always stop. The following two lemmas show, however, 
+  %that this procedure can actually stop often earlier without having to consider all
+  %dependants.
+  %
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %\begin{tabular}{@ {}l}
+  %@{thm[mode=IfThen] eq_up_self}\\
+  %@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+  %@{text "then"} @{thm (concl) eq_up}.
+  %\end{tabular}
+  %\end{isabelle}
+  %
+  %\noindent
+  %The first lemma states that if the current precedence of @{text th} is unchanged,
+  %then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
+  %The second states that if an intermediate @{term cp}-value does not change, then
+  %the procedure can also stop, because none of its dependent threads will
+  %have their current precedence changed.
+  \smallskip
+  *}
+(*<*)
+end
+context step_v_cps_nt
+begin
+(*>*)
+text {*
+  \noindent
+  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and 
+  @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
+  subcases: one where there is a thread to ``take over'' the released
+  resource @{text cs}, and one where there is not. Let us consider them
+  in turn. Suppose in state @{text s}, the thread @{text th'} takes over
+  resource @{text cs} from thread @{text th}. We can prove
+
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm depend_s}
+  \end{isabelle}
+  
+  \noindent
+  which shows how the @{text RAG} needs to be changed. The next lemma suggests
+  how the current precedences need to be recalculated. For threads that are
+  not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
+  can show
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm[mode=IfThen] cp_kept}
+  \end{isabelle}
+  
+  \noindent
+  For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
+  recalculate their current precedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
+  \noindent
+  In the other case where there is no thread that takes over @{text cs}, we can show how
+  to recalculate the @{text RAG} and also show that no current precedence needs
+  to be recalculated.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm depend_s}\\
+  @{thm eq_cp}
+  \end{tabular}
+  \end{isabelle}
+  *}
+(*<*)
+end
+context step_P_cps_e
+begin
+(*>*)
+text {*
+  \noindent
+  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and 
+  @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
+  the one where @{text cs} is not locked, and one where it is. We treat the former case
+  first by showing that
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm depend_s}\\
+  @{thm eq_cp}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  This means we need to add a holding edge to the @{text RAG} and no
+  current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
+  \noindent
+  In the second case we know that resource @{text cs} is locked. We can show that
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm depend_s}\\
+  @{thm[mode=IfThen] eq_cp}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  That means we have to add a waiting edge to the @{text RAG}. Furthermore
+  the current precedence for all threads that are not dependants of @{text th}
+  are unchanged. For the others we need to follow the edges 
+  in the @{text RAG} and recompute the @{term "cp"}. To do this we can start from @{term "th"} 
+  and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
+  the @{term "cp"} of every 
+  thread encountered on the way. Since the @{term "depend"}
+  is loop free, this procedure will always stop. The following lemma shows, however, 
+  that this procedure can actually stop often earlier without having to consider all
+  dependants.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  %%@ {t hm[mode=IfThen] eq_up_self}\\
+  @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+  @{text "then"} @{thm (concl) eq_up}.
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  This lemma states that if an intermediate @{term cp}-value does not change, then
+  the procedure can also stop, because none of its dependent threads will
+  have their current precedence changed.
+  *}
+(*<*)
+end
+(*>*)
+text {*
+  \noindent
+  As can be seen, a pleasing byproduct of our formalisation is that the properties in
+  this section closely inform an implementation of PIP, namely whether the
+  @{text RAG} needs to be reconfigured or current precedences need to
+  be recalculated for an event. This information is provided by the lemmas we proved.
+  We confirmed that our observations translate into practice by implementing
+  our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 
+  Stanford University \cite{PINTOS}. To implement PIP, we only need to modify the kernel 
+  functions corresponding to the events in our formal model. The events translate to the following 
+  function interface in PINTOS:
+
+  \begin{center}
+  \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
+  \hline
+  {\bf Event} & {\bf PINTOS function} \\
+  \hline
+  @{text Create} & @{text "thread_create"}\\
+  @{text Exit}   & @{text "thread_exit"}\\
+  @{text Set}    & @{text "thread_set_priority"}\\
+  @{text P}      & @{text "lock_acquire"}\\
+  @{text V}      & @{text "lock_release"}\\ 
+  \hline
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  Our implicit assumption that every event is an atomic operation is ensured by the architecture of 
+  PINTOS. The case where an unlocked resource is given next to the waiting thread with the
+  highest precedence is realised in our implementation by priority queues. We implemented
+  them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations
+  for accessing and updating. Apart from having to implement relatively complex data\-structures in C
+  using pointers, our experience with the implementation has been very positive: our specification 
+  and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. 
+*}
+
+section {* Conclusion *}
+
+text {* 
+  The Priority Inheritance Protocol (PIP) is a classic textbook
+  algorithm used in many real-time operating systems in order to avoid the problem of
+  Priority Inversion.  Although classic and widely used, PIP does have
+  its faults: for example it does not prevent deadlocks in cases where threads
+  have circular lock dependencies.
+
+  We had two goals in mind with our formalisation of PIP: One is to
+  make the notions in the correctness proof by Sha et al.~\cite{Sha90}
+  precise so that they can be processed by a theorem prover. The reason is
+  that a mechanically checked proof avoids the flaws that crept into their
+  informal reasoning. We achieved this goal: The correctness of PIP now
+  only hinges on the assumptions behind our formal model. The reasoning, which is
+  sometimes quite intricate and tedious, has been checked by Isabelle/HOL. 
+  We can also confirm that Paulson's
+  inductive method for protocol verification~\cite{Paulson98} is quite
+  suitable for our formal model and proof. The traditional application
+  area of this method is security protocols. 
+
+  The second goal of our formalisation is to provide a specification for actually
+  implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
+  explain how to use various implementations of PIP and abstractly
+  discuss their properties, but surprisingly lack most details important for a
+  programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).  
+  That this is an issue in practice is illustrated by the
+  email from Baker we cited in the Introduction. We achieved also this
+  goal: The formalisation allowed us to efficently implement our version
+  of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86 
+  architecture. It also gives the first author enough data to enable
+  his undergraduate students to implement PIP (as part of their OS course).
+  A byproduct of our formalisation effort is that nearly all
+  design choices for the PIP scheduler are backed up with a proved
+  lemma. We were also able to establish the property that the choice of
+  the next thread which takes over a lock is irrelevant for the correctness
+  of PIP. 
+
+  PIP is a scheduling algorithm for single-processor systems. We are
+  now living in a multi-processor world. Priority Inversion certainly
+  occurs also there.  However, there is very little ``foundational''
+  work about PIP-algorithms on multi-processor systems.  We are not
+  aware of any correctness proofs, not even informal ones. There is an
+  implementation of a PIP-algorithm for multi-processors as part of the
+  ``real-time'' effort in Linux, including an informal description of the implemented scheduling
+  algorithm given in \cite{LINUX}.  We estimate that the formal
+  verification of this algorithm, involving more fine-grained events,
+  is a magnitude harder than the one we presented here, but still
+  within reach of current theorem proving technology. We leave this
+  for future work.
+
+  The most closely related work to ours is the formal verification in
+  PVS of the Priority Ceiling Protocol done by Dutertre
+  \cite{dutertre99b}---another solution to the Priority Inversion
+  problem, which however needs static analysis of programs in order to
+  avoid it. There have been earlier formal investigations
+  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
+  checking techniques. The results obtained by them apply,
+  however, only to systems with a fixed size, such as a fixed number of 
+  events and threads. In contrast, our result applies to systems of arbitrary
+  size. Moreover, our result is a good 
+  witness for one of the major reasons to be interested in machine checked 
+  reasoning: gaining deeper understanding of the subject matter.
+
+  Our formalisation
+  consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
+  code with a few apply-scripts interspersed. The formal model of PIP
+  is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
+  definitions and proofs span over 770 lines of code. The properties relevant
+  for an implementation require 2000 lines. 
+  %The code of our formalisation 
+  %can be downloaded from
+  %\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.\medskip
+
+  \noindent
+  {\bf Acknowledgements:}
+  We are grateful for the comments we received from anonymous
+  referees.
+
+  \bibliographystyle{plain}
+  \bibliography{root}
+*}
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r c4783e4ef43f -r a04084de4946 Paper/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/ROOT.ML	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,1 @@
+use_thy "Paper";
\ No newline at end of file
diff -r c4783e4ef43f -r a04084de4946 Paper/document/llncs.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/llncs.cls	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2002/01/28 v2.13
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+  \ifnum #1>\c@tocdepth \else
+    \vskip \z@ \@plus.2\p@
+    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+               \parfillskip -\rightskip \pretolerance=10000
+     \parindent #2\relax\@afterindenttrue
+     \interlinepenalty\@M
+     \leavevmode
+     \@tempdima #3\relax
+     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+     {#4}\nobreak
+     \leaders\hbox{$\m@th
+        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+        mu$}\hfill
+     \nobreak
+     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+     \par}%
+  \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Key words:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+   \@setfontsize\small\@ixpt{11}%
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 8\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin   {63\p@}
+\setlength\evensidemargin  {63\p@}
+\setlength\marginparwidth  {90\p@}
+
+\setlength\headsep   {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter      {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+            \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+       \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+      \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+                 \thispagestyle{empty}%
+                 \if@twocolumn
+                     \onecolumn
+                     \@tempswatrue
+                   \else
+                     \@tempswafalse
+                 \fi
+                 \null\vfil
+                 \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+    \ifnum \c@secnumdepth >-2\relax
+      \refstepcounter{part}%
+      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+    \else
+      \addcontentsline{toc}{part}{#1}%
+    \fi
+    \markboth{}{}%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \ifnum \c@secnumdepth >-2\relax
+       \huge\bfseries \partname~\thepart
+       \par
+       \vskip 20\p@
+     \fi
+     \Huge \bfseries #2\par}%
+    \@endpart}
+\def\@spart#1{%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \Huge \bfseries #1\par}%
+    \@endpart}
+\def\@endpart{\vfil\newpage
+              \if@twoside
+                \null
+                \thispagestyle{empty}%
+                \newpage
+              \fi
+              \if@tempswa
+                \twocolumn
+              \fi}
+
+\newcommand\chapter{\clearpage
+                    \thispagestyle{empty}%
+                    \global\@topnum\z@
+                    \@afterindentfalse
+                    \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+                       \if@mainmatter
+                         \refstepcounter{chapter}%
+                         \typeout{\@chapapp\space\thechapter.}%
+                         \addcontentsline{toc}{chapter}%
+                                  {\protect\numberline{\thechapter}#1}%
+                       \else
+                         \addcontentsline{toc}{chapter}{#1}%
+                       \fi
+                    \else
+                      \addcontentsline{toc}{chapter}{#1}%
+                    \fi
+                    \chaptermark{#1}%
+                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
+                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
+                    \if@twocolumn
+                      \@topnewpage[\@makechapterhead{#2}]%
+                    \else
+                      \@makechapterhead{#2}%
+                      \@afterheading
+                    \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \ifnum \c@secnumdepth >\m@ne
+      \if@mainmatter
+        \large\bfseries \@chapapp{} \thechapter
+        \par\nobreak
+        \vskip 20\p@
+      \fi
+    \fi
+    \interlinepenalty\@M
+    \Large \bfseries #1\par\nobreak
+    \vskip 40\p@
+  }}
+\def\@schapter#1{\if@twocolumn
+                   \@topnewpage[\@makeschapterhead{#1}]%
+                 \else
+                   \@makeschapterhead{#1}%
+                   \@afterheading
+                 \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \normalfont
+    \interlinepenalty\@M
+    \Large \bfseries  #1\par\nobreak
+    \vskip 40\p@
+  }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\large\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\normalsize\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+                  \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini  {17\p@}
+\setlength\leftmargin    {\leftmargini}
+\setlength\leftmarginii  {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv  {\leftmargini}
+\setlength  \labelsep  {.5em}
+\setlength  \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+            \parsep 0\p@ \@plus1\p@ \@minus\p@
+            \topsep 8\p@ \@plus2\p@ \@minus4\p@
+            \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus\p@\@minus\p@
+              \parsep    \z@
+              \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+                                                    {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{auco}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+   \addvspace{2em plus\p@}%  % space above part line
+   \begingroup
+     \parindent \z@
+     \rightskip \z@ plus 5em
+     \hrule\vskip5pt
+     \large               % same size as for a contribution heading
+     \bfseries\boldmath   % set line in boldface
+     \leavevmode          % TeX command to enter horizontal mode.
+     #1\par
+     \vskip5pt
+     \hrule
+     \vskip1pt
+     \nobreak             % Never break after part entry
+   \endgroup}
+
+\def\@dotsep{2}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+                     {\thechapter}#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmarkwop}%
+  \fi\@gtempa{toc}{chapter}}
+\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+      \nobreak
+      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+      \@dotsep mu$}\hfill
+      \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=\z@ %15\p@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+%\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@            % no chapter numbers
+\tocsecnum=15\p@          % section 88. plus 2.222pt
+\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+    \section*{\listfigurename
+      \@mkboth{\listfigurename}{\listfigurename}}%
+    \@starttoc{lof}%
+    }
+
+\renewcommand\listoftables{%
+    \section*{\listtablename
+      \@mkboth{\listtablename}{\listtablename}}%
+    \@starttoc{lot}%
+    }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \def\@biblabel##1{##1.}
+      \small
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+     {\let\protect\noexpand\immediate
+     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+    {\@ifundefined
+       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+        ?}\@warning
+       {Citation `\@citeb' on page \thepage \space undefined}}%
+    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+     \else
+      \advance\@tempcntb\@ne
+      \ifnum\@tempcntb=\@tempcntc
+      \else\advance\@tempcntb\m@ne\@citeo
+      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+               \@citea\def\@citea{,\,\hskip\z@skip}%
+               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+                \def\@citea{--}\fi
+      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \small
+      \list{}%
+           {\settowidth\labelwidth{}%
+            \leftmargin\parindent
+            \itemindent=-\parindent
+            \labelsep=\z@
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+      \def\@cite#1{#1}%
+      \def\@lbibitem[#1]#2{\item[]\if@filesw
+        {\def\protect##1{\string ##1\space}\immediate
+      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+   \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+                \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+                \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+               {\@mkboth{\indexname}{\indexname}%
+                \thispagestyle{empty}\parindent\z@
+                \parskip\z@ \@plus .3\p@\relax
+                \let\item\par
+                \def\,{\relax\ifmmode\mskip\thinmuskip
+                             \else\hskip0.2em\ignorespaces\fi}%
+                \normalfont\small
+                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+                }
+                {\end{multicols}}
+
+\renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width 2truecm
+  \kern2.6\p@}
+  \newdimen\fnindent
+  \fnindent1em
+\long\def\@makefntext#1{%
+    \parindent \fnindent%
+    \leftskip \fnindent%
+    \noindent
+    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+  \vskip\abovecaptionskip
+  \sbox\@tempboxa{{\bfseries #1.} #2}%
+  \ifdim \wd\@tempboxa >\hsize
+    {\bfseries #1.} #2\par
+  \else
+    \global \@minipagefalse
+    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+  \fi
+  \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+        \reset@font
+        \small
+        \@setnobreak
+        \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@float{table}}
+               {\end@float}
+\renewenvironment{table*}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@dblfloat{table}}
+               {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+                   \gdef\@title{No Title Given}%
+                   \gdef\@subtitle{}%
+                   \gdef\@institute{No Institute Given}%
+                   \gdef\@thanks{}%
+                   \global\titlerunning={}\global\authorrunning={}%
+                   \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+   \gdef\fnnstart{0}%
+ \else
+   \xdef\fnnstart{\c@@inst}%
+   \setcounter{@inst}{1}%
+   \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+   {\star\star\star}\or \dagger\or \ddagger\or
+   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+   \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+  \refstepcounter{chapter}%
+  \stepcounter{section}%
+  \setcounter{section}{0}%
+  \setcounter{subsection}{0}%
+  \setcounter{figure}{0}
+  \setcounter{table}{0}
+  \setcounter{equation}{0}
+  \setcounter{footnote}{0}%
+  \begingroup
+    \parindent=\z@
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \if@twocolumn
+      \ifnum \col@number=\@ne
+        \@maketitle
+      \else
+        \twocolumn[\@maketitle]%
+      \fi
+    \else
+      \newpage
+      \global\@topnum\z@   % Prevents figures from going at top of page.
+      \@maketitle
+    \fi
+    \thispagestyle{empty}\@thanks
+%
+    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+    \instindent=\hsize
+    \advance\instindent by-\headlineindent
+%    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+%       \addcontentsline{toc}{title}{\the\toctitle}\fi
+    \if@runhead
+       \if!\the\titlerunning!\else
+         \edef\@title{\the\titlerunning}%
+       \fi
+       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+       \ifdim\wd\titrun>\instindent
+          \typeout{Title too long for running head. Please supply}%
+          \typeout{a shorter form with \string\titlerunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\titrun=\hbox{\small\rm
+          Title Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@title{\copy\titrun}%
+    \fi
+%
+    \if!\the\tocauthor!\relax
+      {\def\and{\noexpand\protect\noexpand\and}%
+      \protected@xdef\toc@uthor{\@author}}%
+    \else
+      \def\\{\noexpand\protect\noexpand\newline}%
+      \protected@xdef\scratch{\the\tocauthor}%
+      \protected@xdef\toc@uthor{\scratch}%
+    \fi
+%    \addcontentsline{toc}{author}{\toc@uthor}%
+    \if@runhead
+       \if!\the\authorrunning!
+         \value{@inst}=\value{@auth}%
+         \setcounter{@auth}{1}%
+       \else
+         \edef\@author{\the\authorrunning}%
+       \fi
+       \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+       \ifdim\wd\authrun>\instindent
+          \typeout{Names of authors too long for running head. Please supply}%
+          \typeout{a shorter form with \string\authorrunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\authrun=\hbox{\small\rm
+          Authors Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@author{\copy\authrun}%
+       \markboth{\@author}{\@title}%
+     \fi
+  \endgroup
+  \setcounter{footnote}{\fnnstart}%
+  \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{@inst}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+  \pretolerance=10000
+  \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+  \vskip -.65cm
+  \pretolerance=10000
+  \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}\@addtoreset{#1}{#3}%
+   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+                              \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}%
+   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+                               \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+  {\expandafter\@ifdefinable\csname #1\endcsname
+  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+                    \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+    \expandafter\xdef\csname #1name\endcsname{#2}%
+    \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+       {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+   \def\@thmcountersep{.}
+   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+   \if@envcntreset
+      \@addtoreset{theorem}{section}
+   \else
+      \@addtoreset{theorem}{chapter}
+   \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+   \if@envcntsect % mit section numeriert
+      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+   \else % nicht mit section numeriert
+      \if@envcntreset
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{section}}
+      \else
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{chapter}}%
+      \fi
+   \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+    \def\@tempa{#1}%
+    \let\@tempd\@elt
+    \def\@elt##1{%
+        \def\@tempb{##1}%
+        \ifx\@tempa\@tempb\else
+            \@addtoreset{##1}{#2}%
+        \fi}%
+    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+    \expandafter\def\csname cl@#2\endcsname{}%
+    \@tempc
+    \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+      }
+
+\renewenvironment{abstract}{%
+      \list{}{\advance\topsep by0.35cm\relax\small
+      \leftmargin=1cm
+      \labelwidth=\z@
+      \listparindent=\z@
+      \itemindent\listparindent
+      \rightmargin\leftmargin}\item[\hskip\labelsep
+                                    \bfseries\abstractname]}
+    {\endlist}
+
+\newdimen\headlineindent             % dimension for space between
+\headlineindent=1.166cm              % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \leftmark\hfil}
+   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \hfil}
+   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls
diff -r c4783e4ef43f -r a04084de4946 Paper/document/mathpartir.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/mathpartir.sty	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,446 @@
+%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+%  Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
+%
+%  Author         : Didier Remy 
+%  Version        : 1.2.0
+%  Bug Reports    : to author
+%  Web Site       : http://pauillac.inria.fr/~remy/latex/
+% 
+%  Mathpartir 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}
+    [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+%% \newdimen \mpr@tmpdim
+%% Dimens are a precious ressource. Uses seems to be local.
+\let \mpr@tmpdim \@tempdima
+
+% 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}
+
+\newenvironment{mathparpagebreakable}[1][]
+  {\begingroup 
+   \par
+   \mpr@savepar \parskip 0em \hsize \linewidth \centering
+      \mpr@prebindings \mpr@paroptions #1%
+      \vskip \abovedisplayskip \vskip -\lineskip%
+     \ifmmode  \else  $\displaystyle\fi
+     \MathparBindings
+  }
+  {\unskip
+   \ifmmode $\fi \par\endgroup
+   \vskip \belowdisplayskip
+   \noindent
+  \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
+}
+
+\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}
+
+%% Part III -- Type inference rules
+
+\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@item #1{$\displaystyle #1$}
+\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 T 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{\mpr@item {##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
+  }{}
+
+%% The default
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\mpr@over #2}$}}
+\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\@@atop #2}$}}
+
+\let \mpr@fraction \mpr@@fraction
+
+%% A generic solution to arrow
+
+\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
+     \def \mpr@tail{#1}%
+     \def \mpr@body{#2}%
+     \def \mpr@head{#3}%
+     \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
+     \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
+     \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
+     \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
+     \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
+     \setbox0=\hbox {$\box1 \@@atop \box2$}%
+     \dimen0=\wd0\box0
+     \box0 \hskip -\dimen0\relax
+     \hbox to \dimen0 {$%
+       \mathrel{\mpr@tail}\joinrel
+       \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
+     $}}}
+
+%% Old stuff should be removed in next version
+\def \mpr@@nothing #1#2
+    {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
+\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
+     \let \mpr@over \@@over
+     \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. 
+%  
+
+%% Keys that make sence in all kinds of rules
+\def \mprset #1{\setkeys{mprset}{#1}}
+\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
+\define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
+\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mprset}{sep}{\def\mpr@sep{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\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}}
+
+\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}
+  \@tempdima \dp0 \advance \@tempdima by -\dp1
+  \raise \@tempdima \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 \TirNameStyle #1{\small \textsc{#1}}
+\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
+\let \TirName \tir@name
+\let \DefTirName \TirName
+\let \RefTirName \TirName
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
diff -r c4783e4ef43f -r a04084de4946 Paper/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.bib	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,205 @@
+
+@Book{Paulson96,
+  author = 	 {L.~C.~Paulson},
+  title = 	 {{ML} for the {W}orking {P}rogrammer},
+  publisher = 	 {Cambridge University Press},
+  year = 	 {1996}
+}
+
+
+@Manual{LINUX,
+  author =       {S.~Rostedt},
+  title =        {{RT}-{M}utex {I}mplementation {D}esign},
+  note =         {Linux Kernel Distribution at, 
+                  www.kernel.org/doc/Documentation/rt-mutex-design.txt}
+}
+
+@Misc{PINTOS,
+  author = {B.~Pfaff},
+  title = {{PINTOS}}, 
+  note = {\url{http://www.stanford.edu/class/cs140/projects/}},
+}
+
+
+@inproceedings{Haftmann08,
+  author    = {F.~Haftmann and M.~Wenzel},
+  title     = {{L}ocal {T}heory {S}pecifications in {I}sabelle/{I}sar},
+  booktitle = {Proc.~of the International Conference on Types, Proofs and Programs (TYPES)},
+  year      = {2008},
+  pages     = {153-168},
+  series    = {LNCS},
+  volume    = {5497}
+}
+
+
+@TechReport{Yodaiken02,
+  author =       {V.~Yodaiken},
+  title =        {{A}gainst {P}riority {I}nheritance},
+  institution =  {Finite State Machine Labs (FSMLabs)},
+  year =         {2004}
+}
+
+
+@Book{Vahalia96,
+  author =       {U.~Vahalia},
+  title =        {{UNIX} {I}nternals: {T}he {N}ew {F}rontiers},
+  publisher =    {Prentice-Hall},
+  year =         {1996}
+}
+
+@Article{Reeves98,
+  title =	"{R}e: {W}hat {R}eally {H}appened on {M}ars?",
+  author =	"G.~E.~Reeves",
+  journal =	"Risks Forum",
+  year = 	"1998",
+  number =	"54",
+  volume =	"19"
+}
+
+@Article{Sha90,
+  title =	"{P}riority {I}nheritance {P}rotocols: {A}n {A}pproach to
+		 {R}eal-{T}ime {S}ynchronization",
+  author =	"L.~Sha and R.~Rajkumar and J.~P.~Lehoczky",
+  journal =	"IEEE Transactions on Computers",
+  year = 	"1990",
+  number =	"9",
+  volume =	"39",
+  pages =	"1175--1185"
+}
+
+
+@Article{Lampson80,
+  author =	"B.~W.~Lampson and D.~D.~Redell",
+  title =	"{{E}xperiences with {P}rocesses and {M}onitors in {M}esa}",
+  journal =	"Communications of the ACM",
+  volume =	"23",
+  number =	"2",
+  pages =	"105--117",
+  year = 	"1980"
+}
+
+@inproceedings{Wang09,
+  author    = {J.~Wang and H.~Yang and X.~Zhang},
+  title     = {{L}iveness {R}easoning with {I}sabelle/{HOL}},
+  booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in 
+               Higher Order Logics (TPHOLs)},
+  year      = {2009},
+  pages     = {485--499},
+  volume    = {5674},
+  series    = {LNCS}
+}
+
+@PhdThesis{Faria08,
+  author =       {J.~M.~S.~Faria},
+  title =        {{F}ormal {D}evelopment of {S}olutions for {R}eal-{T}ime {O}perating {S}ystems 
+                 with {TLA+/TLC}},
+  school =       {University of Porto},
+  year =         {2008}
+}
+
+
+@Article{Paulson98,
+  author =       {L.~C.~Paulson},
+  title =        {{T}he {I}nductive {A}pproach to {V}erifying {C}ryptographic {P}rotocols},
+  journal =      {Journal of Computer Security},
+  year =         {1998},
+  volume =       {6},
+  number =       {1--2},
+  pages =        {85--128}
+}
+
+@MISC{locke-july02,
+author = {D. Locke},
+title = {Priority Inheritance: The Real Story},
+month = July,
+year = {2002},
+howpublished={\url{http://www.math.unipd.it/~tullio/SCD/2007/Materiale/Locke.pdf}},
+}
+
+
+@InProceedings{Steinberg10,
+  author =       {U.~Steinberg and A.~B\"otcher and B.~Kauer},
+  title =        {{T}imeslice {D}onation in {C}omponent-{B}ased {S}ystems},
+  booktitle = {Proc.~of the 6th International Workshop on Operating Systems
+               Platforms for Embedded Real-Time Applications (OSPERT)},
+  pages =     {16--23},
+  year =      {2010}
+}
+
+@inproceedings{dutertre99b,
+  title =	"{T}he {P}riority {C}eiling {P}rotocol: {F}ormalization and
+		 {A}nalysis {U}sing {PVS}",
+  author =	"B.~Dutertre",
+  booktitle = {Proc.~of the 21st IEEE Conference on Real-Time Systems Symposium (RTSS)},
+  year = {2000},
+  pages = {151--160},
+  publisher = {IEEE Computer Society}
+}
+
+@InProceedings{Jahier09,
+  title =	"{S}ynchronous {M}odeling and {V}alidation of {P}riority
+		 {I}nheritance {S}chedulers",
+  author =	"E.~Jahier and B.~Halbwachs and P.~Raymond",
+  booktitle =	"Proc.~of the 12th International Conference on Fundamental 
+                 Approaches to Software Engineering (FASE)",
+  year = 	"2009",
+  volume =	"5503",
+  series =      "LNCS",
+  pages =	"140--154"
+}
+
+@InProceedings{Wellings07,
+  title =	"{I}ntegrating {P}riority {I}nheritance {A}lgorithms in the {R}eal-{T}ime 
+                 {S}pecification for {J}ava",
+  author =	"A.~Wellings and A.~Burns and O.~M.~Santos and B.~M.~Brosgol",
+  publisher =	"IEEE Computer Society",
+  year = 	"2007",
+  booktitle =	"Proc.~of the 10th IEEE International Symposium on Object 
+                and Component-Oriented Real-Time Distributed Computing (ISORC)",
+  pages =	"115--123"
+}
+
+@Article{Wang:2002:SGP,
+  author =	"Y. Wang and E. Anceaume and F. Brasileiro and F.
+		 Greve and M. Hurfin",
+  title =	"Solving the group priority inversion problem in a
+		 timed asynchronous system",
+  journal =	"IEEE Transactions on Computers",
+  volume =	"51",
+  number =	"8",
+  pages =	"900--915",
+  month =	aug,
+  year = 	"2002",
+  CODEN =	"ITCOB4",
+  doi =  	"http://dx.doi.org/10.1109/TC.2002.1024738",
+  ISSN = 	"0018-9340 (print), 1557-9956 (electronic)",
+  issn-l =	"0018-9340",
+  bibdate =	"Tue Jul 5 09:41:56 MDT 2011",
+  bibsource =	"http://www.computer.org/tc/;
+		 http://www.math.utah.edu/pub/tex/bib/ieeetranscomput2000.bib",
+  URL =  	"http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=1024738",
+  acknowledgement = "Nelson H. F. Beebe, University of Utah, Department
+		 of Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake
+		 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1
+		 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
+		 \path|beebe@acm.org|, \path|beebe@computer.org|
+		 (Internet), URL:
+		 \path|http://www.math.utah.edu/~beebe/|",
+  fjournal =	"IEEE Transactions on Computers",
+  doi-url =	"http://dx.doi.org/10.1109/TC.2002.1024738",
+}
+
+@Article{journals/rts/BabaogluMS93,
+  title =	"A Formalization of Priority Inversion",
+  author =	"{\"O} Babaoglu and K. Marzullo and F. B. Schneider",
+  journal =	"Real-Time Systems",
+  year = 	"1993",
+  number =	"4",
+  volume =	"5",
+  bibdate =	"2011-06-03",
+  bibsource =	"DBLP,
+		 http://dblp.uni-trier.de/db/journals/rts/rts5.html#BabaogluMS93",
+  pages =	"285--303",
+  URL =  	"http://dx.doi.org/10.1007/BF01088832",
+}
+
diff -r c4783e4ef43f -r a04084de4946 Paper/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.tex	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,79 @@
+\documentclass[runningheads]{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{mathpartir}
+\usepackage{tikz}
+\usepackage{pgf}
+%\usetikzlibrary{arrows,automata,decorations,fit,calc}
+%\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
+%\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
+%\usetikzlibrary{matrix}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+%%\usepackage{proof}
+%%\usepackage{mathabx}
+\usepackage{stmaryrd}
+\usepackage{url}
+\usepackage{color}
+\titlerunning{Proving the Priority Inheritance Protocol Correct}
+
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymiota}{}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+\definecolor{mygrey}{rgb}{.80,.80,.80}
+
+\begin{document}
+
+\title{Priority Inheritance Protocol Proved Correct}
+\author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
+\institute{PLA University of Science and Technology, China \and 
+           King's College London, United Kingdom}
+\maketitle
+
+\begin{abstract}
+In real-time systems with threads, resource locking and 
+priority sched\-uling, one faces the problem of Priority
+Inversion. This problem can make the behaviour of threads
+unpredictable and the resulting bugs can be hard to find.  The
+Priority Inheritance Protocol is one solution implemented in many
+systems for solving this problem, but the correctness of this solution
+has never been formally verified in a theorem prover. As already
+pointed out in the literature, the original informal investigation of
+the Property Inheritance Protocol presents a correctness ``proof'' for
+an \emph{incorrect} algorithm. In this paper we fix the problem of
+this proof by making all notions precise and implementing a variant of
+a solution proposed earlier. Our formalisation in Isabelle/HOL
+uncovers facts not mentioned in the literature, but also shows how to
+efficiently implement this protocol. Earlier correct implementations
+were criticised as too inefficient. Our formalisation is based on
+Paulson's inductive approach to verifying protocols.\medskip
+
+{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
+real-time systems, Isabelle/HOL
+\end{abstract}
+
+\input{session}
+
+%\bibliographystyle{plain}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff -r c4783e4ef43f -r a04084de4946 Paper/tt.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/tt.thy	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,94 @@
+
+There are several works on inversion avoidance:
+\begin{enumerate}
+\item {\em Solving the group priority inversion problem in a timed asynchronous system}. 
+The notion of \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> is introduced. The main strategy is still inversion avoidance. 
+The method is by reordering requests in the setting of Client-Server.
+\item {\em Examples of inaccurate specification of the protocol}.
+\end{enumerate}
+
+
+
+
+
+
+section{* Related works *}
+
+text {*
+1.	<<Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java>> models and 
+verifies the combination of Priority Inheritance (PI) and Priority Ceiling Emulation (PCE) protocols in 
+the setting of Java virtual machine using extended Timed Automata(TA) formalism of the UPPAAL tool. 
+Although a detailed formal model of combined PI and PCE is given, the number of properties is quite 
+small and the focus is put on the harmonious working of PI and PCE. Most key features of PI 
+(as well as PCE) are not shown. Because of the limitation of the model checking technique
+ used there, properties are shown only for a small number of scenarios. Therefore, the verification 
+does not show the correctness of the formal model itself in a convincing way.  
+2.	<< Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC>>. A formal model 
+of PI is given in TLA+. Only 3 properties are shown for PI using model checking. The limitation of 
+model checking is intrinsic to the work.
+3.	<<Synchronous modeling and validation of priority inheritance schedulers>>. Gives a formal model 
+of PI and PCE in AADL (Architecture Analysis & Design Language) and checked several properties 
+using model checking. The number of properties shown there is less than here and the scale 
+is also limited by the model checking technique. 
+
+
+There are several works on inversion avoidance:
+1.	<<Solving the group priority inversion problem in a timed asynchronous system>>. 
+The notion of \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> is introduced. The main strategy is still inversion avoidance. 
+The method is by reordering requests in the setting of Client-Server.
+
+
+<<Examples of inaccurate specification of the protocol>>.
+
+*}
+
+text {*
+
+\section{An overview of priority inversion and priority inheritance}
+
+Priority inversion refers to the phenomenon when a thread with high priority is blocked 
+by a thread with low priority. Priority happens when the high priority thread requests 
+for some critical resource already taken by the low priority thread. Since the high 
+priority thread has to wait for the low priority thread to complete, it is said to be 
+blocked by the low priority thread. Priority inversion might prevent high priority 
+thread from fulfill its task in time if the duration of priority inversion is indefinite 
+and unpredictable. Indefinite priority inversion happens when indefinite number 
+of threads with medium priorities is activated during the period when the high 
+priority thread is blocked by the low priority thread. Although these medium 
+priority threads can not preempt the high priority thread directly, they are able 
+to preempt the low priority threads and cause it to stay in critical section for 
+an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. 
+
+Priority inheritance is one protocol proposed to avoid indefinite priority inversion. 
+The basic idea is to let the high priority thread donate its priority to the low priority 
+thread holding the critical resource, so that it will not be preempted by medium priority 
+threads. The thread with highest priority will not be blocked unless it is requesting 
+some critical resource already taken by other threads. Viewed from a different angle, 
+any thread which is able to block the highest priority threads must already hold some 
+critical resource. Further more, it must have hold some critical resource at the 
+moment the highest priority is created, otherwise, it may never get change to run and 
+get hold. Since the number of such resource holding lower priority threads is finite, 
+if every one of them finishes with its own critical section in a definite duration, 
+the duration the highest priority thread is blocked is definite as well. The key to 
+guarantee lower priority threads to finish in definite is to donate them the highest 
+priority. In such cases, the lower priority threads is said to have inherited the 
+highest priority. And this explains the name of the protocol: 
+{\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay.
+
+The objectives of this paper are:
+\begin{enumerate}
+\item Build the above mentioned idea into formal model and prove a series of properties 
+until we are convinced that the formal model does fulfill the original idea. 
+\item Show how formally derived properties can be used as guidelines for correct 
+and efficient implementation.
+\end{enumerate}.
+The proof is totally formal in the sense that every detail is reduced to the 
+very first principles of Higher Order Logic. The nature of interactive theorem 
+proving is for the human user to persuade computer program to accept its arguments. 
+A clear and simple understanding of the problem at hand is both a prerequisite and a 
+byproduct of such an effort, because everything has finally be reduced to the very 
+first principle to be checked mechanically. The former intuitive explanation of 
+Priority Inheritance is just such a byproduct. 
+*}
+
+*)