\nonstopmode

\documentclass[11pt]{article}
\makeatletter

\usepackage[a4paper]{anysize}
\usepackage{amsmath,amsfonts,amssymb,theorem}
\usepackage{rotating}
\usepackage{xspace}
\usepackage{heqn,html}

\providecommand{\mybigsqcap}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}} 
\providecommand{\bigsqcap}{{\raisebox{1.3ex}{\begin{turn}{180}$\bigsqcup$\end{turn}}}} 

\providecommand{\nrleq}[3]{\ensuremath{(\leqslant #1 \; #2 \; #3)} }
\providecommand{\nrgeq}[3]{\ensuremath{(\geqslant #1 \; #2 \; #3)} }

\providecommand{\alc}{\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}}\xspace}
\providecommand{\alcqi}{\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}\xspace}
\providecommand{\alco}{\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{O}}\xspace}
\providecommand{\alcqio}{\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}\xspace}
\providecommand{\alcqo}{\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}\xspace}
\providecommand{\alcq}{\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace}

\providecommand{\deltai}{\ensuremath{\Delta^\mathcal{I}} }

\providecommand{\ctwo}{\ensuremath{C^2}\xspace}
\providecommand{\nexptime}{\textsc{NExp\-Time}\xspace}
\providecommand{\exptime}{\textsc{Exp\-Time}\xspace}
\providecommand{\pspace}{\textsc{PSpace}\xspace}

\providecommand{\TcBox}{\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}}\xspace}
\providecommand{\TcBoxes}{\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Boxes}}\xspace}
\providecommand{\TgBox}{\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}\xspace}
\providecommand{\TgBoxes}{\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}}\xspace}

\providecommand{\shortcite}{\cite}
\providecommand{\shortciteA}{\cite}
\providecommand{\citeA}{\cite}

 {\theorembodyfont{\itshape } }
{ \theoremstyle{break} }
{ \theoremstyle{break} }
{ }
{ }

\providecommand{\qed}{}
\par\usepackage[dvips]{color}
\pagecolor[gray]{.7}


\makeatletter
\count@=\the\catcode`\_ \catcode`\_=8 
\newenvironment{tex2html_wrap}{}{} \catcode`\_=\count@
\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}{451pt}
\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\end@float{\realend@float\global\let\@freelist\@savefreelist}
\let\real@dbflt=\@dbflt \let\end@dblfloat=\end@float
\let\@largefloatcheck=\relax
\def\@dbflt{\let\@savefreelist\@freelist\real@dbflt}
\def\adjustnormalsize{\def\normalsize{\mathsurround=0pt \realnormalsize
 \parindent=0pt\abovedisplayskip=0pt\belowdisplayskip=0pt}\normalsize}%
\def\lthtmltypeout#1{{\let\protect\string\immediate\write\lthtmlwrite{#1}}}%
\newcommand\lthtmlhboxmathA{\adjustnormalsize\setbox\sizebox=\hbox\bgroup}%
\newcommand\lthtmlvboxmathA{\adjustnormalsize\setbox\sizebox=\vbox\bgroup%
 \let\ifinner=\iffalse }%
\newcommand\lthtmlboxmathZ{\@next\next\@currlist{}{\def\next{\voidb@x}}%
 \expandafter\box\next\egroup}%
\newcommand\lthtmlmathtype[1]{\def\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\lthtmlfigureZ{\lthtmlboxmathZ\lthtmllogmath\copy\sizebox
       \global\let\@freelist\@savefreelist}%
\newcommand\lthtmldisplayA[1]{\lthtmlmathtype{#1}\lthtmlvboxmathA}%
\newcommand\lthtmldisplayB[1]{\edef\preveqno{(\theequation)}%
  \lthtmldisplayA{#1}\let\@eqnnum\relax}%
\newcommand\lthtmldisplayZ{\lthtmlboxmathZ\lthtmllogmath\lthtmlsetmath}%
\newcommand\lthtmlinlinemathA[1]{\lthtmlmathtype{#1}\lthtmlhboxmathA  \vrule height1.5ex width0pt }%
\newcommand\lthtmlinlineA[1]{\lthtmlmathtype{#1}\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}
\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\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=\ht\sizebox
  \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\expandafter\vfill
  \else\expandafter\vss\fi}%
\makeatletter \tracingstats = 1 


\begin{document}
\pagestyle{empty}\thispagestyle{empty}%
\lthtmltypeout{latex2htmlLength hsize=\the\hsize}%
\lthtmltypeout{latex2htmlLength vsize=\the\vsize}%
\lthtmltypeout{latex2htmlLength hoffset=\the\hoffset}%
\lthtmltypeout{latex2htmlLength voffset=\the\voffset}%
\lthtmltypeout{latex2htmlLength topmargin=\the\topmargin}%
\lthtmltypeout{latex2htmlLength topskip=\the\topskip}%
\lthtmltypeout{latex2htmlLength headheight=\the\headheight}%
\lthtmltypeout{latex2htmlLength headsep=\the\headsep}%
\lthtmltypeout{latex2htmlLength parskip=\the\parskip}%
\lthtmltypeout{latex2htmlLength oddsidemargin=\the\oddsidemargin}%
\makeatletter
\if@twoside\lthtmltypeout{latex2htmlLength evensidemargin=\the\evensidemargin}%
\else\lthtmltypeout{latex2htmlLength evensidemargin=\the\oddsidemargin}\fi%
\makeatother
{\newpage\clearpage
% contents=\ensuremath  {\@mathcal {A}\tmspace  -\thinmuskip {.1667em}\@mathcal {L}\tmspace  -\thinmuskip {.1667em}\@mathcal {C}\tmspace  -\thinmuskip {.1667em}\@mathcal {Q}\tmspace  -\thinmuskip {.1667em}\@math...}
\lthtmlinlinemathA{tex2html_wrap_inline5193}%
\ensuremath  {\@mathcal {A}\tmspace  -\thinmuskip {.1667em}\@mathcal {L}\tmspace  -\thinmuskip {.1667em}\@mathcal {C}\tmspace  -\thinmuskip {.1667em}\@mathcal {Q}\tmspace  -\thinmuskip {.1667em}\@mathcal {I}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath  {\text  {T\hspace  {-1pt}}_C\hspace  {-1pt}\text  {Boxes}}
\lthtmlinlinemathA{tex2html_wrap_inline5195}%
\ensuremath  {\text  {T\hspace  {-1pt}}_C\hspace  {-1pt}\text  {Boxes}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}
\lthtmlinlinemathA{tex2html_wrap_inline2741}%
\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}
\lthtmlinlinemathA{tex2html_wrap_inline2743}%
\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{C^2}
\lthtmlinlinemathA{tex2html_wrap_inline2745}%
\ensuremath{C^2}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\textsc{NExp\-Time}
\lthtmlfigureA{tex2html_wrap4245}%
\textsc{NExp\-Time}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\textsc{Exp\-Time}
\lthtmlfigureA{tex2html_wrap4249}%
\textsc{Exp\-Time}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\textsc{PSpace}
\lthtmlfigureA{tex2html_wrap4255}%
\textsc{PSpace}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
% contents=\begin{displaymath}\texttt{Human}\sqcap (\texttt{Male}\sqcup \texttt{Female} ) \sqcap \ensuremath{(\geqslant 2 \; \texttt{hasChild}\; \texttt{Female} )}\sqcap \forall \texttt{hasChild} .\texttt{Human}...}
\lthtmldisplayA{displaymath2685}%
\begin{displaymath}\texttt{Human}\sqcap (\texttt{Male}\sqcup \texttt{Female} ) \sqcap \ensuremath{(\geqslant 2 \; \texttt{hasChild}\; \texttt{Female} )}\sqcap \forall \texttt{hasChild} .\texttt{Human}\end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}}
\lthtmlinlinemathA{tex2html_wrap_inline2767}%
\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathsf{K}$
\lthtmlinlinemathA{tex2html_wrap_inline3197}%
$\mathsf{K}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}
\lthtmlinlinemathA{tex2html_wrap_inline2783}%
\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}
\lthtmlinlinemathA{tex2html_wrap_inline2785}%
\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}\exists {\texttt{hasChild} ^{-1}}.{\texttt{ALICE} } \sqcap \exists {\texttt{hasChild} ^{-1}}.\texttt{BOB}\sqcap \exists {\texttt{livesWith} }.(\texttt{ALICE}\sqcup \texttt{BOB} ) . ...}
\lthtmldisplayA{displaymath2686}%
\begin{displaymath}\exists {\texttt{hasChild} ^{-1}}.{\texttt{ALICE} } \sqcap \exists
{\texttt{hasChild} ^{-1}}.\texttt{BOB}\sqcap \exists {\texttt{livesWith} }.(\texttt{ALICE}\sqcup \texttt{BOB} ) .
\end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{align*}\texttt{Parent} & = \texttt{Human}\sqcap (\geqslant  1 \;   {\texttt{hasChild} }) \sqcap \forall \texttt{hasChild} .\texttt{Human}\\\texttt{Toddler} &= \texttt{Human}\sqcap \texttt{VeryY...}
\lthtmlfigureA{alignstar159}%
\begin{align*}\texttt{Parent} & = \texttt{Human}\sqcap (\geqslant  1 \;
  {\texttt{hasChild} }) \sqcap \forall \texttt{hasChild} .\texttt{Human}\\
  \texttt{Toddler} &= \texttt{Human}\sqcap \texttt{VeryYoung}\\
  \texttt{BusyParent} &= \texttt{Parent}\sqcap \ensuremath{(\geqslant 2 \; \texttt{hasChild}\; \texttt{Toddler} )}\end{align*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\bot$
\lthtmlinlinemathA{tex2html_wrap_inline3199}%
$\bot$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{align*}\texttt{Female}\sqcap \texttt{Male} & = \bot\\\texttt{Female}\sqcup \texttt{Male} & = \texttt{Human}\sqcap (= 2 \    \texttt{hasChild} ^{-1} \ {\texttt{Human} }) \end{align*}
\lthtmlfigureA{alignstar176}%
\begin{align*}\texttt{Female}\sqcap \texttt{Male} & = \bot\\
  \texttt{Female}\sqcup \texttt{Male} & = \texttt{Human}\sqcap (= 2 \ 
  \texttt{hasChild} ^{-1} \ {\texttt{Human} })
\end{align*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}(\leq 2 \; (\texttt{Human}\sqcap \ensuremath{(\leqslant 0 \; \texttt{hasChild} ^{-1} \; \texttt{Human} )} )) \end{displaymath}
\lthtmldisplayA{displaymath2687}%
\begin{displaymath}(\leq 2 \; (\texttt{Human}\sqcap \ensuremath{(\leqslant 0 \; \texttt{hasChild} ^{-1} \; \texttt{Human} )} ))
\end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{figure}\begin{center}     \framebox[\textwidth]{       \begin{tabular}{l|cc|cc}         & \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace& \ensuremath{\mathcal{A}\!\mathc...}
\lthtmlfigureA{figure199}%
\begin{figure}\begin{center}
    \framebox[\textwidth]{
      \begin{tabular}{l|cc|cc}
        & \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace& \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}\xspace& \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}\xspace& \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}\xspace\\
      \hline
      Concept Satisfiability & \textsc{PSpace}\xspace-c. & open & \textsc{PSpace}\xspace-c. & \textbf{NExpTime}-c.\\
      GCIs & \textsc{Exp\-Time}\xspace-c. & \textsc{Exp\-Time}\xspace-c. & \textsc{Exp\-Time}\xspace-c. & \textbf{NExpTime}-c.\\
      Cardinality Restr. & \textbf{ExpTime}-c. & \textbf{ExpTime}-c. &
      \textbf{NExpTime}-c. & \textbf{NExpTime}-c.%
\end{tabular}
    }   \end{center}
  \end{figure}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
% contents=$A \in N_C$
\lthtmlinlinemathA{tex2html_wrap_inline3205}%
$A \in N_C$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}\neg C, \ C_1 \sqcap C_2, \   \text{and} \ \ensuremath{(\geqslant n \; S \; C)} ,   \end{displaymath}
\lthtmldisplayA{displaymath2688}%
\begin{displaymath}\neg C, \ C_1 \sqcap C_2, \   \text{and} \ \ensuremath{(\geqslant n \; S \; C)} ,
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$n \in \mathbb{N} $
\lthtmlinlinemathA{tex2html_wrap_inline3213}%
$n \in \mathbb{N} $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$R \in   N_R$
\lthtmlinlinemathA{tex2html_wrap_inline3219}%
$R \in
  N_R$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\geqslant   n \ C)$
\lthtmlinlinemathA{tex2html_wrap_inline3221}%
$(\geqslant
  n \ C)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\leqslant n \ C)$
\lthtmlinlinemathA{tex2html_wrap_inline3223}%
$(\leqslant n \ C)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}}
\lthtmlinlinemathA{tex2html_wrap_inline2817}%
\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I} = (\Delta^\mathcal{I},\cdot^\mathcal{I})$
\lthtmlinlinemathA{tex2html_wrap_inline3229}%
$\mathcal{I} = (\Delta^\mathcal{I},\cdot^\mathcal{I})$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\Delta^\mathcal{I}}
\lthtmlinlinemathA{tex2html_wrap_inline2819}%
\ensuremath{\Delta^\mathcal{I}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\cdot^\mathcal{I})$
\lthtmlinlinemathA{tex2html_wrap_inline3231}%
$(\cdot^\mathcal{I})$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$A^{\mathcal{I}}$
\lthtmlinlinemathA{tex2html_wrap_inline3235}%
$A^{\mathcal{I}}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$R^{\mathcal{I}}$
\lthtmlinlinemathA{tex2html_wrap_inline3239}%
$R^{\mathcal{I}}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\ensuremath{\Delta^\mathcal{I}}\times \ensuremath{\Delta^\mathcal{I}} $
\lthtmlinlinemathA{tex2html_wrap_inline3241}%
$\ensuremath{\Delta^\mathcal{I}}\times \ensuremath{\Delta^\mathcal{I}} $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\sharp M$
\lthtmlinlinemathA{tex2html_wrap_inline3243}%
$\sharp M$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{align*}(\neg C)^{\mathcal{I}} & := \ensuremath{\Delta^\mathcal{I}}\setminus C^{\mathcal{I}},\\(C_1 \sqcap C_2)^{\mathcal{I}} & :=  C_1^{\mathcal{I}} \cap C_2^{\mathcal{I}},\\(\geqslant n \ R \ ...}
\lthtmlfigureA{alignstar242}%
\begin{align*}(\neg C)^{\mathcal{I}} & := \ensuremath{\Delta^\mathcal{I}}\setminus C^{\mathcal{I}},\\
    (C_1 \sqcap C_2)^{\mathcal{I}} & :=  C_1^{\mathcal{I}} \cap C_2^{\mathcal{I}},\\
    (\geqslant n \ R \ C)^{\mathcal{I}} & := \{ a \in \ensuremath{\Delta^\mathcal{I}}\mid
    \sharp\{ b \in \ensuremath{\Delta^\mathcal{I}}\mid (a,b) \in R^{\mathcal{I}} \wedge b \in C^{\mathcal{I}} \} \geq n
    \}, \\
    (\geqslant n \ R^{-1} \ C)^{\mathcal{I}} & := \{ a \in \ensuremath{\Delta^\mathcal{I}}\mid \sharp\{ b \in
    \ensuremath{\Delta^\mathcal{I}}\mid (b,a) \in R^{\mathcal{I}} \wedge b \in C^{\mathcal{I}} \} \geq n \}.
  \end{align*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3247}%
$\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\sharp (C^{\mathcal{I}}) \geq n$
\lthtmlinlinemathA{tex2html_wrap_inline3251}%
$\sharp (C^{\mathcal{I}}) \geq n$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\sharp   (C^{\mathcal{I}}) \leq n$
\lthtmlinlinemathA{tex2html_wrap_inline3255}%
$\sharp
  (C^{\mathcal{I}}) \leq n$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models T$
\lthtmlinlinemathA{tex2html_wrap_inline3265}%
$\mathcal{I}\models T$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\forall \ C)$
\lthtmlinlinemathA{tex2html_wrap_inline3269}%
$(\forall \ C)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\leqslant 0 \; \neg C)$
\lthtmlinlinemathA{tex2html_wrap_inline3271}%
$(\leqslant
0 \; \neg C)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}\begin{array}{r@{\;}c@{\;}l@{\qquad}r@{\;}c@{\;}l}   C_1 \sqcup C_2 & = & \neg(\neg C_1 \sqcap \neg  C_2) & \ensuremath{(\leqslant n \; S \; C)} & = &   \neg \ensuremath{(\geqslant ...}
\lthtmldisplayA{displaymath2689}%
\begin{displaymath}\begin{array}{r@{\;}c@{\;}l@{\qquad}r@{\;}c@{\;}l}
  C_1 \sqcup C_2 & = & \neg(\neg C_1 \sqcap \neg  C_2) & \ensuremath{(\leqslant n \; S \; C)} & = &
  \neg \ensuremath{(\geqslant (n+1) \; S \; C)}\\
   C_1 \rightarrow C_2 & 
  = & \neg C_1 \sqcup C_2 & (=n \; S \; C) & = & \ensuremath{(\leqslant n \; S \; C)}\sqcap \ensuremath{(\geqslant n \; S \; C)}\\
  \exists S.C & = & \ensuremath{(\geqslant 1 \; S \; C)} & \top & = & A \sqcup \neg A \quad \text{for some
    } A \in N_C\\
   \forall S.C & = & \ensuremath{(\leqslant 0 \; S \; \neg C)}\end{array}
\end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\leqslant 0 \ (C \sqcap \neg D) \sqcup (\neg C \sqcap D))$
\lthtmlinlinemathA{tex2html_wrap_inline3279}%
$(\leqslant 0 \ (C \sqcap \neg D) \sqcup (\neg C \sqcap D))$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C^\mathcal{I}= D^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3285}%
$C^\mathcal{I}= D^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C^\mathcal{I}\neq \emptyset$
\lthtmlinlinemathA{tex2html_wrap_inline3295}%
$C^\mathcal{I}\neq
\emptyset$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$T \cup \{(\geqslant \ 1 \ C) \}$
\lthtmlinlinemathA{tex2html_wrap_inline3301}%
$T \cup \{(\geqslant \ 1 \ C) \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{figure}   \begin{center}     \framebox[\textwidth]{       $\begin{array}{l@{\;}c@{\;}l}         \Psi_x(A) & := & Ax \hfill \text{for $A \in N_C$ }\\\Psi_x(\neg C) & := & \neg \Psi_x(C)\\\Psi_x(...}
\lthtmlfigureA{figure278}%
\begin{figure}
  \begin{center}
    \framebox[\textwidth]{
      $\begin{array}{l@{\;}c@{\;}l}
        \Psi_x(A) & := & Ax \hfill \text{for $A \in N_C$ }\\
        \Psi_x(\neg C) & := & \neg \Psi_x(C)\\
        \Psi_x(C_1 \sqcap C_2) & := & \Psi_x(C_1) \wedge \Psi_x(C_2)\\
        \Psi_x \ensuremath{(\geqslant n \; R \; C)} & := & \exists^{\geq n} y.(Rxy \wedge \Psi_y(C))\\
        \Psi_x \ensuremath{(\geqslant n \; R^{-1} \; C)} & := & \exists^{\geq n} y.(Ryx \wedge
        \Psi_y(C))\\[1ex]
        \Psi_y(C) & := & \Psi_x(C)[x \backslash y, y \backslash x]\\[1ex]
        \Psi(\bowtie n \ C) & := & \exists^{\bowtie n} x.\Psi_x(C) \hfill
        \text{for $\bowtie \;\in \{ \geqslant,\leqslant\}$ }\\[1ex]
        \Psi(T) & := & \bigwedge \{ \Psi(\bowtie \ n \ C) \mid (\bowtie \
        n \ C) \in T \}
      \end{array}$       }   \end{center}
  \end{figure}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\exists^{\geq \ell}$
\lthtmlinlinemathA{tex2html_wrap_inline3309}%
$\exists^{\geq \ell}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\Psi$
\lthtmlinlinemathA{tex2html_wrap_inline3311}%
$\Psi$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{section}
\stepcounter{subsection}
{\newpage\clearpage
% contents=$\mathbb{Z} _n$
\lthtmlinlinemathA{tex2html_wrap_inline3323}%
$\mathbb{Z} _n$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\{0,\dots,n-1\}$
\lthtmlinlinemathA{tex2html_wrap_inline3325}%
$\{0,\dots,n-1\}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\oplus_n$
\lthtmlinlinemathA{tex2html_wrap_inline3327}%
$\oplus_n$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{D} = (D,H,V)$
\lthtmlinlinemathA{tex2html_wrap_inline3331}%
$\mathcal{D} = (D,H,V)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$H,V   \subseteq D \times D$
\lthtmlinlinemathA{tex2html_wrap_inline3335}%
$H,V
  \subseteq D \times D$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$s,t \in \mathbb{N} $
\lthtmlinlinemathA{tex2html_wrap_inline3337}%
$s,t \in \mathbb{N} $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathbb{Z} _s \times \mathbb{Z} _t$
\lthtmlinlinemathA{tex2html_wrap_inline3341}%
$\mathbb{Z} _s \times \mathbb{Z} _t$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$w = w_0 \dots w_{n-1}$
\lthtmlinlinemathA{tex2html_wrap_inline3343}%
$w = w_0 \dots w_{n-1}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$n \leq s$
\lthtmlinlinemathA{tex2html_wrap_inline3349}%
$n \leq s$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{D}$
\lthtmlinlinemathA{tex2html_wrap_inline3351}%
$\mathcal{D}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\tau:   U(s,t) \rightarrow D$
\lthtmlinlinemathA{tex2html_wrap_inline3357}%
$\tau:
  U(s,t) \rightarrow D$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(x,y) \in U(s,t)$
\lthtmlinlinemathA{tex2html_wrap_inline3359}%
$(x,y) \in U(s,t)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\tau(x,y) = d$
\lthtmlinlinemathA{tex2html_wrap_inline3361}%
$\tau(x,y) = d$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\tau(x     \oplus_s 1,y) = d'$
\lthtmlinlinemathA{tex2html_wrap_inline3363}%
$\tau(x
    \oplus_s 1,y) = d'$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(d,d') \in H$
\lthtmlinlinemathA{tex2html_wrap_inline3365}%
$(d,d') \in H$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\tau(x, y \oplus_t 1) = d'$
\lthtmlinlinemathA{tex2html_wrap_inline3369}%
$\tau(x, y \oplus_t 1) = d'$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(d,d')     \in V$
\lthtmlinlinemathA{tex2html_wrap_inline3371}%
$(d,d')
    \in V$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\tau(i,0) = w_i$
\lthtmlinlinemathA{tex2html_wrap_inline3373}%
$\tau(i,0) = w_i$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$0\leq i < n$
\lthtmlinlinemathA{tex2html_wrap_inline3375}%
$0\leq i < n$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mbox{$\bullet$}$
\lthtmlinlinemathA{tex2html_wrap_inline318}%
$\mbox{$\bullet$}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$S(n),T(n) \geq 2n$
\lthtmlinlinemathA{tex2html_wrap_inline3381}%
$S(n),T(n) \geq 2n$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\Sigma$
\lthtmlinlinemathA{tex2html_wrap_inline3385}%
$\Sigma$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$x \in \Sigma^*$
\lthtmlinlinemathA{tex2html_wrap_inline3389}%
$x \in \Sigma^*$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$w \in D^*$
\lthtmlinlinemathA{tex2html_wrap_inline3391}%
$w \in D^*$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$s\geq s_0+2, t\geq t_0     +2$
\lthtmlinlinemathA{tex2html_wrap_inline3409}%
$s\geq s_0+2, t\geq t_0
    +2$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$s,t \geq 2$
\lthtmlinlinemathA{tex2html_wrap_inline3421}%
$s,t \geq 2$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{L}(M)$
\lthtmlinlinemathA{tex2html_wrap_inline3439}%
$\mathcal{L}(M)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{trans}$
\lthtmlinlinemathA{tex2html_wrap_inline3445}%
$\textit{trans}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$v \in \Sigma^*$
\lthtmlinlinemathA{tex2html_wrap_inline3451}%
$v \in \Sigma^*$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$v \in   \mathcal{L}(M)$
\lthtmlinlinemathA{tex2html_wrap_inline3455}%
$v \in
  \mathcal{L}(M)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{trans}(v)$
\lthtmlinlinemathA{tex2html_wrap_inline3467}%
$\textit{trans}(v)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
% contents=$\mathbb{Z} _{2^n} \times \mathbb{Z} _{2^n}$
\lthtmlinlinemathA{tex2html_wrap_inline3469}%
$\mathbb{Z} _{2^n}
\times \mathbb{Z} _{2^n}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$X_0,\dots,X_{n-1}$
\lthtmlinlinemathA{tex2html_wrap_inline3473}%
$X_0,\dots,X_{n-1}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$Y_0,\dots,Y_{n-1}$
\lthtmlinlinemathA{tex2html_wrap_inline3475}%
$Y_0,\dots,Y_{n-1}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$a \in \Delta^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3487}%
$a \in \Delta^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a)$
\lthtmlinlinemathA{tex2html_wrap_inline3489}%
$\textit{pos}\xspace(a)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{gather*}\textit{pos}\xspace(a) := (\textit{xpos}(a), \textit{ypos}(a)) := \biggl( \sum_{i = 0}^{n-1} x_i \cdot 2^i, \quad \sum_{i =     0}^{n-1} y_i \cdot 2^i \biggr) \; , \; \text{where}\\\beg...}
\lthtmlfigureA{gatherstar363}%
\begin{gather*}\textit{pos}\xspace(a) := (\textit{xpos}(a), \textit{ypos}(a)) := \biggl( \sum_{i = 0}^{n-1} x_i \cdot 2^i, \quad \sum_{i =
    0}^{n-1} y_i \cdot 2^i \biggr) \; , \; \text{where}\\
  \begin{array}{c@{\qquad}c}
    x_i = 
    \begin{cases}
      0, & \text{if $a \not\in X_i^\mathcal{I}$ } \\
      1, & \text{otherwise}
    \end{cases} &
    y_i = 
    \begin{cases}
      0, & \text{if $a \not\in Y_i^\mathcal{I}$ } \\
      1, & \text{otherwise} \ .
    \end{cases}
  \end{array} 
\end{gather*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}x = \sum_{i=0}^{n-1} x_i \cdot 2^i \quad \text{and} \quad x' =   \sum_{i=0}^{n-1} x'_i \cdot 2^i .   \end{displaymath}
\lthtmldisplayA{displaymath2690}%
\begin{displaymath}x = \sum_{i=0}^{n-1} x_i \cdot 2^i \quad \text{and} \quad x' =
  \sum_{i=0}^{n-1} x'_i \cdot 2^i .
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{multline*}\begin{split}       x' \equiv x+1 \pmod{2^n} \quad \text{iff} \quad & \bigwedge_{k=0}^{n-1}       (\bigwedge_{j=0}^{k-1} x_j = 1) \rightarrow (x_k = 1 \leftrightarrow x'_k = 0) \\\wed...}
\lthtmlfigureA{multlinestar390}%
\begin{multline*}\begin{split}
      x' \equiv x+1 \pmod{2^n} \quad \text{iff} \quad & \bigwedge_{k=0}^{n-1}
      (\bigwedge_{j=0}^{k-1} x_j = 1) \rightarrow (x_k = 1 \leftrightarrow x'_k = 0) \\
      \wedge & \bigwedge_{k=0}^{n-1} (\bigvee_{j=0}^{k-1} x_j = 0) \rightarrow
      (x_k = x'_k) \; ,
    \end{split}
  \end{multline*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{figure}\begin{center}     \framebox[\textwidth]{       $       \begin{array}{r@{\;}c@{\;}ll}         T_n & = \bigl \{  & (\forall \ \exists {{\textit{east}}\xspace} . \top), & (\forall \       ...}
\lthtmlfigureA{figure409}%
\begin{figure}\begin{center}
    \framebox[\textwidth]{
      $
      \begin{array}{r@{\;}c@{\;}ll}
        T_n & = \bigl \{  & (\forall \ \exists {{\textit{east}}\xspace} . \top), & (\forall \
        \exists {{\textit{north}}\xspace} . \top), \\
        && (\forall \ (= 1 \; {\textit{east}}\xspace^{-1} \; \top)), &   (\forall \ (= 1 \;
        {\textit{north}}\xspace^{-1} \; \top)),\\
        && (\geqslant 1 \; C_{(0,0)}), &  (\geqslant 1 \; C_{(2^n-1,2^n-1)}),\\
        && (\leqslant 1 \; C_{(2^n-1,2^n-1)}), & (\forall \ D_{\textit{east}}\xspace\sqcap
        D_{\textit{north}}\xspace) \ \bigr \}\\[1ex]
        C_{(0,0)}  & = & \underset{k=0}{\overset{n-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}} \neg X_k \sqcap
        \underset{k=0}{\overset{n-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}} \neg Y_k\\[1ex]
        C_{(2^n-1,2^n-1)} & = & \underset{k=0}{\overset{n-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}} X_k \sqcap
        \underset{k=0}{\overset{n-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}} Y_k\\[1ex]
        D_{\textit{east}}\xspace& = & \multicolumn{2}{@{}l}{\underset{k=0}{\overset{n-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}} (
          \underset{j=0}{\overset{k-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}} X_j) \rightarrow ((X_k \rightarrow
          \forall {\textit{east}}\xspace. \neg X_k) \sqcap (\neg X_k \rightarrow \forall
          {\textit{east}}\xspace.X_k)) \; \sqcap}\\
        && \multicolumn{2}{@{}l}{\underset{k=0}{\overset{n-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}} (
          \underset{j=0}{\overset{k-1}{\displaystyle \bigsqcup}} \neg X_j) \rightarrow ((X_k
          \rightarrow \forall {\textit{east}}\xspace.X_k) \sqcap (\neg X_k \rightarrow \forall {\textit{east}}\xspace.
          \neg X_k)) \; \sqcap}\\
        && \multicolumn{2}{@{}l}{\underset{k=0}{\overset{n-1}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}}((Y_k \rightarrow \forall 
          {\textit{east}}\xspace. Y_k) \sqcap (\neg Y_k \rightarrow \forall {\textit{east}}\xspace.\neg Y_k))}\\
        D_{\textit{north}}\xspace& = & \dots
      \end{array}
      $       }   \end{center}
  \end{figure}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a) = (0,0)$
\lthtmlinlinemathA{tex2html_wrap_inline3521}%
$\textit{pos}\xspace(a)
= (0,0)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a) = (2^n-1, 2^n-1)$
\lthtmlinlinemathA{tex2html_wrap_inline3527}%
$\textit{pos}\xspace(a) = (2^n-1, 2^n-1)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$D_{\textit{north}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3529}%
$D_{\textit{north}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$D_{\textit{east}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3531}%
$D_{\textit{east}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=${\textit{north}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3533}%
${\textit{north}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=${\textit{east}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3535}%
${\textit{east}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{xpos}$
\lthtmlinlinemathA{tex2html_wrap_inline3549}%
$\textit{xpos}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{ypos}$
\lthtmlinlinemathA{tex2html_wrap_inline3551}%
$\textit{ypos}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3557}%
$\textit{pos}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$D_{\textit{east}}\xspace, D_{\textit{north}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3561}%
$D_{\textit{east}}\xspace, D_{\textit{north}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$a,b \in \Delta^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3563}%
$a,b \in \Delta^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{gather*}\begin{array}{lll}       \text{$(a,b) \in {\textit{east}}\xspace^\mathcal{I}$\space and $a \in D_{\textit{east}}\xspace^\mathcal{I}$\space implies:} \quad &       \textit{xpos}(b) & \eq...}
\lthtmlfigureA{gatherstar470}%
\begin{gather*}\begin{array}{lll}
      \text{$(a,b) \in {\textit{east}}\xspace^\mathcal{I}$\space and $a \in D_{\textit{east}}\xspace^\mathcal{I}$\space implies:} \quad &
      \textit{xpos}(b) & \equiv \textit{xpos}(a)+1 \pmod{2^n} \\
      & \textit{ypos}(b) & = \textit{ypos}(a)
    \end{array}\\
    \begin{array}{lll}
      \text{$(a,b) \in {\textit{north}}\xspace^\mathcal{I}$\space and $a \in D_{\textit{north}}\xspace^\mathcal{I}$\space implies:} \quad &
      \textit{xpos}(b) & =  \textit{xpos}(a) \\
      & \textit{ypos}(b) & \equiv \textit{ypos}(a) +1 \pmod{2^n}
    \end{array}
  \end{gather*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}(\Delta^\mathcal{I},{\textit{east}}\xspace^\mathcal{I},{\textit{north}}\xspace^\mathcal{I}) \cong (U(2^n,2^n),S_1,S_2) \; ,   \end{displaymath}
\lthtmldisplayA{displaymath2691}%
\begin{displaymath}(\Delta^\mathcal{I},{\textit{east}}\xspace^\mathcal{I},{\textit{north}}\xspace^\mathcal{I}) \cong (U(2^n,2^n),S_1,S_2) \; ,
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\ensuremath{\Delta^\mathcal{I}} $
\lthtmlinlinemathA{tex2html_wrap_inline3587}%
$\ensuremath{\Delta^\mathcal{I}} $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}d(a) = (2^n-1 - \textit{xpos}(a)) + (2^n-1 - \textit{ypos}(a)) .   \end{displaymath}
\lthtmldisplayA{displaymath2692}%
\begin{displaymath}d(a) = (2^n-1 - \textit{xpos}(a)) + (2^n-1 - \textit{ypos}(a)) .
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a) = \textit{pos}\xspace(b)$
\lthtmlinlinemathA{tex2html_wrap_inline3605}%
$\textit{pos}\xspace(a) = \textit{pos}\xspace(b)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models   (\leqslant 1 \; C_{(2^n-1,2^n-1)})$
\lthtmlinlinemathA{tex2html_wrap_inline3609}%
$\mathcal{I}\models
  (\leqslant 1 \; C_{(2^n-1,2^n-1)})$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{xpos}(a) < 2^n-1$
\lthtmlinlinemathA{tex2html_wrap_inline3625}%
$\textit{xpos}(a) < 2^n-1$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{ypos}(a) < 2^n-1$
\lthtmlinlinemathA{tex2html_wrap_inline3627}%
$\textit{ypos}(a) < 2^n-1$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models T_n$
\lthtmlinlinemathA{tex2html_wrap_inline3631}%
$\mathcal{I}\models T_n$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$a,b \in (\exists   {\textit{east}}\xspace.\top)^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3633}%
$a,b \in (\exists
  {\textit{east}}\xspace.\top)^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(a,a_1) \in {\textit{east}}\xspace^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3637}%
$(a,a_1) \in {\textit{east}}\xspace^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(b,b_1) \in {\textit{east}}\xspace^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3639}%
$(b,b_1) \in {\textit{east}}\xspace^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a_1) =    \textit{pos}\xspace(b_1)$
\lthtmlinlinemathA{tex2html_wrap_inline3643}%
$\textit{pos}\xspace(a_1) = 
  \textit{pos}\xspace(b_1)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{align*}\textit{xpos}(a_1) & \equiv \textit{xpos}(b_1) \equiv \textit{xpos}(a) + 1 \pmod{2^n} \\\textit{ypos}(a_1) & = \textit{ypos}(b_1) = \textit{ypos}(a)   \end{align*}
\lthtmlfigureA{alignstar493}%
\begin{align*}\textit{xpos}(a_1) & \equiv \textit{xpos}(b_1) \equiv \textit{xpos}(a) + 1 \pmod{2^n} \\
    \textit{ypos}(a_1) & = \textit{ypos}(b_1) = \textit{ypos}(a)
  \end{align*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$a_1 \in (=1 \ {\textit{east}}\xspace^{-1}.\top)^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3649}%
$a_1 \in (=1 \ {\textit{east}}\xspace^{-1}.\top)^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\{(a,a_1), (b,a_1) \} \subseteq {\textit{east}}\xspace^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3651}%
$\{(a,a_1), (b,a_1) \} \subseteq {\textit{east}}\xspace^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(x,y) \in U(2^n,2^n)$
\lthtmlinlinemathA{tex2html_wrap_inline3657}%
$(x,y) \in U(2^n,2^n)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a) = (x,y)$
\lthtmlinlinemathA{tex2html_wrap_inline3663}%
$\textit{pos}\xspace(a) = (x,y)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models (\geqslant 1 \; C_{(0,0)})$
\lthtmlinlinemathA{tex2html_wrap_inline3669}%
$\mathcal{I}\models (\geqslant 1 \; C_{(0,0)})$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(x-1,y) \in U(2^n,2^n)$
\lthtmlinlinemathA{tex2html_wrap_inline3685}%
$(x-1,y) \in U(2^n,2^n)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a) = (x-1,y)$
\lthtmlinlinemathA{tex2html_wrap_inline3691}%
$\textit{pos}\xspace(a) = (x-1,y)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{pos}\xspace(a_1) =   (x,y)$
\lthtmlinlinemathA{tex2html_wrap_inline3697}%
$\textit{pos}\xspace(a_1) =
  (x,y)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\leqslant (2^n \cdot 2^n) \ \top)$
\lthtmlinlinemathA{tex2html_wrap_inline3703}%
$(\leqslant (2^n \cdot 2^n) \ \top)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
% contents=$\mathcal{D} = (D,V,H)$
\lthtmlinlinemathA{tex2html_wrap_inline3713}%
$\mathcal{D} = (D,V,H)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$w = w_0 \dots w_{n-1} \in   D^*$
\lthtmlinlinemathA{tex2html_wrap_inline3715}%
$w = w_0 \dots w_{n-1} \in
  D^*$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$T(n,\mathcal{D},w)$
\lthtmlinlinemathA{tex2html_wrap_inline3717}%
$T(n,\mathcal{D},w)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$T(n,\mathcal{D},w):= T_n\cup T_\mathcal{D} \cup T_w $
\lthtmlinlinemathA{tex2html_wrap_inline3731}%
$T(n,\mathcal{D},w):= T_n\cup T_\mathcal{D} \cup T_w $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$T_\mathcal{D}$
\lthtmlinlinemathA{tex2html_wrap_inline3735}%
$T_\mathcal{D}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$d \in D$
\lthtmlinlinemathA{tex2html_wrap_inline3743}%
$d \in D$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{gather*}(\forall \ \underset{d \in D}{\bigsqcup} C_d), \quad     (\forall \ \underset{d \in D}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}\ \ \underset{d' \in      ...}
\lthtmlfigureA{gatherstar522}%
\begin{gather*}(\forall \ \underset{d \in D}{\bigsqcup} C_d), \quad
    (\forall \ \underset{d \in D}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}\ \ \underset{d' \in
      D\setminus\{d\}}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}\neg (C_d \sqcap C_{d'})),\\
    (\forall \ \underset{d \in D}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}} (C_d \rightarrow (\forall
    {\textit{east}}\xspace. \underset{(d,d') \in H}{\bigsqcup} C_{d'}))), \quad
    (\forall \ \underset{d \in D}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}} (C_d \rightarrow (\forall {\textit{north}}\xspace.
    \underset{(d,d') \in V}{\bigsqcup} C_{d'}))).
  \end{gather*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{T}_w$
\lthtmlinlinemathA{tex2html_wrap_inline3755}%
$\mathcal{T}_w$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}(\forall \ (C_{(0,0)}  \rightarrow C_{w_0})), \dots,    (\forall \ (C_{(n-1,0)} \rightarrow C_{w_{n-1}}) ,   \end{displaymath}
\lthtmldisplayA{displaymath2694}%
\begin{displaymath}(\forall \ (C_{(0,0)}  \rightarrow C_{w_0})), \dots, 
  (\forall \ (C_{(n-1,0)} \rightarrow C_{w_{n-1}}) ,
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3779}%
$\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{CIN}$
\lthtmlinlinemathA{tex2html_wrap_inline3783}%
$\mathcal{CIN}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{T_{\text{gci}}}
\lthtmlinlinemathA{tex2html_wrap_inline2947}%
\ensuremath{T_{\text{gci}}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
% contents=$o \in N_I$
\lthtmlinlinemathA{tex2html_wrap_inline3791}%
$o \in N_I$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C \sqsubseteq D$
\lthtmlinlinemathA{tex2html_wrap_inline3795}%
$C \sqsubseteq D$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}
\lthtmlinlinemathA{tex2html_wrap_inline2963}%
\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$ o^\mathcal{I}\subseteq \Delta^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3803}%
$ o^\mathcal{I}\subseteq \Delta^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$o^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3807}%
$o^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$o_1 \neq o_2$
\lthtmlinlinemathA{tex2html_wrap_inline3809}%
$o_1 \neq o_2$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$o_1^\mathcal{I}\neq o_2^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3811}%
$o_1^\mathcal{I}\neq o_2^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C^\mathcal{I}   \subseteq D^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3817}%
$C^\mathcal{I}
  \subseteq D^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\ensuremath{T_{\text{gci}}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3819}%
$\ensuremath{T_{\text{gci}}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models \ensuremath{T_{\text{gci}}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3827}%
$\mathcal{I}\models \ensuremath{T_{\text{gci}}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3829}%
$\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline3831}%
$\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}}
\lthtmlinlinemathA{tex2html_wrap_inline2997}%
\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}}%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
% contents=$\{(\leqslant 1 \; C), (\geqslant 1 \; C) \}$
\lthtmlinlinemathA{tex2html_wrap_inline3837}%
$\{(\leqslant 1 \; C), (\geqslant 1 \; C) \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$T = \{ (\bowtie_1 n_1 \; C_1), \dots (\bowtie_k n_k \; C_k) \}$
\lthtmlinlinemathA{tex2html_wrap_inline3841}%
$T = \{ (\bowtie_1 n_1 \; C_1), \dots (\bowtie_k n_k \; C_k) \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\geqslant 0 \; C)$
\lthtmlinlinemathA{tex2html_wrap_inline3845}%
$(\geqslant 0 \; C)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\Phi(T)$
\lthtmlinlinemathA{tex2html_wrap_inline3849}%
$\Phi(T)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}\Phi(T) = \bigcup \{ \Phi(\bowtie_i n_i \; C_i) \mid 1 \leq i \leq k \} ,    \end{displaymath}
\lthtmldisplayA{displaymath2695}%
\begin{displaymath}\Phi(T) = \bigcup \{ \Phi(\bowtie_i n_i \; C_i) \mid 1 \leq i \leq k \} , 
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\Phi(\bowtie_i n_i \; C_i)$
\lthtmlinlinemathA{tex2html_wrap_inline3851}%
$\Phi(\bowtie_i n_i \; C_i)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\bowtie_i = \leqslant$
\lthtmlinlinemathA{tex2html_wrap_inline3853}%
$\bowtie_i = \leqslant$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\bowtie_i = \geqslant$
\lthtmlinlinemathA{tex2html_wrap_inline3855}%
$\bowtie_i = \geqslant$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}\Phi(\bowtie_i n_i \; C_i) =    \begin{cases}     \{ C_i \sqsubseteq o_i^1 \sqcup \dots \sqcup o_i^{n_i} \} & \text{if }     \bowtie_i = \leqslant \\\{ o_i^j \sqsubseteq C_i \mid 1 ...}
\lthtmldisplayA{displaymath2696}%
\begin{displaymath}\Phi(\bowtie_i n_i \; C_i) = 
  \begin{cases}
    \{ C_i \sqsubseteq o_i^1 \sqcup \dots \sqcup o_i^{n_i} \} & \text{if }
    \bowtie_i = \leqslant \\
    \{ o_i^j \sqsubseteq C_i \mid 1 \leq j \leq n_i \} \cup \{ o_i^j
    \sqsubseteq \neg o_i^\ell \mid 1 \leq j < \ell \leq n_i \} & \text{if }
    \bowtie_i = \geqslant 
  \end{cases} ,
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$o_i^1, \dots, o_i^{n_i}$
\lthtmlinlinemathA{tex2html_wrap_inline3857}%
$o_i^1, \dots, o_i^{n_i}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\neg \top$
\lthtmlinlinemathA{tex2html_wrap_inline3859}%
$\neg \top$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models   (\bowtie_i n_i \; C_i)$
\lthtmlinlinemathA{tex2html_wrap_inline3877}%
$\mathcal{I}\models
  (\bowtie_i n_i \; C_i)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$1 \leq i \leq k$
\lthtmlinlinemathA{tex2html_wrap_inline3879}%
$1 \leq i \leq k$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}'$
\lthtmlinlinemathA{tex2html_wrap_inline3881}%
$\mathcal{I}'$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\sharp C_i^\mathcal{I}\leq   n_i$
\lthtmlinlinemathA{tex2html_wrap_inline3899}%
$\sharp C_i^\mathcal{I}\leq
  n_i$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C_i \sqsubseteq \neg \top$
\lthtmlinlinemathA{tex2html_wrap_inline3905}%
$C_i \sqsubseteq \neg \top$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(o_i^j)^{\mathcal{I}'}$
\lthtmlinlinemathA{tex2html_wrap_inline3907}%
$(o_i^j)^{\mathcal{I}'}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C_i^\mathcal{I}\subseteq \{ (o_i^j)^{\mathcal{I}'} \mid 1 \leq j \leq n_i \}$
\lthtmlinlinemathA{tex2html_wrap_inline3909}%
$C_i^\mathcal{I}\subseteq \{ (o_i^j)^{\mathcal{I}'} \mid 1 \leq j \leq n_i \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C_i^{\mathcal{I}'} \subseteq (o_i^1)^{\mathcal{I}'} \cup \dots \cup   (o_i^{n_i})^{\mathcal{I}'}$
\lthtmlinlinemathA{tex2html_wrap_inline3911}%
$C_i^{\mathcal{I}'} \subseteq (o_i^1)^{\mathcal{I}'} \cup \dots \cup
  (o_i^{n_i})^{\mathcal{I}'}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}' \models \Phi(\leqslant n_i   \; C_i)$
\lthtmlinlinemathA{tex2html_wrap_inline3913}%
$\mathcal{I}' \models \Phi(\leqslant n_i
  \; C_i)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\sharp C_i^\mathcal{I}\geq n_i$
\lthtmlinlinemathA{tex2html_wrap_inline3921}%
$\sharp C_i^\mathcal{I}\geq n_i$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$x_1, \dots x_{n_i}$
\lthtmlinlinemathA{tex2html_wrap_inline3923}%
$x_1, \dots x_{n_i}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\Delta^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3927}%
$\Delta^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\{ x_1, \dots, x_{n_i} \} \subseteq   C_i^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3929}%
$\{ x_1, \dots, x_{n_i} \} \subseteq
  C_i^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(o_i^j)^{\mathcal{I}'} = \{x_j \}$
\lthtmlinlinemathA{tex2html_wrap_inline3931}%
$(o_i^j)^{\mathcal{I}'} = \{x_j \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}' \models o_i^j   \sqsubseteq \neg o_i^\ell$
\lthtmlinlinemathA{tex2html_wrap_inline3933}%
$\mathcal{I}' \models o_i^j
  \sqsubseteq \neg o_i^\ell$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$1 \leq i < \ell \leq n_i$
\lthtmlinlinemathA{tex2html_wrap_inline3935}%
$1 \leq i < \ell \leq n_i$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$x_j   \in C_i^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3937}%
$x_j
  \in C_i^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}' \models o_i^j \sqsubseteq C_i$
\lthtmlinlinemathA{tex2html_wrap_inline3939}%
$\mathcal{I}' \models o_i^j \sqsubseteq C_i$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}'   \models \Phi(\geqslant n_i \; C_i)$
\lthtmlinlinemathA{tex2html_wrap_inline3941}%
$\mathcal{I}'
  \models \Phi(\geqslant n_i \; C_i)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}' \models \Phi(T)$
\lthtmlinlinemathA{tex2html_wrap_inline3949}%
$\mathcal{I}' \models \Phi(T)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\bowtie_i n_i \; C_i)$
\lthtmlinlinemathA{tex2html_wrap_inline3959}%
$(\bowtie_i n_i \; C_i)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\Phi(\leqslant 0 \;   C_i) = \{ C_i \sqsubseteq \; \neg \top \}$
\lthtmlinlinemathA{tex2html_wrap_inline3967}%
$\Phi(\leqslant 0 \;
  C_i) = \{ C_i \sqsubseteq \; \neg \top \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models \Phi(T)$
\lthtmlinlinemathA{tex2html_wrap_inline3969}%
$\mathcal{I}\models \Phi(T)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C_i^\mathcal{I}= \emptyset$
\lthtmlinlinemathA{tex2html_wrap_inline3971}%
$C_i^\mathcal{I}= \emptyset$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}\models (\leqslant 0 \; C_i)$
\lthtmlinlinemathA{tex2html_wrap_inline3973}%
$\mathcal{I}\models (\leqslant 0 \; C_i)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\{ C_i \sqsubseteq o_i^1   \sqcup \dots \sqcup o_i^{n_i} \} \subseteq \Phi(T)$
\lthtmlinlinemathA{tex2html_wrap_inline3979}%
$\{ C_i \sqsubseteq o_i^1
  \sqcup \dots \sqcup o_i^{n_i} \} \subseteq \Phi(T)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\sharp C_i^\mathcal{I}\leq \sharp (o_i^1 \sqcup \dots \sqcup   o_i^{n_i})^\mathcal{I}\leq n_i$
\lthtmlinlinemathA{tex2html_wrap_inline3983}%
$\sharp C_i^\mathcal{I}\leq \sharp (o_i^1 \sqcup \dots \sqcup
  o_i^{n_i})^\mathcal{I}\leq n_i$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$ \{   o_i^j \sqsubseteq C_i \mid 1 \leq j \leq n_i \} \cup \{ o_i^j \sqsubseteq   \neg o_i^\ell \mid 1 \leq j < \ell \leq n_i \} \subseteq \Phi(T)$
\lthtmlinlinemathA{tex2html_wrap_inline3987}%
$ \{
  o_i^j \sqsubseteq C_i \mid 1 \leq j \leq n_i \} \cup \{ o_i^j \sqsubseteq
  \neg o_i^\ell \mid 1 \leq j < \ell \leq n_i \} \subseteq \Phi(T)$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\{ (o_i^j)^\mathcal{I}\mid 1 \leq j \leq n_i \}   \subseteq C_i^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3989}%
$\{ (o_i^j)^\mathcal{I}\mid 1 \leq j \leq n_i \}
  \subseteq C_i^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$1   \leq j < \ell \leq n_i$
\lthtmlinlinemathA{tex2html_wrap_inline3991}%
$1
  \leq j < \ell \leq n_i$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(o_i^j)^\mathcal{I}\neq (o_i^\ell)^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3993}%
$(o_i^j)^\mathcal{I}\neq (o_i^\ell)^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$n_i = \sharp \bigcup \{ (o_i^j)^\mathcal{I}\mid 1 \leq j \leq n_i \} \leq \sharp   C_i^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline3995}%
$n_i = \sharp \bigcup \{ (o_i^j)^\mathcal{I}\mid 1 \leq j \leq n_i \} \leq \sharp
  C_i^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage\clearpage
% contents=$\mathcal{C\!N\!O}$
\lthtmlinlinemathA{tex2html_wrap_inline4005}%
$\mathcal{C\!N\!O}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
% contents=$\mathcal{C\!I\!O}$
\lthtmlinlinemathA{tex2html_wrap_inline4011}%
$\mathcal{C\!I\!O}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{C\!I\!N\!O}$
\lthtmlinlinemathA{tex2html_wrap_inline4013}%
$\mathcal{C\!I\!N\!O}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textsc{Exp\-Time}\xspace\neq \textsc{NExp\-Time}\xspace$
\lthtmlinlinemathA{tex2html_wrap_inline4015}%
$\textsc{Exp\-Time}\xspace\neq \textsc{NExp\-Time}\xspace$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{paragraph}
{\newpage\clearpage
% contents=$o_1,o_2 \in N_I$
\lthtmlinlinemathA{tex2html_wrap_inline4025}%
$o_1,o_2
\in N_I$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$o_1 \sqsubseteq \neg o_2$
\lthtmlinlinemathA{tex2html_wrap_inline4029}%
$o_1 \sqsubseteq \neg o_2$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}T = \{ o \sqsubseteq \ensuremath{(\leqslant k \; R \; \top)} , \ \top \sqsubseteq \exists R^- . o \} \end{displaymath}
\lthtmldisplayA{displaymath653}%
\begin{displaymath}T = \{ o \sqsubseteq \ensuremath{(\leqslant k \; R \; \top)} , \ \top \sqsubseteq \exists R^- . o \}
\end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{create}$
\lthtmlinlinemathA{tex2html_wrap_inline4049}%
$\textit{create}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}\begin{array}{r@{\;}c@{\;}ll}     T_n & = \bigl \{  & \top \sqsubseteq \exists {{\textit{east}}\xspace} . \top, & \top \sqsubseteq     \exists {{\textit{north}}\xspace} . \top, \\&&...}
\lthtmldisplayA{displaymath2697}%
\begin{displaymath}\begin{array}{r@{\;}c@{\;}ll}
    T_n & = \bigl \{  & \top \sqsubseteq \exists {{\textit{east}}\xspace} . \top, & \top \sqsubseteq
    \exists {{\textit{north}}\xspace} . \top, \\
    && \top \sqsubseteq  (= 1 \; {\textit{east}}\xspace^{-1} \; \top), &   \top \sqsubseteq  (= 1 \;
    {\textit{north}}\xspace^{-1} \; \top),\\
    && \top \sqsubseteq  \exists {\textit{create}} . {C_{(0,0)}}, &  o \;\sqsubseteq
    C_{(2^n-1,2^n-1)},\\
    && C_{(2^n-1,2^n-1)} \sqsubseteq o, & \top \sqsubseteq  D_{\textit{east}}\xspace\sqcap  D_{\textit{north}}\xspace\ \bigr \}
  \end{array}
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{paragraph}
{\newpage\clearpage
% contents=$\{   \top \sqsubseteq C_1, \dots, \top \sqsubseteq C_k \}$
\lthtmlinlinemathA{tex2html_wrap_inline4055}%
$\{
  \top \sqsubseteq C_1, \dots, \top \sqsubseteq C_k \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{spy}$
\lthtmlinlinemathA{tex2html_wrap_inline4057}%
$\textit{spy}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\cdot^{\textit{spy}}$
\lthtmlinlinemathA{tex2html_wrap_inline4061}%
$\cdot^{\textit{spy}}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$A^{\textit{spy}} =   A $
\lthtmlinlinemathA{tex2html_wrap_inline4063}%
$A^{\textit{spy}} =
  A $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$o^{\textit{spy}} = o$
\lthtmlinlinemathA{tex2html_wrap_inline4067}%
$o^{\textit{spy}} = o$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(\neg   C)^{\textit{spy}} = \neg C^{\textit{spy}}$
\lthtmlinlinemathA{tex2html_wrap_inline4071}%
$(\neg
  C)^{\textit{spy}} = \neg C^{\textit{spy}}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$(C_1 \sqcap C_2)^{\textit{spy}} = C_1^{\textit{spy}} \sqcap   C_2^{\textit{spy}}$
\lthtmlinlinemathA{tex2html_wrap_inline4073}%
$(C_1 \sqcap C_2)^{\textit{spy}} = C_1^{\textit{spy}} \sqcap
  C_2^{\textit{spy}}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=${\ensuremath{(\geqslant n \; R \; C)} }^{\textit{spy}} = \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap     C^{\textit{spy}})} $
\lthtmlinlinemathA{tex2html_wrap_inline4075}%
${\ensuremath{(\geqslant n \; R \; C)} }^{\textit{spy}} = \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap
    C^{\textit{spy}})} $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}C_T = i \sqcap \underset{\top \sqsubseteq C \in T}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}} C^{\textit{spy}}     \sqcap \underset{\top \sqsubseteq C ...}
\lthtmldisplayA{displaymath694}%
\begin{displaymath}C_T = i \sqcap \underset{\top \sqsubseteq C \in T}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}} C^{\textit{spy}}
    \sqcap \underset{\top \sqsubseteq C \in T}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}}\forall \textit{spy}. C^{\textit{spy}}
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$a \in   (C_T)^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline4095}%
$a \in
  (C_T)^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$i^\mathcal{I}= \{ a\}$
\lthtmlinlinemathA{tex2html_wrap_inline4097}%
$i^\mathcal{I}= \{ a\}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{displaymath}\Delta^{\mathcal{I}'} = \{ a\} \cup \{ x \in \Delta^\mathcal{I}\mid (a,x) \in \textit{spy}^\mathcal{I}   \}   \end{displaymath}
\lthtmldisplayA{displaymath2698}%
\begin{displaymath}\Delta^{\mathcal{I}'} = \{ a\} \cup \{ x \in \Delta^\mathcal{I}\mid (a,x) \in \textit{spy}^\mathcal{I}
  \}
  \end{displaymath}%
\lthtmldisplayZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\cdot^{\mathcal{I}'} = \cdot^\mathcal{I}|_{\Delta^{\mathcal{I}'}}$
\lthtmlinlinemathA{tex2html_wrap_inline4101}%
$\cdot^{\mathcal{I}'} = \cdot^\mathcal{I}|_{\Delta^{\mathcal{I}'}}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\textsc{Claim 1:}
\lthtmlfigureA{tex2html_wrap4675}%
\textsc{Claim 1:}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$x \in \Delta^{\mathcal{I}'}$
\lthtmlinlinemathA{tex2html_wrap_inline4103}%
$x \in \Delta^{\mathcal{I}'}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$x \in (C^{\textit{spy}})^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline4107}%
$x \in (C^{\textit{spy}})^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$x \in C^{\mathcal{I}'}$
\lthtmlinlinemathA{tex2html_wrap_inline4109}%
$x \in C^{\mathcal{I}'}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C = \ensuremath{(\geqslant n \; R \; D)} $
\lthtmlinlinemathA{tex2html_wrap_inline4113}%
$C = \ensuremath{(\geqslant n \; R \; D)} $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$C^{\textit{spy}} = \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap D^{\textit{spy}})} $
\lthtmlinlinemathA{tex2html_wrap_inline4115}%
$C^{\textit{spy}} = \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap D^{\textit{spy}})} $%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{align*}& x \in \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap D^{\textit{spy}})} ^\mathcal{I}\\\text{iff } \; & \sharp \{ y \in \Delta^\mathcal{I}\mid (x,y) \in R^\mathcal...}
\lthtmlfigureA{alignstar720}%
\begin{align*}& x \in \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap D^{\textit{spy}})} ^\mathcal{I}\\
    \text{iff } \; & \sharp \{ y \in \Delta^\mathcal{I}\mid (x,y) \in R^\mathcal{I}\text{ and } y
    \in (\exists \textit{spy}^-.i)^\mathcal{I}\cap (D^{\textit{spy}})^\mathcal{I}\} \geqslant n\\
    (*) \text{ iff } \; & \sharp \{ y \in \Delta^{\mathcal{I}'} \mid (x,y) \in R^{\mathcal{I}'} \text{
      and } y \in D^{\mathcal{I}'} \} \geqslant n\\
    \text{iff } \; & x \in \ensuremath{(\geqslant n \; R \; D)} ^{\mathcal{I}'} ,
  \end{align*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\top \sqsubseteq C \in T$
\lthtmlinlinemathA{tex2html_wrap_inline4121}%
$\top \sqsubseteq C \in T$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}' \models \top \sqsubseteq C$
\lthtmlinlinemathA{tex2html_wrap_inline4129}%
$\mathcal{I}' \models \top \sqsubseteq C$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$i^{\mathcal{I}'} = \{ a \}$
\lthtmlinlinemathA{tex2html_wrap_inline4141}%
$i^{\mathcal{I}'} = \{ a \}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\textit{spy}^{\mathcal{I}'} = \{   (a,x) \mid x \in \Delta^\mathcal{I}$
\lthtmlinlinemathA{tex2html_wrap_inline4143}%
$\textit{spy}^{\mathcal{I}'} = \{
  (a,x) \mid x \in \Delta^\mathcal{I}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{I}' \models T$
\lthtmlinlinemathA{tex2html_wrap_inline4151}%
$\mathcal{I}' \models T$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\textsc{Claim 2:}
\lthtmlfigureA{tex2html_wrap4681}%
\textsc{Claim 2:}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$x \in (C^{\textit{spy}})^{\mathcal{I}'}$
\lthtmlinlinemathA{tex2html_wrap_inline4163}%
$x \in (C^{\textit{spy}})^{\mathcal{I}'}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\begin{align*}& x \in \ensuremath{(\geqslant n \; R \; D)} ^{\mathcal{I}'}\\\text{iff } \; & \sharp \{ y \in \Delta^{\mathcal{I}'} \mid (x,y) \in R^{\mathcal{I}'}     \text{ and } y \in D^{\mathcal{I}...}
\lthtmlfigureA{alignstar749}%
\begin{align*}& x \in \ensuremath{(\geqslant n \; R \; D)} ^{\mathcal{I}'}\\
    \text{iff } \; & \sharp \{ y \in \Delta^{\mathcal{I}'} \mid (x,y) \in R^{\mathcal{I}'}
    \text{ and } y \in D^{\mathcal{I}'} \} \geqslant n\\
    (*) \text{ iff } \; & \sharp \{ y \in \Delta^{\mathcal{I}'} \mid (x,y) \in R^{\mathcal{I}'},
    (a,y) \in \textit{spy}^{\mathcal{I}'}, \text{ and } y \in (D^{\textit{spy}})^{\mathcal{I}'} \} \geqslant n\\
    \text{iff } \; & x \in \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap
      D^{\textit{spy}})} ^{\mathcal{I}'} .
  \end{align*}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$({{\raisebox{1.3ex}{\begin{turn}{180}$\bigsqcup$\end{turn}}}}_{\top \sqsubseteq C \in T}   C^{\textit{spy}} )^{\mathcal{I}'} = \Delta^{\mathcal{I}'}$
\lthtmlinlinemathA{tex2html_wrap_inline4177}%
$({{\raisebox{1.3ex}{\begin{turn}{180}$\bigsqcup$\end{turn}}}}_{\top \sqsubseteq C \in T}
  C^{\textit{spy}} )^{\mathcal{I}'} = \Delta^{\mathcal{I}'}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$a \in (C_T)^{\mathcal{I}'}$
\lthtmlinlinemathA{tex2html_wrap_inline4179}%
$a \in (C_T)^{\mathcal{I}'}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
% contents=\begin{figure}\begin{center}     \framebox[\textwidth]{       \begin{tabular}{l|cc|cc}         & \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace& \ensuremath{\mathcal{A}\!\mathc...}
\lthtmlfigureA{figure784}%
\begin{figure}\begin{center}
    \framebox[\textwidth]{
      \begin{tabular}{l|cc|cc}
        & \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace& \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}\xspace& \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}\xspace& \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}\xspace\\
      \hline
      Concept Satisfiability & \textsc{PSpace}\xspace-c. & open & \textsc{PSpace}\xspace-c. & \textsc{NExp\-Time}\xspace-c.\\
      GCIs & \textsc{Exp\-Time}\xspace-c. & \textsc{Exp\-Time}\xspace-c. & \textsc{Exp\-Time}\xspace-c. & \textsc{NExp\-Time}\xspace-c.\\
      Cardinality Restr. & \textsc{Exp\-Time}\xspace-c. & \textsc{Exp\-Time}\xspace-c. &
      \textsc{NExp\-Time}\xspace-c. & \textsc{NExp\-Time}\xspace-c.
    \end{tabular}
    }   \end{center}
  \end{figure}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{S\!H\!I\!Q}$
\lthtmlinlinemathA{tex2html_wrap_inline4189}%
$\mathcal{S\!H\!I\!Q}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathcal{D\!L\!R}$
\lthtmlinlinemathA{tex2html_wrap_inline4191}%
$\mathcal{D\!L\!R}$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=$\mathsf{CPDL}_g$
\lthtmlinlinemathA{tex2html_wrap_inline4193}%
$\mathsf{CPDL}_g$%
\lthtmlinlinemathZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\l
\lthtmlfigureA{tex2html_wrap4811}%
\l%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
% contents=\textsc{Kl-One}
\lthtmlfigureA{tex2html_wrap4841}%
\textsc{Kl-One}%
\lthtmlfigureZ
\hfill\lthtmlcheckvsize\clearpage}


\end{document}
