equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 Function \isa{rev} has quadratic worst-case running time |
5 Function \isa{rev} has quadratic worst-case running time |
5 because it calls function \isa{\at} for each element of the list and |
6 because it calls function \isa{\at} for each element of the list and |
6 \isa{\at} is linear in its first argument. A linear time version of |
7 \isa{\at} is linear in its first argument. A linear time version of |
86 need to generalize your proposition even further. This requires insight into |
87 need to generalize your proposition even further. This requires insight into |
87 the problem at hand and is beyond simple rules of thumb. In a nutshell: you |
88 the problem at hand and is beyond simple rules of thumb. In a nutshell: you |
88 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
89 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
89 to learn about some advanced techniques for inductive proofs.% |
90 to learn about some advanced techniques for inductive proofs.% |
90 \end{isamarkuptxt}% |
91 \end{isamarkuptxt}% |
91 \end{isabelle}% |
92 \end{isabellebody}% |
92 %%% Local Variables: |
93 %%% Local Variables: |
93 %%% mode: latex |
94 %%% mode: latex |
94 %%% TeX-master: "root" |
95 %%% TeX-master: "root" |
95 %%% End: |
96 %%% End: |