# HG changeset patch # User blanchet # Date 1288083617 -7200 # Node ID d170c322157ad96d524e51ac020005c3f8abd77f # Parent f2a14b6effcf8961b0c5479206c0a891e3db3d3e improved English diff -r f2a14b6effcf -r d170c322157a doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue Oct 26 10:59:28 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Tue Oct 26 11:00:17 2010 +0200 @@ -1751,7 +1751,7 @@ {\slshape Nitpick ran out of time after checking 9 of 10 scopes.} \postw -Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree +Furthermore, applying \textit{skew} or \textit{split} on a well-formed tree should not alter the tree: \prew @@ -1802,10 +1802,10 @@ \postw Nitpick's output reveals that the element $0$ was added as a left child of $1$, -where both have a level of 1. This violates the second AA tree invariant, which -states that a left child's level must be less than its parent's. This shouldn't -come as a surprise, considering that we commented out the tree rebalancing code. -Reintroducing the code seems to solve the problem: +where both nodes have a level of 1. This violates the second AA tree invariant, +which states that a left child's level must be less than its parent's. This +shouldn't come as a surprise, considering that we commented out the tree +rebalancing code. Reintroducing the code seems to solve the problem: \prew \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\