1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Oct 22 14:51:47 2009 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Oct 22 16:34:30 2009 +0200
     1.3 @@ -1439,10 +1439,10 @@
     1.4  \phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
     1.5  \phantom{``$(\quad$}$k = 1 \mathrel{\land} (u = \Lambda \mathrel{\lor} (\textit{level}~u = 1 \mathrel{\land} \textit{left}~u = \Lambda \mathrel{\land} \textit{right}~u = \Lambda))$ \\
     1.6  \phantom{``$($}$\textrm{else}$ \\
     1.7 -\hbox{\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
     1.8 +\hbox{}\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
     1.9  \mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k
    1.10 -\mathrel{\land} \textit{level}~u \le k \mathrel{\land}
    1.11 -\textit{level}~(\textit{right}~u) < k)$''}\kern-200mm
    1.12 +\mathrel{\land} \textit{level}~u \le k$ \\
    1.13 +\hbox{}\phantom{``$(\quad$}${\land}\; \textit{level}~(\textit{right}~u) < k)$''
    1.14  \postw
    1.15  
    1.16  Rebalancing the tree upon insertion and removal of elements is performed by two