equal
deleted
inserted
replaced
19 \noindent |
19 \noindent |
20 Define the datatype of \rmindex{binary trees}:% |
20 Define the datatype of \rmindex{binary trees}:% |
21 \end{isamarkuptext}% |
21 \end{isamarkuptext}% |
22 \isamarkuptrue% |
22 \isamarkuptrue% |
23 \isacommand{datatype}\isamarkupfalse% |
23 \isacommand{datatype}\isamarkupfalse% |
24 \ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}% |
24 \ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}% |
25 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
26 \noindent |
26 \noindent |
27 Define a function \isa{mirror} that mirrors a binary tree |
27 Define a function \isa{mirror} that mirrors a binary tree |
28 by swapping subtrees recursively. Prove% |
28 by swapping subtrees recursively. Prove% |
29 \end{isamarkuptext}% |
29 \end{isamarkuptext}% |
30 \isamarkuptrue% |
30 \isamarkuptrue% |
31 \isacommand{lemma}\isamarkupfalse% |
31 \isacommand{lemma}\isamarkupfalse% |
32 \ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequoteopen}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequoteclose}% |
32 \ mirror{\isaliteral{5F}{\isacharunderscore}}mirror{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}mirror{\isaliteral{28}{\isacharparenleft}}mirror\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequoteclose}}% |
33 \isadelimproof |
33 \isadelimproof |
34 % |
34 % |
35 \endisadelimproof |
35 \endisadelimproof |
36 % |
36 % |
37 \isatagproof |
37 \isatagproof |
48 Define a function \isa{flatten} that flattens a tree into a list |
48 Define a function \isa{flatten} that flattens a tree into a list |
49 by traversing it in infix order. Prove% |
49 by traversing it in infix order. Prove% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 \isamarkuptrue% |
51 \isamarkuptrue% |
52 \isacommand{lemma}\isamarkupfalse% |
52 \isacommand{lemma}\isamarkupfalse% |
53 \ {\isachardoublequoteopen}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequoteclose}% |
53 \ {\isaliteral{22}{\isachardoublequoteopen}}flatten{\isaliteral{28}{\isacharparenleft}}mirror\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev{\isaliteral{28}{\isacharparenleft}}flatten\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
54 \isadelimproof |
54 \isadelimproof |
55 % |
55 % |
56 \endisadelimproof |
56 \endisadelimproof |
57 % |
57 % |
58 \isatagproof |
58 \isatagproof |