\batchmode
\documentstyle[a4wide,apalike,html,12pt,verbatim]{article}
\makeatletter
\renewcommand {\htmladdnormallink}[2]{#1}
\newcommand {\LEGOLIB}{/usr/local/share/lego/lib}
\newcommand {\Hoare}[3]{\left\{#1\right\}#2\left\{#3\right\}}
\makeatother
\newenvironment{tex2html_wrap}{}{}
\newwrite\lthtmlwrite
\def\lthtmltypeout#1{{\let\protect\string\immediate\write\lthtmlwrite{#1}}}%
\newbox\sizebox
\begin{document}
\pagestyle{empty}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\eta$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline349: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\leq$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline353: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \begin{displaymath}x \leq y = \exists s {:} \mbox{\it nat}\ x + s = y.
\end{displaymath}
}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{\it list} \alpha \rightarrow
\alpha + \empty$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline359: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{0,\ldots,n-1\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline361: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\iota$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline377: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\left\{p\right\}S\left\{q\right\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline391: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\sigma$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline395: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mathop p\sigma$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline397: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\tau$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline401: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mathop q\tau$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline403: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \begin{displaymath}\left\{p[t/x]\right\}x:=t\left\{p\right\}\mbox,\end{displaymath}
}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\}S\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline407: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\}\,\texttt{skip}\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline415: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$p\to q$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline417: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\}\,x:=t\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline419: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$p\to r[t/x]$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline423: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$r\to q$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline425: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\}\,S_1;S_2\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline427: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\}\,S_1\,\{r\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline431: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{r\}\,S_2\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline433: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\}\,\textbf{if}\ b\ \textbf{then}\ S_1\ \textbf{else}\ S_2\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline435: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\wedge b\}\,S_1\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline437: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\wedge{\neg
b}\}\,S_2\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline439: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{p\}\,\textbf{while}\ b\ \textbf{do}\ S\ \textbf{od}\,\{q\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline441: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$p\to r$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline445: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\{r\wedge b\}\,S\{r\}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline447: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$(r\wedge{\neg b})\to q$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline449: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
\stepcounter{subsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$(i/j) \leq (i'/j') \iff i \times j' \leq i' \times j$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline491: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\end{document}