\batchmode

\documentclass[11pt]{article}
\RequirePackage{ifthen}



\usepackage{times}
\usepackage{a4}
\usepackage{pstricks}
\usepackage{pst-node}
\usepackage{html}


%
\providecommand{\online}[1]{(Available online\footnote{\texttt{#1}}\/)}
%
\providecommand{\hak}{Hassan A\"{\i}t-Kaci}
%
\providecommand{\aka}{\emph{a.k.a.}}%
\providecommand{\etal}{\emph{et al.}}%
\providecommand{\cf}{\emph{cf.}}%
\providecommand{\eg}{\emph{e.g.}}%
\providecommand{\etc}{\emph{etc.}}%
\providecommand{\ie}{\emph{i.e.}}%
\providecommand{\viz}{\emph{viz.}}
%
\providecommand{\opl}{\textsc{Opl}}%
\providecommand{\matisse}{\textsc{Matisse}}
\long

\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage[centertags]{amsmath}
\usepackage{theorem}
\usepackage{fleqn}

\theoremheaderfont{\scshape}

\newtheorem{theorem}{Theorem}[section]\newtheorem{definition}{Definition}[section]\newtheorem{corollary}{Corollary}[section]
\theorembodyfont{\normalfont\slshape }
\newtheorem{example}{Example}[section]\newtheorem{proof}{Proof}[section]
%
\renewcommand{\empty}{\emptyset}
%
\renewcommand{\c}[1]{\ensuremath{{\mathcal #1}}}%
\renewcommand{\t}[1]{\ensuremath{\mathtt{#1}}}%
\renewcommand{\b}[1]{\ensuremath{\mathbf{#1}}}
%
\providecommand{\m}[1]{\ensuremath{\mathbb{#1}}}%
\providecommand{\g}[1]{\ensuremath{\mathfrak{#1}}}
%
\providecommand{\true}{\ensuremath{\mathfrak{true}}}%
\providecommand{\false}{\ensuremath{\mathfrak{false}}}
%
\providecommand{\NN}{\ensuremath{\mathbb{N}}}%
\providecommand{\BB}{\ensuremath{\mathbb{B}}}
%
\providecommand{\C}{\b {C}}%
\providecommand{\V}{\b {V}}%
\providecommand{\T}{\b {T}}%
\providecommand{\OP}{\b {O}}
%
\providecommand{\BT}{\c {B}}%
\providecommand{\VT}{\c {V}}%
\providecommand{\TT}{\c {T}}
%
\providecommand{\MON}[3]{\langle #1,#2,#3\rangle}
%
\providecommand{\abs}[2]{\lambda #1.#2}%
\providecommand{\app}[2]{#1\;#2}%
\providecommand{\arr}[2]{#1\rightarrow #2}
%
\providecommand{\pr}[2]{\langle #1,#2\rangle}%
\providecommand{\tp}[2]{\langle #1, \cdots, #2\rangle}%
\providecommand{\pj}[2]{#1.#2}
%
\providecommand{\ite}[3]{\ensuremath{\mathfrak{if}}\;#1\;\ensuremath{\mathfrak{then}}\;#2\;\ensuremath{\mathfrak{else}}\;#3}
%
\providecommand{\fix}{\ensuremath{\mathfrak{fix}}}%
\providecommand{\op}{\ensuremath{\mathfrak{op}}}
%
\providecommand{\integer}{\t {int}}%
\providecommand{\bool}{\t {bool}}
%
\providecommand{\gives}{\;\longrightarrow\;}%
\providecommand{\from}{\;\leftarrow\;}
%
\providecommand{\subst}[3]{#3[#1/#2]}
%
\providecommand{\typerule}[2]{\displaystyle\frac{#1}{#2}}%
\providecommand{\sequent}[3]{#1\;\vdash\;#2 : #3}
%
\providecommand{\type}{\b {type}}%
\providecommand{\eqd}{\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}}
%
\providecommand{\set}{\t {set}}%
\providecommand{\bag}{\t {bag}}%
\providecommand{\lst}{\t {list}}
%
\providecommand{\conc}{\ensuremath{\!+\!\!+}}
%
\providecommand{\Z}[1]{\ensuremath{\mathfrak{z}}_{#1}}%
\providecommand{\U}[1]{\ensuremath{\mathfrak{u}}_{#1}}%
\providecommand{\Ty}[1]{\ensuremath{\mathfrak{T}}_{#1}}%
\providecommand{\Co}[1]{\ensuremath{\mathfrak{C}}_{#1}}%
\providecommand{\E}[1]{\Theta_{#1}}
%
\providecommand{\mset}[1]{\{\!\!\{#1\}\!\!\}}
%
\providecommand{\eset}{\{\}}%
\providecommand{\elst}{[]}%
\providecommand{\ebag}{\{\!\!\{\}\!\!\}}
%
\providecommand{\HOM}[2]{\ensuremath{\ensuremath{\mathfrak{hom}}_{#1}^{#2}}}
%
\providecommand{\subeq}[2]{\ensuremath{\Theta_{#1}\subseteq\Theta_{#2}}}
%
\providecommand{\comp}[3]{\ensuremath{#1\{#2\;[\!]\;#3\}}}%
\providecommand{\setcomp}[2]{\ensuremath{\{#1\;[\!]\;#2\}}}
%
\renewcommand{\Join}{\vartriangleright\!\!\vartriangleleft}

\usepackage[dvips]{pstcol}


\pagecolor[gray]{.7}

\usepackage[latin1]{inputenc}



\makeatletter

\makeatletter
\count@=\the\catcode`\_ \catcode`\_=8 
\newenvironment{tex2html_wrap}{}{}%
\catcode`\<=12\catcode`\_=\count@
\newcommand{\providedcommand}[1]{\expandafter\providecommand\csname #1\endcsname}%
\newcommand{\renewedcommand}[1]{\expandafter\providecommand\csname #1\endcsname{}%
  \expandafter\renewcommand\csname #1\endcsname}%
\newcommand{\newedenvironment}[1]{\newenvironment{#1}{}{}\renewenvironment{#1}}%
\let\newedcommand\renewedcommand
\let\renewedenvironment\newedenvironment
\makeatother
\let\mathon=$
\let\mathoff=$
\ifx\AtBeginDocument\undefined \newcommand{\AtBeginDocument}[1]{}\fi
\newbox\sizebox
\setlength{\hoffset}{0pt}\setlength{\voffset}{0pt}
\addtolength{\textheight}{\footskip}\setlength{\footskip}{0pt}
\addtolength{\textheight}{\topmargin}\setlength{\topmargin}{0pt}
\addtolength{\textheight}{\headheight}\setlength{\headheight}{0pt}
\addtolength{\textheight}{\headsep}\setlength{\headsep}{0pt}
\setlength{\textwidth}{349pt}
\newwrite\lthtmlwrite
\makeatletter
\let\realnormalsize=\normalsize
\global\topskip=2sp
\def\preveqno{}\let\real@float=\@float \let\realend@float=\end@float
\def\@float{\let\@savefreelist\@freelist\real@float}
\def\liih@math{\ifmmode$\else\bad@math\fi}
\def\end@float{\realend@float\global\let\@freelist\@savefreelist}
\let\real@dbflt=\@dbflt \let\end@dblfloat=\end@float
\let\@largefloatcheck=\relax
\let\if@boxedmulticols=\iftrue
\def\@dbflt{\let\@savefreelist\@freelist\real@dbflt}
\def\adjustnormalsize{\def\normalsize{\mathsurround=0pt \realnormalsize
 \parindent=0pt\abovedisplayskip=0pt\belowdisplayskip=0pt}%
 \def\phantompar{\csname par\endcsname}\normalsize}%
\def\lthtmltypeout#1{{\let\protect\string \immediate\write\lthtmlwrite{#1}}}%
\newcommand\lthtmlhboxmathA{\adjustnormalsize\setbox\sizebox=\hbox\bgroup\kern.05em }%
\newcommand\lthtmlhboxmathB{\adjustnormalsize\setbox\sizebox=\hbox to\hsize\bgroup\hfill }%
\newcommand\lthtmlvboxmathA{\adjustnormalsize\setbox\sizebox=\vbox\bgroup %
 \let\ifinner=\iffalse \let\)\liih@math }%
\newcommand\lthtmlboxmathZ{\@next\next\@currlist{}{\def\next{\voidb@x}}%
 \expandafter\box\next\egroup}%
\newcommand\lthtmlmathtype[1]{\gdef\lthtmlmathenv{#1}}%
\newcommand\lthtmllogmath{\lthtmltypeout{l2hSize %
:\lthtmlmathenv:\the\ht\sizebox::\the\dp\sizebox::\the\wd\sizebox.\preveqno}}%
\newcommand\lthtmlfigureA[1]{\let\@savefreelist\@freelist
       \lthtmlmathtype{#1}\lthtmlvboxmathA}%
\newcommand\lthtmlpictureA{\bgroup\catcode`\_=8 \lthtmlpictureB}%
\newcommand\lthtmlpictureB[1]{\lthtmlmathtype{#1}\egroup
       \let\@savefreelist\@freelist \lthtmlhboxmathB}%
\newcommand\lthtmlpictureZ[1]{\hfill\lthtmlfigureZ}%
\newcommand\lthtmlfigureZ{\lthtmlboxmathZ\lthtmllogmath\copy\sizebox
       \global\let\@freelist\@savefreelist}%
\newcommand\lthtmldisplayA{\bgroup\catcode`\_=8 \lthtmldisplayAi}%
\newcommand\lthtmldisplayAi[1]{\lthtmlmathtype{#1}\egroup\lthtmlvboxmathA}%
\newcommand\lthtmldisplayB[1]{\edef\preveqno{(\theequation)}%
  \lthtmldisplayA{#1}\let\@eqnnum\relax}%
\newcommand\lthtmldisplayZ{\lthtmlboxmathZ\lthtmllogmath\lthtmlsetmath}%
\newcommand\lthtmlinlinemathA{\bgroup\catcode`\_=8 \lthtmlinlinemathB}
\newcommand\lthtmlinlinemathB[1]{\lthtmlmathtype{#1}\egroup\lthtmlhboxmathA
  \vrule height1.5ex width0pt }%
\newcommand\lthtmlinlineA{\bgroup\catcode`\_=8 \lthtmlinlineB}%
\newcommand\lthtmlinlineB[1]{\lthtmlmathtype{#1}\egroup\lthtmlhboxmathA}%
\newcommand\lthtmlinlineZ{\egroup\expandafter\ifdim\dp\sizebox>0pt %
  \expandafter\centerinlinemath\fi\lthtmllogmath\lthtmlsetinline}
\newcommand\lthtmlinlinemathZ{\egroup\expandafter\ifdim\dp\sizebox>0pt %
  \expandafter\centerinlinemath\fi\lthtmllogmath\lthtmlsetmath}
\newcommand\lthtmlindisplaymathZ{\egroup %
  \centerinlinemath\lthtmllogmath\lthtmlsetmath}
\def\lthtmlsetinline{\hbox{\vrule width.1em \vtop{\vbox{%
  \kern.1em\copy\sizebox}\ifdim\dp\sizebox>0pt\kern.1em\else\kern.3pt\fi
  \ifdim\hsize>\wd\sizebox \hrule depth1pt\fi}}}
\def\lthtmlsetmath{\hbox{\vrule width.1em\kern-.05em\vtop{\vbox{%
  \kern.1em\kern0.8 pt\hbox{\hglue.17em\copy\sizebox\hglue0.8 pt}}\kern.3pt%
  \ifdim\dp\sizebox>0pt\kern.1em\fi \kern0.8 pt%
  \ifdim\hsize>\wd\sizebox \hrule depth1pt\fi}}}
\def\centerinlinemath{%
  \dimen1=\ifdim\ht\sizebox<\dp\sizebox \dp\sizebox\else\ht\sizebox\fi
  \advance\dimen1by.5pt \vrule width0pt height\dimen1 depth\dimen1 
 \dp\sizebox=\dimen1\ht\sizebox=\dimen1\relax}

\def\lthtmlcheckvsize{\ifdim\ht\sizebox<\vsize 
  \ifdim\wd\sizebox<\hsize\expandafter\hfill\fi \expandafter\vfill
  \else\expandafter\vss\fi}%
\providecommand{\selectlanguage}[1]{}%
\makeatletter \tracingstats = 1 
\providecommand{\Eta}{\textrm{H}}
\providecommand{\Mu}{\textrm{M}}
\providecommand{\Alpha}{\textrm{A}}
\providecommand{\Iota}{\textrm{J}}
\providecommand{\Nu}{\textrm{N}}
\providecommand{\Omicron}{\textrm{O}}
\providecommand{\omicron}{\textrm{o}}
\providecommand{\Chi}{\textrm{X}}
\providecommand{\Beta}{\textrm{B}}
\providecommand{\Kappa}{\textrm{K}}
\providecommand{\Tau}{\textrm{T}}
\providecommand{\Epsilon}{\textrm{E}}
\providecommand{\Zeta}{\textrm{Z}}
\providecommand{\Rho}{\textrm{R}}


\begin{document}
\pagestyle{empty}\thispagestyle{empty}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength hsize=\the\hsize}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength vsize=\the\vsize}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength hoffset=\the\hoffset}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength voffset=\the\voffset}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength topmargin=\the\topmargin}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength topskip=\the\topskip}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength headheight=\the\headheight}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength headsep=\the\headsep}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength parskip=\the\parskip}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength oddsidemargin=\the\oddsidemargin}\lthtmltypeout{}%
\makeatletter
\if@twoside\lthtmltypeout{latex2htmlLength evensidemargin=\the\evensidemargin}%
\else\lthtmltypeout{latex2htmlLength evensidemargin=\the\oddsidemargin}\fi%
\lthtmltypeout{}%
\makeatother
\setcounter{page}{1}
\onecolumn

% !!! IMAGES START HERE !!!

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5038}%
$ \lambda $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5061}%
$ \ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5063}%
$ f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5065}%
$ \oplus$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5067}%
$ \odot$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5075}%
$ \ensuremath{\ensuremath{\mathfrak{hom}}_{\ensuremath{\!+\!\!+}}^{\cup}}[\lambda x.x+1]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5077}%
$ [1,2,1,3,2]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5079}%
$ \{2,3,4\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5081}%
$ \ensuremath{\mathfrak{hom}}_{\ensuremath{\!+\!\!+}}^{\cup}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5085}%
$ L$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5087}%
\begin{displaymath}
\begin{array}{ll}
\t{result}\;\leftarrow\;\{\}; \\ 
\b{foreach}\;\; x\;\; \b{in}\;\; L \;\;\b{do}\; \t{result}\;\leftarrow\;\t{result}\cup f(x); \\ 
\b{return}\;\; \t{result};
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5096}%
$ \Theta_{\oplus}\subseteq\Theta_{\odot}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5098}%
\begin{displaymath}
\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;\;\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}\;\;}l}
\ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](\ensuremath{\mathfrak{z}}_{\oplus})    & \ensuremath{\mathfrak{z}}_{\odot} \\ 
\ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](\ensuremath{\mathfrak{u}}_{\oplus}(x)) & f(x) \\ 
\ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](x\oplus y)     & \ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](x) \odot
                                        \ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](y)
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5100}%
$ f:\alpha\rightarrow \ensuremath{\mathfrak{T}}_{\odot}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5102}%
$ x:\alpha$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5104}%
$ y:\alpha$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5106}%
$ \ensuremath{\mathfrak{T}}_{\oplus}=\ensuremath{\mathfrak{C}}_{\oplus}(\alpha)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5108}%
\begin{displaymath}\begin{array}{ll} \t{result}\;\leftarrow\;\ensuremath{\mathfrak{z}}_{\odot}; \\  \b{foreach}\;\; x_i\;\;\b{in}\;\;\ensuremath{\mathfrak{u}}_{\oplus}(x_1)\oplus\cdots\oplus\ensuremath{\mathfrak{u}}_{\oplus}(x_n) \;\;\b{do}\; \t{result}\;\leftarrow\;\t{result}\odot f(x_i); \\  \b{return}\;\; \t{result}; \end{array}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5112}%
$ \{C\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5114}%
$ \{I\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5116}%
$ \{C,I\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5118}%
$ \ensuremath{\mathfrak{hom}}_{\cup}^{+}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5120}%
\begin{displaymath}
\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;=\;}l}
1 & \ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{+}}[\lambda x.1](\{a\}) \\ 
  & \ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{+}}[\lambda x.1](\{a\}\cup\{a\}) \\ 
  & \ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{+}}[\lambda x.1](\{a\}) \;+\;\ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{+}}[\lambda x.1](\{a\}) \\ 
  & 1 + 1 \\ 
  & 2.
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5124}%
$ x_0\oplus x_0=x_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5126}%
$ x_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5128}%
\begin{displaymath}
\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;=\;}l}
\ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](x_0) & \ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](x_0\oplus x_0) \\ 
 & \ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](x_0) \;\odot\; \ensuremath{\ensuremath{\mathfrak{hom}}_{\oplus}^{\odot}}[f](x_0)
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5132}%
\begin{displaymath}
\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;=\;}l}
\t{length}(l)   & \ensuremath{\ensuremath{\mathfrak{hom}}_{\ensuremath{\!+\!\!+}}^{+}}[\lambda x.1](l) \\ 
e \in s         & \ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{\vee}}[\lambda x.x=e](s) \\ 
s \times t      &
\ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{\cup}}[\lambda x.\ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{\cup}}[\lambda y.\{\langle x,y\rangle \}](t)](s) \\ 
\t{map}(f,s)    & \ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{\cup}}[\lambda x.\{f(x)\}](s) \\ 
\t{filter}(p,s) & \ensuremath{\ensuremath{\mathfrak{hom}}_{\cup}^{\cup}}[\lambda x.\ensuremath{\mathfrak{if}}\;p(x)\;\ensuremath{\mathfrak{then}}\;\{x\}\;\ensuremath{\mathfrak{else}}\;\{\}](s).
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5135}%
$ \{\langle x,x^2\rangle \;|\;x\in\ensuremath{\mathbb{N}}, \exists
n.x=2n\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5137}%
$ \langle x,x^2\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5139}%
$ x\in\ensuremath{\mathbb{N}}, \exists n.x=2n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5143}%
$ \oplus\{e\;[\!]\;Q\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5145}%
$ e$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5147}%
$ Q$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5149}%
$ q_1,\ldots,q_n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5151}%
$ n\geq0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5153}%
$ q_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5155}%
$ x\;\leftarrow\;e$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5157}%
$ x$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5161}%
$ \phi$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5172}%
\begin{displaymath}\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}\;}l}
\ensuremath{\oplus\{e\;[\!]\;\}}& \left\{\begin{array}{ll}
                            \ensuremath{\mathfrak{u}}_{\oplus}(e) & \mbox{if $\oplus$\  is a
                            collection monoid} \\ 
			    e & \mbox{if $\oplus$\  is a primitive monoid}
			    \end{array}\right. \\ 
\ensuremath{\oplus\{e\;[\!]\;x\;\leftarrow\;e', Q\}}&
                            \ensuremath{\ensuremath{\mathfrak{hom}}_{\odot}^{\oplus}}[\lambda x.\ensuremath{\oplus\{e\;[\!]\;Q\}}](e')
                            \\ 
\ensuremath{\oplus\{e\;[\!]\;c, Q\}}& \ensuremath{\mathfrak{if}}\;c\;\ensuremath{\mathfrak{then}}\;\ensuremath{\oplus\{e\;[\!]\;Q\}}\;\ensuremath{\mathfrak{else}}\;\ensuremath{\mathfrak{z}}_{\oplus}
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5174}%
$ e:\ensuremath{\mathfrak{T}}_{\oplus}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5176}%
$ e':\ensuremath{\mathfrak{T}}_{\odot}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5182}%
$ x\;\leftarrow\;e'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5186}%
$ S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5188}%
$ T$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5192}%
$ p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5194}%
$\displaystyle S \vartriangleright\!\!\vartriangleleft _p^f T \;\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}\; \ensuremath{\cup\{f(x,y)\;[\!]\;x\;\leftarrow\;S, y\;\leftarrow\;T, p(x,y)\}}.$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5198}%
$ \t{l}_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5200}%
$ e_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5202}%
$ i=1,\ldots,n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5204}%
$ \langle \t{l}_1=e_1,,\ldots,\t{l}_n=e_n\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5206}%
$ f(x,y) =
\langle \t{name}=y.\t{name},\t{age}=2*x.\t{age}\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5208}%
$ p(x,y)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5210}%
$ x.\t{name}=y.\t{name}, x.\t{age}\geq 18$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5212}%
\begin{displaymath}
\begin{array}{l@{\hskip2em}l}
\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;\;\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}\;\;}l}
\exists x\in s.e & \ensuremath{\vee\{e\;[\!]\;x\;\leftarrow\;s\}}\\ 
\forall x\in s.e & \ensuremath{\wedge\{e\;[\!]\;x\;\leftarrow\;s\}}\\ 
x \in s          & \ensuremath{\vee\{x=y\;[\!]\;y\;\leftarrow\;s\}}\\ 
s \cap t         & \ensuremath{\cup\{x\;[\!]\;x\;\leftarrow\;s, x\in t\}}\\ 
\t{count}(a,s)   & \ensuremath{+\{1\;[\!]\;x\;\leftarrow\;s, x=a\}}\\ 
\end{array}
&
\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;\;\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}\;\;}l}
\t{length}(s)   & \ensuremath{+\{1\;[\!]\;x\;\leftarrow\;s\}}\\ 
\t{sum}(s)      & \ensuremath{+\{x\;[\!]\;x\;\leftarrow\;s\}}\\ 
\t{max}(s)      & \ensuremath{\max\{x\;[\!]\;x\;\leftarrow\;s\}}\\ 
\t{filter}(p,s) & \ensuremath{\cup\{x\;[\!]\;x\;\leftarrow\;s, p(x)\}}\\ 
\t{flatten}(s)  & \ensuremath{\cup\{x\;[\!]\;t\;\leftarrow\;s, x\;\leftarrow\;t\}}\\ 
\end{array}
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5214}%
$ \t{sum}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlfigureA{figure536}%
\begin{figure}\begin{center}
\fbox{$\begin{array}{rrll}
e & ::= & \bot          & \mbox{null value} \\
  &   | & c             & \mbox{constant} \\
  &   | & x             & \mbox{symbol} \\
  &   | & \lambda x.e    & \mbox{abstraction} \\
  &   | & e_1\;e_2& \mbox{application} \\
  &   | & \langle \t {l}_1=e_1, \cdots, \t {l}_n=e_n\rangle  & \mbox{record} \\
  &   | & e.\t {l} & \mbox{projection} \\
  &   | & \ensuremath{\mathfrak{if}}\;e_1\;\ensuremath{\mathfrak{then}}\;e_2\;\ensuremath{\mathfrak{else}}\;e_3 & \mbox{conditional} \\
&   | & \ensuremath{\mathfrak{z}}_{\oplus}    & \mbox{monoid identity} \\
  &   | & \ensuremath{\mathfrak{u}}_{\oplus}(e) & \mbox{monoid unit injection} \\
  &   | & e_1\oplus e_2 & \mbox{monoid operation} \\
  &   | & \ensuremath{\oplus\{e\;[\!]\;Q\}}& \mbox{monoid comprehension} \\
\end{array}$}\end{center}
\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{figure573}%
\begin{figure}\begin{center}
\fbox{\begin{tabular}{rl}
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;\bot : \alpha }$& for any $\Gamma$\  \\\\
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;c : \tau }$& for any $\Gamma$, if $\ensuremath{\mathbf{type}}(a)=\tau$\  \\\\
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;x : \tau }$& if $\Gamma(x)=\tau$\  \\\\
\par
$\displaystyle\frac{\Gamma[x:\tau_1]\;\vdash\;e : \tau_2 }{\Gamma\;\vdash\;\lambda x.e : \tau_1\rightarrow \tau_2 }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e_1 : \tau_1\rightarrow \tau_2 ,
\          \Gamma\;\vdash\;e_2 : \tau_1 }{\Gamma\;\vdash\;e_1\;e_2 : \tau_2 }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e_1 : \tau_1 ,
\          \cdots,
\          \Gamma\;\vdash\;e_k : \tau_k }{\Gamma\;\vdash\;\langle \t {l}_1=e_1, \cdots, \t {l}_k=e_k\rangle  : \langle \t {l}_1:\tau_1, \cdots, \t {l}_k:\tau_k\rangle }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e : \langle \t {l}_1:\tau_1, \cdots, \t {l}_k:\tau_k\rangle }{\Gamma\;\vdash\;e.\t {l} : \tau }$& if $\t {l}\in\{\t {l}_1,\ldots,\t {l}_k\}$\  \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e_1 : \ensuremath{\mathtt{bool}},
\          \Gamma\;\vdash\;e_2 : \tau ,
\          \Gamma\;\vdash\;e_3 : \tau }{\Gamma\;\vdash\;\ensuremath{\mathfrak{if}}\;e_1\;\ensuremath{\mathfrak{then}}\;e_2\;\ensuremath{\mathfrak{else}}\;e_3 : \tau }$& \\\\
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;\ensuremath{\mathfrak{z}}_{\oplus} : \ensuremath{\mathfrak{T}}_{\oplus}}$& for any $\Gamma$\  \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e : \tau }{\Gamma\;\vdash\;\ensuremath{\mathfrak{u}}_{\oplus}(e) : \ensuremath{\mathfrak{C}}_{\oplus}(\tau)}$& if $\oplus$\  is a collection monoid \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e_1 : \ensuremath{\mathfrak{T}}_{\oplus}
,\;        \Gamma\;\vdash\;e_2 : \ensuremath{\mathfrak{T}}_{\oplus}}{\Gamma\;\vdash\;e_1 \oplus e_2 : \ensuremath{\mathfrak{T}}_{\oplus}}$& if $\oplus$\  is a primitive monoid \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e_1 : \ensuremath{\mathfrak{C}}_{\oplus}(\tau)
,\;        \Gamma\;\vdash\;e_2 : \ensuremath{\mathfrak{C}}_{\oplus}(\tau)}{\Gamma\;\vdash\;e_1 \oplus e_2 : \ensuremath{\mathfrak{C}}_{\oplus}(\tau)}$& if $\oplus$\  is a collection monoid \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e : \ensuremath{\mathfrak{T}}_{\oplus}}{\Gamma\;\vdash\;\ensuremath{\oplus\{e\;[\!]\;\}}: \ensuremath{\mathfrak{T}}_{\oplus}}$& if $\oplus$\  is a primitive monoid \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e : \tau }{\Gamma\;\vdash\;\ensuremath{\oplus\{e\;[\!]\;\}}: \ensuremath{\mathfrak{C}}_{\oplus}(\tau)}$& if $\oplus$\  is a collection monoid \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e_2 : \ensuremath{\mathfrak{C}}_{\odot}(\tau_2)
,\;        \Gamma[x:\tau_2]\;\vdash\;\ensuremath{\oplus\{e_1\;[\!]\;Q\}}: \tau_1 }{\Gamma\;\vdash\;\ensuremath{\oplus\{e_1\;[\!]\;x\;\leftarrow\;e_2,Q\}}: \tau_1 }$& if \ensuremath{\Theta_{\odot}\subseteq\Theta_{\oplus}}\\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;e_2 : \ensuremath{\mathtt{bool}},\;        \Gamma\;\vdash\;\ensuremath{\oplus\{e_1\;[\!]\;Q\}}: \tau }{\Gamma\;\vdash\;\ensuremath{\oplus\{e_1\;[\!]\;e_2,Q\}}: \tau }$& 
\par
\end{tabular}}\end{center}
\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
{\newpage\clearpage
\lthtmlfigureA{figure726}%
\begin{figure}\par\begin{center}
\par\begin{tabular}{cccccccccc}
&&& \rnode{TYPE}{type} \\[3cm]
\par\rnode{BASIC}{basic} &
\rnode{STRUCTURE}{structure} &
\rnode{RANGE}{range} &
\rnode{ENUM}{enum} &
\rnode{SETOF}{setof(type)} &
\rnode{ARRAY}{array[type]} \\
\par\end{tabular}
\ncline{-}{TYPE}{BASIC}
\ncline{-}{TYPE}{STRUCTURE}
\ncline{-}{TYPE}{RANGE}
\ncline{-}{TYPE}{ENUM}
\ncline{-}{TYPE}{SETOF}
\ncline{-}{TYPE}{ARRAY}
\end{center}
\par\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\appendix
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5290}%
$ \star$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5292}%
$ S\times
S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5296}%
$ \epsilon\in S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5298}%
$ \langle S,\star,\epsilon\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5300}%
$ x, y, z$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5304}%
$\displaystyle x\star(y\star z) = (x\star y)\star z$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5306}%
$\displaystyle x\star\epsilon = \epsilon\star x = \epsilon.$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5308}%
$ \ensuremath{\mathbb{N}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5310}%
$ \ensuremath{\mathbb{B}}=\{\ensuremath{\mathfrak{true}},\ensuremath{\mathfrak{false}}\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5312}%
$ \langle \ensuremath{\mathbb{N}},+,0\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5314}%
$ \langle \ensuremath{\mathbb{N}},*,1\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5316}%
$ \langle \ensuremath{\mathbb{N}},\max,0\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5318}%
$ \langle \ensuremath{\mathbb{B}},\vee,\ensuremath{\mathfrak{false}}\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5320}%
$ \langle \ensuremath{\mathbb{B}},\wedge,\ensuremath{\mathfrak{true}}\rangle $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5324}%
$\displaystyle x\star y = y\star x$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5326}%
$ x, y$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5328}%
$ \max$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5330}%
$ \vee$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5332}%
$ \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5334}%
$\displaystyle x\star x = x$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5344}%
$ T_{\star}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5348}%
$ \cup_{n\geq 0}T_n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5350}%
$\displaystyle T_n \;\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}\; \left\{ \begin{array}{ll} \ensuremath{\mathbb{N}}& \makebox{if $n=0$} \\  \\  \{ t_1\star t_2 \;|\; t_i\in T_{n-1}, i=1,2 \} & \makebox{if $n>0$} \end{array}\right.$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5358}%
$ T_{\star}\times T_{\star}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5362}%
$ t_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5364}%
$ t_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5370}%
$ t_1\star t_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5382}%
$ 1\star(2\star3)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5384}%
$ (1\star2)\star3$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5396}%
$ [1,2,1]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5398}%
$ 1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5400}%
$ 2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5404}%
$ \{1,2\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5406}%
$ \{\!\!\{1,2,1\}\!\!\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5416}%
$ x\star\epsilon$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5418}%
$ \ensuremath{\mathfrak{u}}_{\star}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5420}%
$ \ensuremath{\!+\!\!+}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5422}%
$ \ensuremath{\mathfrak{u}}_{\ensuremath{\!+\!\!+}}(x)=[x]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5424}%
$ [a,b,c]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5426}%
$ [a]\ensuremath{\!+\!\!+}[b]\ensuremath{\!+\!\!+}[c]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5428}%
$ \{a,b,c\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5430}%
$ \{a\}\cup\{b\}\cup\{c\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5432}%
$ \{\!\!\{a,b,c\}\!\!\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5434}%
$ \{\!\!\{a\}\!\!\}\uplus\{\!\!\{b\}\!\!\}\uplus\{\!\!\{c\}\!\!\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5442}%
$ \ensuremath{\mathfrak{T}}_{\oplus}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5444}%
$ \oplus:
\ensuremath{\mathfrak{T}}_{\oplus}\times\ensuremath{\mathfrak{T}}_{\oplus}\rightarrow \ensuremath{\mathfrak{T}}_{\oplus}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5446}%
$ \ensuremath{\mathfrak{z}}_{\oplus} : \ensuremath{\mathfrak{T}}_{\oplus}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5448}%
$ \Theta_{\oplus}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5452}%
$ C$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5454}%
$ I$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5456}%
$ \ensuremath{\mathfrak{C}}_{\oplus}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5460}%
$ \ensuremath{\mathfrak{u}}_{\oplus} : \alpha\rightarrow \ensuremath{\mathfrak{C}}_{\oplus}(\alpha)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}


\renewcommand{\arraystretch}{1.2}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5466}%
$ \ensuremath{\mathfrak{z}}_{\oplus}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5470}%
$ +$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5472}%
$ \mathtt{int}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5477}%
$ *$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5494}%
$ \mathtt{bool}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5496}%
$ \ensuremath{\mathfrak{false}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5504}%
$ \ensuremath{\mathfrak{true}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}


\renewcommand{\arraystretch}{1.2}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5540}%
$ \ensuremath{\mathfrak{u}}_{\oplus}(x)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5544}%
$ \cup$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5546}%
$ \ensuremath{\mathtt{set}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5548}%
$ \ensuremath{\mathtt{set}}(\alpha)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5550}%
$ \{\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5552}%
$ \{x\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5556}%
$ \uplus$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5558}%
$ \ensuremath{\mathtt{bag}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5560}%
$ \ensuremath{\mathtt{bag}}(\alpha)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5562}%
$ \{\!\!\{\}\!\!\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5564}%
$ \{\!\!\{x\}\!\!\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5570}%
$ \ensuremath{\mathtt{list}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5572}%
$ \ensuremath{\mathtt{list}}(\alpha)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5574}%
$ []$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5576}%
$ [x]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5578}%
$ \emptyset $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5616}%
$ \ensuremath{\mathbf{C}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5618}%
$ a, b
\ldots$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5620}%
$ \ensuremath{\mathbf{V}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5622}%
$ x, y, \ldots$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5624}%
$ t$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5628}%
\begin{displaymath}\begin{array}{rrlll} t & ::= & a          & (a\in\ensuremath{\mathbf{C}}) & \mbox{constant} \\    &   | & x          & (x\in\ensuremath{\mathbf{V}}) & \mbox{symbol} \\    &   | & \lambda x.t & (x\in\ensuremath{\mathbf{V}}) & \mbox{abstraction} \\    &   | & t\;t &          & \mbox{application} \end{array}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5630}%
$ \ensuremath{\mathbf{T}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5634}%
$ \lambda x.t$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5640}%
$ t_1[t_2/x]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5650}%
$ \beta$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5652}%
\begin{displaymath}\begin{array}{rl} (\lambda x.t_1)\;t_2 & \;\longrightarrow\;t_1[t_2/x]. \end{array}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5654}%
$ \ensuremath{{\mathcal B}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5656}%
$ A, B,
\ldots$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5658}%
$ \ensuremath{{\mathcal V}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5660}%
$ \alpha, \beta, \ldots$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5662}%
$ \tau$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5666}%
\begin{displaymath}\begin{array}{rrlll} \tau & ::= & A                 & (A\in\ensuremath{{\mathcal B}})      & \mbox{basic type} \\       &   | & \alpha            & (\alpha\in\ensuremath{{\mathcal V}}) & \mbox{variable type} \\       &   | & \tau\rightarrow \tau   &                & \mbox{function type} \end{array}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5668}%
$ \ensuremath{{\mathcal T}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5682}%
$ \ensuremath{\mathbf{type}}(a)=\tau$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5684}%
$ a$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5688}%
$ \Gamma$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5690}%
$ V$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5696}%
$ x\in\ensuremath{\mathbf{V}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5698}%
$ \tau\in\ensuremath{{\mathcal T}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5700}%
$\displaystyle \Gamma[x:\tau](y) \ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}\left\{ \begin{array}{ll} \tau      & \mbox{if $x = y$}; \\  \\  \Gamma(y) & \mbox{if $x\neq y$}. \end{array}\right.$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5702}%
$ \Gamma[x:\tau]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5728}%
$ \Gamma\;\vdash\;t : \tau $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5738}%
$ t:\tau$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5744}%
$\displaystyle \displaystyle\frac{\Gamma_1\;\vdash\;t_1 : \tau_n ,\   \cdots\   \Gamma_n\;\vdash\;t_n : \tau_n }{\Gamma\;\vdash\;t : \tau }
$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5754}%
$ \tau_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5756}%
$ \Gamma_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5758}%
$ t_n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5760}%
$ \tau_n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5762}%
$ \Gamma_n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5764}%
$ n=0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_indisplay5766}%
$\displaystyle \displaystyle\frac{}{\Gamma\;\vdash\;t : \tau }
$%
\lthtmlindisplaymathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{figure1006}%
\begin{figure}\begin{center}
\fbox{\begin{tabular}{rl}
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;a : \tau }$& for any $\Gamma$, if $\ensuremath{\mathbf{type}}(a)=\tau$\  \\\\
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;x : \tau }$& if $\Gamma(x)=\tau$\  \\\\
\par
$\displaystyle\frac{\Gamma[x:\tau_1]\;\vdash\;t : \tau_2 }{\Gamma\;\vdash\;\lambda x.t : \tau_1\rightarrow \tau_2 }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;t_1 : \tau_1\rightarrow \tau_2 , \ \Gamma\;\vdash\;t_2 : \tau_1 }{\Gamma\;\vdash\;t_1\;t_2 : \tau_2 }
$\  &
\end{tabular}}\end{center}
\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5785}%
$ +, *,
-, /, \vee, \wedge,$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5787}%
$ \ensuremath{\mathbf{O}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5789}%
$ t_1+t_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5791}%
$ (+\;t_1)\;t_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5795}%
$ n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5801}%
$ f(t_1,\ldots,t_{k})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5803}%
$ 1\leq k < n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5807}%
$ \lambda x_1.\ldots\lambda x_{n-k}.f(t_1,\ldots,t_{k},x_1,\ldots,x_{n-k})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5811}%
$ f(t_1,\ldots,t_n) = (\ldots(f\;t_1)
\ldots t_{n-1})\;t_n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5813}%
\begin{displaymath}\begin{array}{rrlll} t & ::= & a          & (a\in\ensuremath{\mathbf{C}}=\ensuremath{\mathbb{N}}\cup\ensuremath{\mathbb{B}}\cup\ensuremath{\mathbf{O}}) & \mbox{constant} \\    &   | & x          & (x\in\ensuremath{\mathbf{V}})                   & \mbox{symbol} \\    &   | & \lambda x.t & (x\in\ensuremath{\mathbf{V}})                   & \mbox{abstraction} \\    &   | & t\;t &                            & \mbox{application} \\    &   | & \langle t, \cdots, t\rangle   &                            & \mbox{tupling} \\    &   | & t.n  & (n\in\ensuremath{\mathbb{N}})                  & \mbox{projection} \\    &   | & \ensuremath{\mathfrak{if}}\;t\;\ensuremath{\mathfrak{then}}\;t\;\ensuremath{\mathfrak{else}}\;t &                         & \mbox{conditional} \\    &   | & \ensuremath{\mathfrak{fix}}\;t &                         & \mbox{recursion} \end{array}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5815}%
\begin{displaymath}\begin{array}{rl} \langle t_1, \cdots, t_k\rangle .i & \;\longrightarrow\;\left\{    \begin{array}{ll}    t_i & \mbox{if $1\leq i\leq k$} \\  \\     \mbox{undefined otherwise}    \end{array}\right. \\  \\  \ensuremath{\mathfrak{if}}\;c\;\ensuremath{\mathfrak{then}}\;t_1\;\ensuremath{\mathfrak{else}}\;t_2 & \;\longrightarrow\;\left\{    \begin{array}{ll}    t_1 & \mbox{if $c=\ensuremath{\mathfrak{true}}$} \\  \\     t_2 & \mbox{if $c=\ensuremath{\mathfrak{false}}$} \\  \\     \mbox{undefined otherwise}    \end{array}\right. \\  \\  \ensuremath{\mathfrak{fix}}\;t & \;\longrightarrow\;t\;(\ensuremath{\mathfrak{fix}}\;t) \end{array}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5817}%
\begin{displaymath}\begin{array}{rrlll} \tau & ::= & \ensuremath{\mathtt{int}}\;|\; \ensuremath{\mathtt{bool}}&                & \mbox{basic type} \\       &   | & \alpha               & (\alpha\in\ensuremath{{\mathcal V}}) & \mbox{variable type} \\       &   | & \langle \tau, \cdots, \tau\rangle       &                & \mbox{tuple type} \\       &   | & \tau\rightarrow \tau      &                & \mbox{function type} \end{array}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5819}%
$ \ensuremath{\mathbf{type}}(n)=\ensuremath{\mathtt{int}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5821}%
$ n\in\ensuremath{\mathbb{N}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5823}%
$ \ensuremath{\mathbf{type}}(\ensuremath{\mathfrak{true}})=\ensuremath{\mathtt{bool}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5825}%
$ \ensuremath{\mathbf{type}}(\ensuremath{\mathfrak{false}})=\ensuremath{\mathtt{bool}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5827}%
$ \ensuremath{\mathbf{type}}(+)=\ensuremath{\mathtt{int}}\rightarrow (\ensuremath{\mathtt{int}}\rightarrow \ensuremath{\mathtt{int}})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5829}%
$ \ensuremath{\mathbf{type}}(\vee)=\ensuremath{\mathtt{bool}}\rightarrow (\ensuremath{\mathtt{bool}}\rightarrow \ensuremath{\mathtt{bool}})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{figure1133}%
\begin{figure}\begin{center}
\fbox{\begin{tabular}{rl}
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;a : \tau }$& for any $\Gamma$, if $\ensuremath{\mathbf{type}}(a)=\tau$\  \\\\
\par
$\displaystyle\frac{}{\Gamma\;\vdash\;x : \tau }$& if $\Gamma(x)=\tau$\  \\\\
\par
$\displaystyle\frac{\Gamma[x:\tau_1]\;\vdash\;t : \tau_2 }{\Gamma\;\vdash\;\lambda x.t : \tau_1\rightarrow \tau_2 }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;t_1 : \tau_1\rightarrow \tau_2 ,
\          \Gamma\;\vdash\;t_2 : \tau_1 }{\Gamma\;\vdash\;t_1\;t_2 : \tau_2 }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;t_1 : \tau_1 ,
\          \cdots,
\          \Gamma\;\vdash\;t_k : \tau_k }{\Gamma\;\vdash\;\langle t_1, \cdots, t_k\rangle  : \langle \tau_1, \cdots, \tau_k\rangle }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;t : \langle \tau_1, \cdots, \tau_k\rangle }{\Gamma\;\vdash\;t.n : \tau }$& if $1\leq n\leq k$\  \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;t_1 : \ensuremath{\mathtt{bool}},
\          \Gamma\;\vdash\;t_2 : \tau ,
\          \Gamma\;\vdash\;t_3 : \tau }{\Gamma\;\vdash\;\ensuremath{\mathfrak{if}}\;t_1\;\ensuremath{\mathfrak{then}}\;t_2\;\ensuremath{\mathfrak{else}}\;t_3 : \tau }$& \\\\
\par
$\displaystyle\frac{\Gamma\;\vdash\;t : \tau\rightarrow \tau }{\Gamma\;\vdash\;\ensuremath{\mathfrak{fix}}\;t : \tau }$& 
\par
\end{tabular}}\end{center}
\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}

\end{document}
