1749 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\ |
1749 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\ |
1750 \textbf{nitpick} \\[2\smallskipamount] |
1750 \textbf{nitpick} \\[2\smallskipamount] |
1751 {\slshape Nitpick ran out of time after checking 9 of 10 scopes.} |
1751 {\slshape Nitpick ran out of time after checking 9 of 10 scopes.} |
1752 \postw |
1752 \postw |
1753 |
1753 |
1754 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree |
1754 Furthermore, applying \textit{skew} or \textit{split} on a well-formed tree |
1755 should not alter the tree: |
1755 should not alter the tree: |
1756 |
1756 |
1757 \prew |
1757 \prew |
1758 \textbf{theorem}~\textit{wf\_skew\_split\/}:\\ |
1758 \textbf{theorem}~\textit{wf\_skew\_split\/}:\\ |
1759 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\ |
1759 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\ |
1800 \hbox{}\qquad Evaluated term: \\ |
1800 \hbox{}\qquad Evaluated term: \\ |
1801 \hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$ |
1801 \hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$ |
1802 \postw |
1802 \postw |
1803 |
1803 |
1804 Nitpick's output reveals that the element $0$ was added as a left child of $1$, |
1804 Nitpick's output reveals that the element $0$ was added as a left child of $1$, |
1805 where both have a level of 1. This violates the second AA tree invariant, which |
1805 where both nodes have a level of 1. This violates the second AA tree invariant, |
1806 states that a left child's level must be less than its parent's. This shouldn't |
1806 which states that a left child's level must be less than its parent's. This |
1807 come as a surprise, considering that we commented out the tree rebalancing code. |
1807 shouldn't come as a surprise, considering that we commented out the tree |
1808 Reintroducing the code seems to solve the problem: |
1808 rebalancing code. Reintroducing the code seems to solve the problem: |
1809 |
1809 |
1810 \prew |
1810 \prew |
1811 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\ |
1811 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\ |
1812 \textbf{nitpick} \\[2\smallskipamount] |
1812 \textbf{nitpick} \\[2\smallskipamount] |
1813 {\slshape Nitpick ran out of time after checking 8 of 10 scopes.} |
1813 {\slshape Nitpick ran out of time after checking 8 of 10 scopes.} |