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




\usepackage{amssymb}
\usepackage{curves}
\usepackage{graphicx}
\usepackage{url}
\usepackage{algorithm}



\newtheorem{definition}{Definition} 
\newtheorem{proposition}{Proposition} 
\newtheorem{lemma}{Lemma} 
\newtheorem{theorem}{Theorem} 
\newtheorem{property}{Property} 
%
\providecommand{\theproof}[1]{{\bf Proof: } #1 \hspace*{\fill}$\Box$\  \\\mbox{}


} 

%
\providecommand{\heads}{\mbox{heads}} 

%
\providecommand{\until}{\makebox[1em]{$\mathbin{\mbox{\sf U}}$}}%
\providecommand{\always}{\mbox{$\Box$}}%
\providecommand{\eventually}{\mbox{$\Diamond$}}%
\providecommand{\balways}[1]{\mbox{$\Box_{#1}$}}%
\providecommand{\beventually}[1]{\mbox{$\Diamond_{#1}$}}%
\providecommand{\next}{\raisebox{0.6mm}{$\scriptstyle \bigcirc$}}%
\providecommand{\reward}{\mathbin{\makebox[1em]{\sf R}}}%
\providecommand{\dollar}{\mbox{\$}}%
\providecommand{\valof}[2]{\mbox{$[\,#1\,]_{#2}$}}%
\providecommand{\since}{\mathbin{\mbox{\sf S}}}%
\providecommand{\last}{\circleddash}%
\providecommand{\previously}{\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}}%
\providecommand{\alwaysPast}{\boxminus}%
\providecommand{\xfltl}{\mbox{\mbox{\$}FLTL}}%
\providecommand{\implies}{\rightarrow}%
\providecommand{\xor}{\oplus}%
\providecommand{\true}{\mbox{$\top$}}%
\providecommand{\false}{\mbox{$\bot$}}%
\providecommand{\tail}[1]{{\small\sf tail}(#1)}%
\providecommand{\modelsb}[1]{\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize $#1$}}\:$}}%
\providecommand{\notmodelsb}[1]{\mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize $#1$}}\:$}}%
\providecommand{\restrict}[2]{\mbox{${#1}\Downarrow{#2}$}} 

%
\providecommand{\PP}{{\cal P}}%
\providecommand{\RR}{{\cal R}}%
\providecommand{\II}{{\cal I}}%
\providecommand{\EE}{{\cal E}}%
\providecommand{\FF}{{\cal F}}%
\providecommand{\LL}{{\cal L}}%
\providecommand{\T}{\Pr}%
\providecommand{\TT}[2]{\Pr(#2,#1,\bullet)}%
\providecommand{\TTT}[3]{\Pr(#2,#1,#3)}%
\providecommand{\TP}{\Pr'}%
\providecommand{\TTP}[2]{\Pr'(#2,#1,\bullet)}%
\providecommand{\TTTP}[3]{\Pr'(#2,#1,#3)} 

%
\providecommand{\fut}{\makebox[1em]{$\mathbin{\mbox{\sf U}}$}}%
\providecommand{\fbx}{\mbox{$\Box$}}%
\providecommand{\fdi}{\mbox{$\Diamond$}}%
\providecommand{\nxt}{\raisebox{0.6mm}{$\scriptstyle \bigcirc$}}%
\providecommand{\snc}{\mathbin{\mbox{\sf S}}}%
\providecommand{\prv}{\circleddash } 

%
\providecommand{\E}{E}%
\providecommand{\F}{F}%
\providecommand{\Expect}{\makebox[1em]{$\mathbin{\mbox{\sf E}}$}}%
\providecommand{\real}{\mbox{I$\!$R}}%
\providecommand{\nat}{\mbox{I$\!$N}}%
\providecommand{\wait}{\mbox{\sc null}}%
\providecommand{\size}[1]{||#1||}%
\providecommand{\kwd}[1]{\mbox{\sf #1\/}}%
\providecommand{\Ind}[2]{\makebox[20pt][r]{#1.}~\hspace*{#2em}}%
\providecommand{\Prog}{\mbox{Prog}}%
\providecommand{\MProg}{\mbox{\em Prog}}%
\providecommand{\Reg}{\mbox{Reg}}%
\providecommand{\MReg}{\mbox{\em Reg}}%
\providecommand{\SProg}{\mbox{R}\mbox{Prog}}%
\providecommand{\MSProg}{\mbox{{\em R}\mbox{\em Prog}}}%
\providecommand{\Rew}{\mbox{Rew}}%
\providecommand{\MRew}{\mbox{\em Rew}}%
\providecommand{\Sub}{\mbox{Sub}}%
\providecommand{\MSub}{\mbox{\em Sub}}%
\providecommand{\PTSub}{\mbox{PTSub}}%
\providecommand{\MPTSub}{\mbox{\em PTSub}}%
\providecommand{\NN}[1]{\overline{#1}} 

%
\providecommand{\pltlmin}{{\sc pltlmin}}%
\providecommand{\pltlsimp}{{\sc pltlsim}}%
\providecommand{\pltlstruct}{{\sc pltlstr}}%
\providecommand{\pltlstrauto}{{\sc pltlstr(a)}}%
\providecommand{\fltl}{{\sc fltl}}%
\providecommand{\fltllao}{{\sc fltl}} 

%
\providecommand{\spuddlinear}{{\sc spudd-linear}}%
\providecommand{\spuddexpon}{{\sc spudd-expon}}%
\providecommand{\balls}{{\sc on/off}}%
\providecommand{\complete}{{\sc complete}} 

%
\providecommand{\nmrdpp}{{\sc nmrdpp}}%
\providecommand{\mdpsim}{{\sc mdpsim}}%
\providecommand{\mtbdd}{{\sc mtbdd}} 

%
\providecommand{\nega}{---}%
\providecommand{\none}{} 


\usepackage[dvips]{color}


\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{\dimen0\ht\sizebox \advance\dimen0\dp\sizebox
  \ifdim\dimen0>.95\vsize
   \lthtmltypeout{%
*** image for \lthtmlmathenv\space is too tall at \the\dimen0, reducing to .95 vsize ***}%
   \ht\sizebox.95\vsize \dp\sizebox\z@ \fi
  \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 


\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_inline9408}%
$\tau (s'_0) = \tau (s'_2) = s_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9410}%
$\tau (s'_1) = \tau (s'_3) = s_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9412}%
$s'_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9414}%
$s'_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9420}%
$\circleddash $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3444}%
$S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3446}%
$S^*$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3450}%
$S^\omega$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3456}%
$i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3458}%
$\Gamma_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3464}%
$\Gamma(i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3466}%
$\langle \Gamma_0, \ldots, \Gamma_i \rangle \in S^{*}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3470}%
$\Gamma;\Gamma'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3472}%
$\Gamma\in S^*$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3474}%
$\Gamma' \in S^\omega$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3476}%
$\langle S,s_0,A,\Pr ,R\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3480}%
$s_{0}\in S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3482}%
$A$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3484}%
$A(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3486}%
$s\in S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3488}%
$\{\Pr(s,a,\bullet) \mid s\!\in\!S, a\!\in\!A(s)\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3492}%
$\Pr(s,a,s')$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3494}%
$s'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3498}%
$s$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3502}%
$R: S \mapsto \mbox{I$\!$R}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3504}%
$R(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3508}%
$\pi : S \mapsto A$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3510}%
$\pi(s)\in A(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3514}%
$V_\pi$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3516}%
$s_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3382}%
\begin{displaymath}
V_\pi(s_0) = \lim_{n\rightarrow\infty} \makebox[1em]{$\mathbin{\mbox{\sf E}}$}\bigg{[} 
\sum_{i=0}^{n} \beta^{i} R(\Gamma_i) \mid \pi, \Gamma_{0} = s_{0} \bigg{]}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3520}%
$0 \leq \beta < 1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3522}%
$S^{*}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3528}%
$R(\Gamma(i))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3536}%
$\pi$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3383}%
\begin{displaymath}
V_{\pi}(s_{0}) = \lim_{n\rightarrow\infty} \makebox[1em]{$\mathbin{\mbox{\sf E}}$}\bigg{[} 
\sum_{i=0}^{n} \beta^{i} R(\Gamma(i)) \mid \pi, \Gamma_{0} = s_{0} \bigg{]}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3540}%
$D=\langle S,s_0,A,\Pr ,R\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3544}%
$\widetilde{D}(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3548}%
$D$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3550}%
$\widetilde{D}(s) = \{ \Gamma\in S^\omega \mid \Gamma_0 = s
\mbox{~and~}\forall i~\exists a \in A(\Gamma_i)~~
\Pr(\Gamma_{i},a,\Gamma_{i+1}) > 0 \}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3554}%
$R$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}



\setlength{\unitlength}{5.5mm}%

\setlength{\unitlength}{5.5mm}

%
\providecommand{\astate}[2]{\put(#1){\bigcircle{1}}
                        \put(#1){\makebox(0,0){#2}}}%

{\newpage\clearpage
\lthtmlfigureA{figure284}%
\begin{figure}\centering
\begin{picture}(0,8)(0,-4)
%
\put(-8.4,0){\begin{picture}(0,0)(0,0)
\put(0,3){\bigcircle{1}}
                        \put(0,3){\makebox(0,0){{\footnotesize$s_0$}}}
\put(0,-1){\bigcircle{1}}
                        \put(0,-1){\makebox(0,0){{\footnotesize$s_1$}}}
%
\put(0,-0.5){\vector(0,1){3}}
\put(-0.3,1){\makebox(0,0){{\footnotesize$d$}}}
\put(0.5,1){\makebox(0,0){{\footnotesize 1.0}}}
%
\put(0.354,2.646){\line(1,-1){0.646}}
\put(-0.25,0.75){\arc(1.25,1.25){-110}} \put(0.48,-0.87){\vector(-4,-3){0}}
\put(2.81,2.75){\line(0,1){0.5}}
\put(1.75,2.75){\arc(-0.75,-0.75){135}}
\put(1.75,3.25){\arc(-0.75,0.75){-135}}
\put(1,4){\vector(-1,-1){0.646}}
\put(-1,2.5){\makebox(0,0){{\footnotesize$a$}}}
\put(-2,0.5){\makebox(0,0){{\footnotesize0.1}}}
\put(-2.5,1.5){\makebox(0,0){{\footnotesize0.9}}}
%
\put(-0.354,2.646){\line(-1,-1){0.646}}
\put(0.25,0.75){\arc(-1.25,1.25){110}} \put(-0.48,-0.87){\vector(4,-3){0}}
\put(-2.81,2.75){\line(0,1){0.5}}
\put(-1.75,2.75){\arc(0.75,-0.75){-135}}
\put(-1.75,3.25){\arc(0.75,0.75){135}}
\put(-1,4){\vector(1,-1){0.646}}
\put(1,2.5){\makebox(0,0){{\footnotesize$b$}}}
\put(2,0.5){\makebox(0,0){{\footnotesize0.5}}}
\put(2.5,1.5){\makebox(0,0){{\footnotesize0.5}}}
%
\put(-0.354,-1.354){\line(-1,-1){0.646}}
\put(1,-2){\vector(-1,1){0.646}}
\put(-0.5,-3.2125){\line(1,0){1}}
\put(-0.5,-2.5){\arc(-0.5,0.5){135}}
\put(0.5,-2.5){\arc(0.5,0.5){-135}}
\put(-1,-1.5){\makebox(0,0){{\footnotesize$c$}}}
\put(0,-2.8){\makebox(0,0){{\footnotesize 1.0}}}
\end{picture}}
\put(-0.8,4){
\parbox[t]{0.52\textwidth}{\footnotesize
  In the initial state $s_0$, $p$\  is false and two actions are possible: $a$
  causes a transition to $s_1$\  with probability 0.1, and no change with
  probability 0.9, while for $b$\  the transition probabilities are 0.5. In
  state $s_1$, $p$\  is true, and actions $c$\  and $d$\  (``stay'' and ``go'') lead
  to $s_1$\  and $s_0$\  respectively with probability 1.
\par
A reward is received the first time $p$\  is true, but not
  subsequently. That is, the rewarded state sequences are:\\
  \hspace*{2em} $\langle s_0,s_1 \rangle$\  \\
  \hspace*{2em} $\langle s_0,s_0,s_1 \rangle$\  \\
  \hspace*{2em} $\langle s_0,s_0,s_0,s_1 \rangle$\  \\
  \hspace*{2em} $\langle s_0,s_0,s_0,s_0,s_1 \rangle$
  \hspace*{1em} etc.
}}
\end{picture}
\par

\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3600}%
$g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3606}%
$D'\!\!=\!\!\langle S',s'_{0},A',\Pr'\!,R'\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3608}%
$D=\langle S,s_{0},A,\Pr ,R\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3610}%
$\tau : S' \mapsto S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3614}%
$A'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3620}%
$\tau(s'_{0}) = s_{0}.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3622}%
$s' \in S'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3624}%
$A'(s')= A(\tau(s'))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3626}%
$s_1,s_2\in S$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3628}%
$a\in A(s_1)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3630}%
$\Pr(s_1,a,s_2) > 0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3632}%
$s_1'\in S'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3634}%
$\tau(s_1')= s_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3636}%
$s_2' \in S'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3638}%
$\tau(s'_2) = s_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3640}%
$a'\in A'(s'_1)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3642}%
$\Pr'(s'_1,a',s'_2)\!=\!\Pr(s_1,a',s_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3644}%
$\Gamma \in \widetilde{D}(s_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3646}%
$\Gamma' \in \widetilde{D}'(s'_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3648}%
$\tau(\Gamma'_{i}) =
\Gamma_{i}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3652}%
$R'(\Gamma'_{i}) = R(\Gamma(i))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3658}%
$D'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3660}%
$\pi'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3666}%
$\Gamma(i)\in \widetilde{D}(s_{0})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3668}%
$\pi(\Gamma(i)) = \pi'(\Gamma'_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3670}%
$j\leq i~\tau(\Gamma'_{j})=\Gamma_{j}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3676}%
$V_{\pi}(s_0) = V_{\pi'}(s'_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{figure375}%
\begin{figure}\centering
\begin{picture}(0,9.5)(0,-4.5)
%
\put(2,-1){\begin{picture}(0,0)(0,0)
\put(3,0){\bigcircle{1}}
                        \put(3,0){\makebox(0,0){{\footnotesize$s'_0$}}}
\put(-1,0){\bigcircle{1}}
                        \put(-1,0){\makebox(0,0){{\footnotesize$s'_1$}}}
%
\put(2.646,0.354){\line(-1,1){0.646}}
\put(0.75,-0.25){\arc(1.25,1.25){110}} \put(-0.87,0.48){\vector(-3,-4){0}}
\put(2.75,2.81){\line(1,0){0.5}}
\put(2.75,1.75){\arc(-0.75,-0.75){-135}}
\put(3.25,1.75){\arc(0.75,-0.75){135}}
\put(4,1){\vector(-1,-1){0.646}}
\put(2.5,-1){\makebox(0,0){{\footnotesize$a$}}}
\put(0.5,-2){\makebox(0,0){{\footnotesize0.1}}}
\put(1.5,-2.5){\makebox(0,0){{\footnotesize0.9}}}
%
\put(2.646,-0.354){\line(-1,-1){0.646}}
\put(0.75,0.25){\arc(1.25,-1.25){-110}} \put(-0.87,-0.48){\vector(-3,4){0}}
\put(2.75,-2.81){\line(1,0){0.5}}
\put(2.75,-1.75){\arc(-0.75,0.75){135}}
\put(3.25,-1.75){\arc(0.75,0.75){-135}}
\put(4,-1){\vector(-1,1){0.646}}
\put(2.5,1){\makebox(0,0){{\footnotesize$b$}}}
\put(0.5,2){\makebox(0,0){{\footnotesize0.5}}}
\put(1.5,2.5){\makebox(0,0){{\footnotesize0.5}}}
%
\put(-1.5,0){\vector(-1,0){3.5}}
\put(-2,-0.3){\makebox(0,0){{\footnotesize$c$}}}
\put(-1.3,1.5){\makebox(0,0){{\footnotesize$d$}}}
%
\end{picture}}
\par
\put(-1.25,4){\oval(4.5,2)[t]}
\put(-3.5,4){\vector(0,-1){0.5}}
\put(1,-0.5){\line(0,1){4.5}}
\par
\put(-3.5,0){\begin{picture}(0,0)(0,0)
\put(0,3){\bigcircle{1}}
                        \put(0,3){\makebox(0,0){{\footnotesize$s'_2$}}}
\put(0,-1){\bigcircle{1}}
                        \put(0,-1){\makebox(0,0){{\footnotesize$s'_3$}}}
%
\put(0,-0.5){\vector(0,1){3}}
\put(-0.3,1){\makebox(0,0){{\footnotesize$d$}}}
\put(0.5,1){\makebox(0,0){{\footnotesize 1.0}}}
%
\put(0.354,2.646){\line(1,-1){0.646}}
\put(-0.25,0.75){\arc(1.25,1.25){-110}} \put(0.48,-0.87){\vector(-4,-3){0}}
\put(2.81,2.75){\line(0,1){0.5}}
\put(1.75,2.75){\arc(-0.75,-0.75){135}}
\put(1.75,3.25){\arc(-0.75,0.75){-135}}
\put(1,4){\vector(-1,-1){0.646}}
\put(-1,2.5){\makebox(0,0){{\footnotesize$a$}}}
\put(-2,0.5){\makebox(0,0){{\footnotesize0.1}}}
\put(-2.5,1.5){\makebox(0,0){{\footnotesize0.9}}}
%
\put(-0.354,2.646){\line(-1,-1){0.646}}
\put(0.25,0.75){\arc(-1.25,1.25){110}} \put(-0.48,-0.87){\vector(4,-3){0}}
\put(-2.81,2.75){\line(0,1){0.5}}
\put(-1.75,2.75){\arc(0.75,-0.75){-135}}
\put(-1.75,3.25){\arc(0.75,0.75){135}}
\put(-1,4){\vector(1,-1){0.646}}
\put(1,2.5){\makebox(0,0){{\footnotesize$b$}}}
\put(2,0.5){\makebox(0,0){{\footnotesize0.5}}}
\put(2.5,1.5){\makebox(0,0){{\footnotesize0.5}}}
%
\put(-0.354,-1.354){\line(-1,-1){0.646}}
\put(1,-2){\vector(-1,1){0.646}}
\put(-0.5,-3.2125){\line(1,0){1}}
\put(-0.5,-2.5){\arc(-0.5,0.5){135}}
\put(0.5,-2.5){\arc(0.5,0.5){-135}}
\put(-1.2,-1.8){\makebox(0,0){{\footnotesize$c$}}}
\put(0,-2.8){\makebox(0,0){{\footnotesize 1.0}}}
%
\end{picture}}
\end{picture}
\par

\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3712}%
$\mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3716}%
$\mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3720}%
$\mathbin{\mbox{\sf S}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3726}%
$\circleddash f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3730}%
$f_1 \mathbin{\mbox{\sf S}}f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3732}%
$f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3734}%
$f_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3736}%
$\models$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3742}%
$\Gamma(i) \models p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3744}%
$p\in\Gamma_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3746}%
$p\in {\cal P}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3748}%
$\Gamma(i) \models \neg f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3750}%
$\Gamma(i)\not\models f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3752}%
$\Gamma(i) \models f_1 \wedge f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3754}%
$\Gamma(i) \models f_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3756}%
$\Gamma(i) \models f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3758}%
$\Gamma(i) \models \circleddash f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3760}%
$i > 0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3762}%
$\Gamma(i-1)
\models f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3764}%
$\Gamma(i) \models f_1 \mathbin{\mbox{\sf S}}f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3766}%
$\exists
j \leq i, \Gamma(j) \models f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3768}%
$\forall k, j<k\leq i,
\Gamma(k) \models f_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3776}%
$\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}f
\equiv \mbox{$\top$}\mathbin{\mbox{\sf S}}f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3782}%
$\boxminus f \equiv \neg\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}\neg f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3788}%
$g \wedge \neg\circleddash \makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3792}%
$\circleddash ^k$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3794}%
$k$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3802}%
$\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}_k f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3804}%
$\vee_{i=1}^{k} \circleddash ^i f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3810}%
$\boxminus _k f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3812}%
$\wedge_{i=1}^{k}
\circleddash ^i f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3818}%
$(f_i
: r_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3820}%
$f_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3822}%
$r_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3830}%
$F$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3836}%
$(f: r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3838}%
$r$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3844}%
$(\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}f : r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3850}%
$(f \wedge \neg\circleddash \makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}f: r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3854}%
$(f \wedge \boxminus _k
\neg f: r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3862}%
$(\circleddash ^n \neg \circleddash \mbox{$\bot$}: r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3864}%
$n^{\mbox{th}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3866}%
$(\circleddash ^2 f_1 \wedge \circleddash 
f_2 \wedge f_3 :r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3872}%
$f_3$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3876}%
$c$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3880}%
$(f \wedge \makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}c: r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3884}%
$(f \wedge \circleddash (\neg
f \mathbin{\mbox{\sf S}}c) : r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3894}%
$(f \wedge \makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}_k c : r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3898}%
$(pp)*$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3902}%
$p^nq^n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3906}%
$\mbox{$f_1 \mathbin{\mbox{\sf S}}f_2$} \equiv
f_2 \vee (f_1 \wedge \circleddash (f_1 \mathbin{\mbox{\sf S}}f_2))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3912}%
$\Gamma(i-1)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3918}%
$||f||$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3920}%
$||F||$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3926}%
${\cal O}(||f||)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3928}%
$\mbox{Reg}(f,s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3940}%
$\Gamma_i =s$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3950}%
$\mbox{Reg}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3954}%
$\mbox{Reg}(p,s) = \mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3956}%
$p\in s$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3964}%
$\mbox{Reg}(\neg f,s)= \neg\mbox{Reg}(f,s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3966}%
$\mbox{Reg}(f_1 \wedge f_2,s) = \mbox{Reg}(f_1,s) \wedge \mbox{Reg}(f_2,s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3968}%
$\mbox{Reg}(\circleddash f,s) = f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3970}%
$\mbox{Reg}(f_1 \mathbin{\mbox{\sf S}}f_2,s) = \mbox{Reg}(f_2,s) \vee (\mbox{Reg}(f_1,s)
\wedge (f_1 \mathbin{\mbox{\sf S}}f_2))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3976}%
$q$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3978}%
$f = (\circleddash \neg q) \wedge (p \mathbin{\mbox{\sf S}}q)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3986}%
$\mbox{Reg}(f,s) = \neg q \wedge (p \mathbin{\mbox{\sf S}}q)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline3992}%
$p \mathbin{\mbox{\sf S}}
q$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4002}%
$\mbox{Reg}(f,s) = \mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4006}%
$X$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4008}%
$\overline{X}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4010}%
$X \cup \{\neg x \mid x \in X\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4012}%
$\Psi \subseteq \overline{\mbox{Sub}(F)}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4016}%
$\Psi$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4024}%
$\circleddash ^k f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4034}%
$\overline{\mbox{Sub}(F)}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4038}%
$\Psi_0 \subseteq \overline{\mbox{Sub}(F)}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4040}%
$\langle s_0 \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4050}%
$\{\psi' \in
\overline{\mbox{Sub}(F)} \mid \Psi \models \mbox{Reg}(\psi',s')\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4052}%
$F = \{q \wedge \circleddash \circleddash p\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4056}%
$\overline{\mbox{Sub}(F)}=
\{p,q,\circleddash p, \circleddash \circleddash p, q \wedge \circleddash \circleddash p, \neg p, \neg q,
\neg \circleddash p, \neg \circleddash \circleddash p, \neg (q \wedge \circleddash \circleddash 
p)\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9725}%
$\textstyle \parbox{0.5\textwidth}{\includegraphics[height=0.18\textheight]{figures/pq}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9726}%
$\textstyle \parbox{0.4\textwidth}{\footnotesize
In the initial state, both $p$\  and $q$\  are false.  When $p$\  is false,
action $a$\  independently sets $p$\  and $q$\  to true with probability
0.8. When both $p$\  and $q$\  are false, action $b$\  sets $q$\  to true with
probability 0.8. Both actions have no effect otherwise. A reward is
obtained whenever $q \wedge \circleddash \circleddash p$. The optimal policy is to
apply $b$\  until $q$\  gets produced, making sure to avoid the state on
the left-hand side, then to apply $a$\  until $p$\  gets produced, and
then to apply $a$\  or $b$\  indifferently forever.  }$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4096}%
$l(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4098}%
$l$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4104}%
$l(s) = F \cup \{\mbox{Reg}(\psi',s') \mid \psi' \in l(s'), \mbox{$s'$\  is a
  successor of $s$}\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4106}%
$\overline{l(s)}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4110}%
$\Psi_0 \subseteq \overline{l(s_0)}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4112}%
$\psi' \subseteq
\overline{l(s')}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4116}%
$\psi'
\subseteq \overline{\mbox{Sub}(F)}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4130}%
$l(\{p\})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9752}%
$\textstyle \parbox{0.55\textwidth}{\includegraphics[height=0.4\textheight]{figures/pqpltlsim}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9753}%
$\textstyle \parbox{0.4\textwidth}{\footnotesize
\par
The following subformulae in $\overline{\mbox{Sub}(F)}$\  label the e-states:\\
$f_1: p$\\
$f_2: q$\\
$f_3: \circleddash p$\\
$f_4: \circleddash \circleddash p$\\
$f_5: q \wedge \circleddash \circleddash p$\\
$f_6: \neg p$\\
$f_7: \neg q$\\
$f_8: \neg \circleddash p$\\
$f_9: \neg \circleddash \circleddash p$\\
$f_{10}: \neg (q \wedge \circleddash \circleddash p)$
}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9757}%
$\textstyle \parbox{0.55\textwidth}{\includegraphics[height=0.4\textheight]{figures/pqpltlmin}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline9758}%
$\textstyle \parbox{0.4\textwidth}{\footnotesize
\par
The function $l$\  is given by:\\
$l(\{\}) = \{q \wedge \circleddash \circleddash p, \circleddash p, p\}$\\
$l(\{p\}) = \{q \wedge \circleddash \circleddash p\}$\\
$l(\{q\}) = \{q \wedge \circleddash \circleddash p, \circleddash p, p\}$\\
$l(\{p,q\}) =  \{q \wedge \circleddash \circleddash p, \circleddash p, p\}$\\[2ex]
The following formulae label the e-states:\\
$f_1: q \wedge \circleddash \circleddash p$\\
$f_2: \circleddash p$\\
$f_3: p$\\
$f_4: \neg(q \wedge \circleddash \circleddash p$)\\
$f_5: \neg\circleddash p$\\
$f_6: \neg p$\\
}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsubsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4182}%
$T$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4184}%
$\mbox{PTSub}(F)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4190}%
$T =
\{ \circleddash \psi \mid \psi \in \mbox{PTSub}(F), \psi \neq \circleddash \psi'\} \cup
\{\circleddash \psi \mid \circleddash \psi \in \mbox{PTSub}(F)\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4192}%
$f_1 \mathbin{\mbox{\sf S}}f_2 \equiv f_2 \vee (f_1 \wedge \circleddash (f_1
\mathbin{\mbox{\sf S}}f_2))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4198}%
$\mbox{PTSub}(F) = \{\circleddash p,\circleddash \circleddash p\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4206}%
$b$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap9776}%
\includegraphics[height=0.12\textheight]{figures/pqpltlstructprvp}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap9777}%
\includegraphics[height=0.12\textheight]{figures/pqpltlstructprvprvp}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap9778}%
\includegraphics[height=0.2\textheight]{figures/pqpltlstructreward}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4208}%
$\circleddash p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4210}%
$\circleddash \circleddash p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3384}%
\begin{displaymath}F = \{\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}(p \mathbin{\mbox{\sf S}}\ (q \vee
\circleddash r))\} \equiv  \{\top \mathbin{\mbox{\sf S}}\ (p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r))\}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3385}%
\begin{displaymath}\mbox{PTSub}(F) = \{ \top \mathbin{\mbox{\sf S}}\ (p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r)),
p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r), \circleddash r\}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3386}%
\begin{displaymath}T = \{ t_1: \circleddash (\top \mathbin{\mbox{\sf S}}\ (p \mathbin{\mbox{\sf S}}(q \vee \circleddash r))), t_2:
\circleddash (p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r)), t3: \circleddash r\}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4216}%
$p,q$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4218}%
$t_1, t_2, t_3$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3387}%
\begin{displaymath}
\begin{array}{ll}
\top \mathbin{\mbox{\sf S}}\ (p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r)) & \equiv\\
(p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r)) \vee \circleddash (\top \mathbin{\mbox{\sf S}}\ (p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r)))& \equiv\\
(q \vee \circleddash r) \vee (p \wedge \circleddash (p \mathbin{\mbox{\sf S}}\ (q \vee \circleddash r))) \vee t_1 & \equiv\\
 (q \vee t_3) \vee (p \wedge t_2) \vee t_1
\end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4220}%
$s_{0}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4222}%
$E(\pi)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4230}%
$s \in E(\pi)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4238}%
$^{*}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4246}%
$\{\langle s_0,s_1\rangle, \langle
s_0,s_0,s_1\rangle, \langle s_0,s_0,s_0,s_1\rangle \ldots\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4250}%
${\cal P}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath4252}%
\begin{displaymath}
{\cal L}::= {\cal P}\;|\; \neg {\cal P}\;|\; \mbox{$\top$}\;|\; \mbox{$\bot$}
\;|\; \mbox{\$}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

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

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4266}%
$\scriptstyle \bigcirc$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4268}%
$\mathbin{\mbox{\sf U}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath4270}%
\begin{displaymath}
{\cal F}::= {\cal L}\;|\; {\cal F}\wedge {\cal F}\;|\; {\cal F}
\vee {\cal F}\;|\; \raisebox{0.6mm}{$\scriptstyle \bigcirc$}{\cal F}\;|\; {\cal F}\makebox[1em]{$\mathbin{\mbox{\sf U}}$}{\cal F}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4274}%
$f_1 \makebox[1em]{$\mathbin{\mbox{\sf U}}$}f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4276}%
$f_{1}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4278}%
$f_{2}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4282}%
$\Box$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4290}%
$\mbox{$\Box$}f
\equiv f \makebox[1em]{$\mathbin{\mbox{\sf U}}$}\mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4296}%
$\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{k} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4302}%
$\raisebox{0.6mm}{$\scriptstyle \bigcirc$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4308}%
$\mbox{$\Diamond_{k}$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4312}%
$\bigvee_{i=1}^{k} \raisebox{0.6mm}{$\scriptstyle \bigcirc$}^i f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4318}%
$\mbox{$\Box_{k}$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4322}%
$\bigwedge_{i=1}^{k} \raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{i} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4328}%
$\neg\mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4330}%
$\mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4332}%
$B$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4342}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4348}%
$\Gamma\in
S^{\omega}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4356}%
$\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4362}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4364}%
$\Gamma(i)\in B$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4372}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4380}%
$(\Gamma,i)\mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4386}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4396}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \neg p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4400}%
$p\not\in\Gamma_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4414}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_1 \wedge f_2\; \mbox{ iff } \; (\Gamma,i)
  \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_1 \mbox{ and } (\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4428}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_1 \vee f_2\; \mbox{ iff } \; (\Gamma,i)
  \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_1 \mbox{ or } (\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4440}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \raisebox{0.6mm}{$\scriptstyle \bigcirc$}f\; \mbox{ iff } \;
(\Gamma,i+1)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4452}%
$(\Gamma,i)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_1 \makebox[1em]{$\mathbin{\mbox{\sf U}}$}f_2\; \mbox{ iff } \; \forall k\geq i
\mbox{ if } (\forall j, i\leq j\leq k \; (\Gamma,j)\mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4458}%
$\mbox{ then } (\Gamma,k)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4466}%
$\Gamma
\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4472}%
$(\Gamma,0)\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4478}%
$\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4504}%
$B_f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4514}%
$\mbox{$\Box$}(p \rightarrow \mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4532}%
$B_f \;\equiv\; \bigcap\{B \mid \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4548}%
$\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize $B$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4554}%
$\bigcap\emptyset$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4588}%
$B_g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4598}%
$\mbox{$\Box$}(p \rightarrow \mbox{$\Box$}\mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4604}%
$\neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p
\wedge \mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4620}%
$\mbox{$\Box$}((\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{k+1} p \wedge \mbox{$\Box_{k}$} \neg p) \rightarrow 
\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{k+1} \mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4632}%
$\mbox{$\Box$}(c \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{$\Box$}(p \rightarrow 
\mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4644}%
$\mbox{$\Box$}(c\rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}(\neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}
(p \wedge \mbox{\$})))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4652}%
$\mbox{$\Box$}(c \rightarrow \mbox{$\Box_{k}$}(p \rightarrow 
\mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4660}%
$\mbox{\$}\makebox[1em]{$\mathbin{\mbox{\sf U}}$}\neg p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4670}%
$\mbox{$\Box$}(q \rightarrow (\mbox{\$}
\makebox[1em]{$\mathbin{\mbox{\sf U}}$}\neg p))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4678}%
$\neg q
\makebox[1em]{$\mathbin{\mbox{\sf U}}$}((\neg p \wedge \neg q) \vee (q \wedge \mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4682}%
$\raisebox{0.6mm}{$\scriptstyle \bigcirc$}p \rightarrow \mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4694}%
$\mbox{$\Box$}(p \rightarrow \mbox{\$}) \vee
  \mbox{$\Box$}(\neg p \rightarrow \mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4698}%
$\neg p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4708}%
$\{B \mid
\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4718}%
$B \subseteq S^{*}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4728}%
$\Gamma(i) \in B_f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4756}%
$\mbox{\mbox{\$}FLTL}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4766}%
$\mbox{Prog}(b,s,f)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4770}%
$\mbox{Prog}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4790}%
$f \wedge \mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4798}%
$f \wedge \mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{algorithm679}%
\begin{algorithm}
% latex2html id marker 679

\caption{
\$FLTL Progression}
\begin{tabular}{l@{~~~}l@{~~~}l}
$\mbox{Prog}(\mbox{true},s,\mbox{\$})$\  & = & $\mbox{$\top$}$\\
$\mbox{Prog}(\mbox{false},s,\mbox{\$})$\  & = & $\mbox{$\bot$}$\\
$\mbox{Prog}(b,s,\mbox{$\top$})$\  & = & $\mbox{$\top$}$\\
$\mbox{Prog}(b,s,\mbox{$\bot$})$\  & = & $\mbox{$\bot$}$\\
$\mbox{Prog}(b,s,p)$\  & = & $\mbox{$\top$}$\  iff $p\in s$\  and $\mbox{$\bot$}$\  otherwise\\
$\mbox{Prog}(b,s,\neg p)$\  &= & $\mbox{$\top$}$\  iff $p\not\in s$\  and $\mbox{$\bot$}$\  otherwise\\
$\mbox{Prog}(b,s,f_1 \wedge f_2)$\  & = & $\mbox{Prog}(b,s,f_1) \wedge \mbox{Prog}(b,s,f_2)$\\
$\mbox{Prog}(b,s,f_1 \vee f_2)$\  & = &  $\mbox{Prog}(b,s,f_1) \vee \mbox{Prog}(b,s,f_2)$\\
$\mbox{Prog}(b,s,\raisebox{0.6mm}{$\scriptstyle \bigcirc$}f)$\   & = & $f$\\
$\mbox{Prog}(b,s,f_{1} \makebox[1em]{$\mathbin{\mbox{\sf U}}$}f_{2})$\  & = & $\mbox{Prog}(b,s,f_{2})$\  $\vee
(\mbox{Prog}(b,s,f_{1}) \wedge f_{1} \makebox[1em]{$\mathbin{\mbox{\sf U}}$}f_{2})$\  \\[1ex]
$\mbox{Rew}(s,f)$\  & = & true iff $\mbox{Prog}(\mbox{false},s,f)=\mbox{$\bot$}$\\
$\mbox{\$}\mbox{Prog}(s,f)$\  & = & $\mbox{Prog}(\mbox{Rew}(s,f),s,f)$
\end{tabular}
\end{algorithm}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4890}%
$b \Leftrightarrow (\Gamma(i) \in B)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4902}%
$(\Gamma,i+1) \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{\em Prog}(b,
\Gamma_i,f)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4932}%
$\mbox{\$}\mbox{Prog}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4934}%
$\mbox{Rew}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4942}%
$\langle f_0, f_1, \ldots \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4944}%
$f_0 = f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4946}%
$f_{i+1} = \mbox{\$}\mbox{Prog}(\Gamma_i,f_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4970}%
$f_{i+1}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4978}%
$\{\Gamma(i)|
\mbox{Rew}(\Gamma_i,f_i)\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4982}%
$f = \neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4992}%
$\mbox{Prog}(\mbox{false},s,f) = \bot \vee (\bot
\wedge \neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$})) \equiv \bot$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4994}%
$\bot$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline4996}%
$\mbox{Rew}(s,f)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5000}%
$\mbox{\$}\mbox{Prog}(s,f) = \mbox{Prog}(\mbox{true},s,f) = \top \vee (\bot \wedge
\neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$})) \equiv \top$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5010}%
$\mbox{Prog}(\mbox{false},s,f) =
\bot \vee (\top \wedge \neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$})) \equiv \neg p
\makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5018}%
$\mbox{\$}\mbox{Prog}(s,f) =
\mbox{Prog}(\mbox{false},s,f) = \neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5026}%
$\mbox{\$}\mbox{\em Prog}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5036}%
$\mbox{\em Rew}(\Gamma_i,f_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5038}%
$\Gamma(i)\in B_{f}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5050}%
$f_i = \mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5070}%
$\Gamma_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5076}%
$f_0 =
\raisebox{0.6mm}{$\scriptstyle \bigcirc$}p \rightarrow \mbox{\$}= \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\neg p \vee \mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5078}%
$\mbox{Rew}(\Gamma_0,f_0) = \mbox{false}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5080}%
$f_{1} = \neg p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5082}%
$p\in\Gamma_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5086}%
$f_{2} = \mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5098}%
$\raisebox{0.6mm}{$\scriptstyle \bigcirc$}\raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{$\top$}\rightarrow \mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5112}%
$\phi \subseteq \mbox{\mbox{\$}FLTL}\ \times \mbox{I$\!$R}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5122}%
$(f:r) \in \phi$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5124}%
$R_{\phi}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5128}%
$ {\displaystyle R_{\phi}(\Gamma(i)) = \sum_{(f:r) \in \phi} \{r\mid
  \Gamma(i) \in B_{f}\}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5138}%
$\{\neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$}) : 5.2,
\mbox{$\Box$}(q\rightarrow \mbox{$\Box$}\mbox{\$}) : 7.3\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5142}%
$7.3$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5146}%
$12.5$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5152}%
$\langle \phi_{0}, \phi_{1},
\ldots\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5154}%
$\phi_{i+1} =
\mbox{R}\mbox{Prog}(\Gamma_i,\phi_{i})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5156}%
$\mbox{R}\mbox{Prog}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3388}%
\begin{displaymath}\mbox{R}\mbox{Prog}(s,\phi) = \{(\mbox{Prog}(s,f):r) \mid (f:r) \in \phi\}\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5160}%
$\phi_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath3389}%
\begin{displaymath}
\sum_{(f:r) \in \phi_{i}} \{r \mid \mbox{Rew}(\Gamma_{i},f)\}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5164}%
$\langle \phi_{0},\phi_{1}
  \ldots\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5168}%
$\mbox{{\em R}\mbox{\em Prog}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5172}%
$(\mbox{$\bot$}\!:\!r)\!\not\in\!\phi_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5176}%
${\displaystyle \sum_{(f:r) \in \phi_{i}} \{r \mid
    \mbox{\em Rew}(\Gamma_{i},f)\} = R_{\phi}(\Gamma(i))}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5180}%
$\phi_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5184}%
$\langle s, \phi\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5194}%
$\langle t,\psi \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5196}%
$s=t$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5204}%
$\{(p \rightarrow \mbox{\$}:3),
  (q \rightarrow \mbox{\$}:2)\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5206}%
$\{((p
  \wedge q) \rightarrow \mbox{\$}:5), ((p \wedge \neg q)
  \rightarrow \mbox{\$}:3), ((\neg p \wedge q) \rightarrow
  \mbox{\$}:2)\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5210}%
$\phi_{0}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5214}%
$R_{\phi_0} = R$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5218}%
$D'=\langle S',s'_{0},A',\Pr',R'\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5222}%
$S' \subseteq S\times 2^{\mbox{\mbox{\$}FLTL}\ \times \mbox{I$\!$R}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5224}%
$s'_{0} = \langle s_{0},\phi_0 \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5226}%
$A'(\langle s,\phi \rangle) = A(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5228}%
$a\in A'(\langle s, \phi\rangle)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5230}%
$\Pr'(\langle
s,\phi\rangle,a,\langle s', \phi'\rangle) =$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5232}%
$\left\{ \begin{array}{ll}
  \Pr(s,a,s') & \mbox{if~} \phi' = \mbox{{\em R}\mbox{\em Prog}}(s,\phi)\\0 &
   \mbox{otherwise}
\end{array} \right.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5234}%
$a\not\in A'(\langle s, \phi\rangle)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5236}%
$\Pr'(\langle
s,\phi\rangle,a,\bullet)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5238}%
$R'(\langle s,\phi\rangle) = {\displaystyle \sum_{(f:r) \in \phi}
\{r \mid \mbox{\em Rew}(s,f)\}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5264}%
$\Pr'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5266}%
$\Pr $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5272}%
$\tau(\langle s,\phi\rangle) = s$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5274}%
$\mbox{R}\mbox{Prog}(s_0,\phi_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5276}%
$q \wedge \circleddash \circleddash p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5288}%
$\mbox{$\Box$}((p \wedge
\raisebox{0.6mm}{$\scriptstyle \bigcirc$}\raisebox{0.6mm}{$\scriptstyle \bigcirc$}q) \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5292}%
$\{f_1\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5294}%
$\{f_1,f_2\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5296}%
$\{f_1,f_2,f_3\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline10214}%
$\textstyle \parbox{0.55\textwidth}{\includegraphics[height=0.4\textheight]{figures/pqfltl}}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline10215}%
$\textstyle \parbox{0.4\textwidth}{\footnotesize
\par
The following formulae label the e-states:\\
$f_1: \mbox{$\Box$}((p \wedge \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\raisebox{0.6mm}{$\scriptstyle \bigcirc$}q) \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{\$})$\\
$f_2: \raisebox{0.6mm}{$\scriptstyle \bigcirc$}q \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{\$}$\\
$f_3: q \rightarrow \mbox{\$}$\\
}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5320}%
$\langle s',\phi'\rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5334}%
$\phi'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5348}%
$\mbox{$\Box$}(p
\rightarrow (\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{k}q \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{k}\mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5368}%
$\rho$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5370}%
$\mu$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5378}%
$\mbox{I$\!$R}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5380}%
$\tau(e)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5386}%
$S'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5396}%
$\Gamma'(i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5398}%
$\widetilde{D'}(s'_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5400}%
$\Gamma'(i) = e$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5404}%
$\widetilde{D}(s_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5408}%
$j \leq i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5410}%
$\Gamma(j) = \tau(\Gamma'_j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5412}%
$\Delta
\in S^*$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5414}%
\begin{displaymath}
  \rho(e): \Delta \mapsto \left\{\begin{array}{ll}
      R(\Gamma(i-1);\Delta) & \mbox{if $\Delta_0 = \Gamma_i$} \\
      0 & \mbox{otherwise}
  \end{array}\right.
  \end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath5416}%
\begin{displaymath}
  \mu(e): \Delta \mapsto \left\{\begin{array}{ll}
      R(\Gamma(i-1);\Delta) & \mbox{if $\Delta \in \widetilde{D}(\Gamma_i)$} \\
      0 & \mbox{otherwise}
  \end{array}\right.
  \end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5420}%
$\rho(e)(\Delta)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5422}%
$\mu(e)(\Delta)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5424}%
$\Delta$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5452}%
$s'_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5454}%
$\tau(s'_1) = \tau(s'_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5456}%
$\mu(s'_1) = \mu(s'_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5480}%
$\rho(s'_1) = \rho(s'_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5500}%
$(\mbox{$\bot$}:r) \in \phi$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5502}%
$c_0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5506}%
$\langle s,\phi,c \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5510}%
$a \in A'(\langle s,\phi,c\rangle)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5512}%
$a\in A(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5516}%
$c\neq \mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5522}%
$\mbox{$\Box$}(p\rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}
q)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5532}%
$\neg \mbox{heads}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5536}%
$\mbox{heads}\wedge \neg \circleddash \makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}\mbox{heads}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5538}%
$\circleddash ^{2}
\mbox{heads}\wedge \circleddash \mbox{heads}\wedge \neg \mbox{heads}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5542}%
$\Diamond$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{figure863}%
\begin{figure}\begin{verbatim}

action flip
   heads (0.5)
endaction

action tilt
   heads (heads (0.9) (0.1))
endaction

heads = ff
[first, 5.0]? heads and ~prv (pdi heads)
[seq, 1.0]? (prv^2 heads) and (prv heads) and ~heads\end{verbatim}

\vspace*{-2ex}

\vspace*{-2ex}
\end{figure}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5544}%
$(\beta,\epsilon)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10354}%
\includegraphics[height=0.17\textheight]{figures/value}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10355}%
\includegraphics[height=0.1\textheight]{figures/policy}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10356}%
\includegraphics[height=0.28\textheight]{figures/domain}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5556}%
$\circleddash ^nf$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

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

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5562}%
$p_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5566}%
$a_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5570}%
$p_j$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5572}%
$1 \leq j < i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5598}%
$i/(n+1)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5602}%
$j\neq i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5606}%
$2^n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5612}%
$n=6$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5616}%
$\circleddash ^{n} \neg
\circleddash \mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5622}%
$\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{n}\mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10459}%
\includegraphics[width=0.65\textwidth]{figures/structure}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10463}%
\includegraphics[width=0.65\textwidth]{figures/uncertainty}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5640}%
$1 \leq n \leq 12$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5648}%
$(\wedge_{i=1}^{n} p_i) \wedge (\neg\circleddash \makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}\wedge_{i=1}^{n} p_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5650}%
${\cal O}(1)||S||$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5656}%
$(\wedge_{i=1}^{n}\circleddash ^{i} p_i) \wedge \circleddash ^{n} \neg \circleddash \mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5658}%
${\cal O}(n)||S||$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5662}%
$\vee_{i=1}^{n-1} (\circleddash p_i \wedge p_{i+1})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5664}%
${\cal O}(n^{k})||S||$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5670}%
$\circleddash ^{n} \wedge_{i=1}^{n} p_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5672}%
${\cal O}(2^n)||S||$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10513}%
\includegraphics[width=0.65\textwidth]{figures/syntax}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5678}%
$\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}_{k} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5680}%
$\boxminus _{k}f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5690}%
$\mbox{\emph{prvOut}}\equiv\circleddash ^n (\wedge_{i=1}^{n} p_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5692}%
$\mbox{\emph{prvIn}}\equiv\wedge_{i=1}^{n} \circleddash ^n p_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10528}%
\includegraphics[width=0.65\textwidth]{figures/multiplesize}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10532}%
\includegraphics[width=0.65\textwidth]{figures/multipletime}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5696}%
$\{f_1,f_2, \ldots, f_n\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5700}%
$f_1 \vee f_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5702}%
$\{f_1 \equiv \top, f_2 \equiv \bot\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5704}%
$\{f_1 \equiv \bot, f_2 \equiv \top\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5706}%
$f_i = \circleddash p_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5714}%
$\{(\circleddash \vee_{i=1}^{n} (p_i
\wedge_{j=1,j\neq i}^{n} \neg p_j) : r), \ldots, (\circleddash \wedge_{i=1}^{n}
p_i : n*r)\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5722}%
$g \wedge \circleddash ^{k} c$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5726}%
$g \wedge
\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}_{k}c$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5732}%
$\mbox{$\Box$}(c \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}^k (g \rightarrow 
\$))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5738}%
$\mbox{$\Box$}(c \rightarrow \mbox{$\Box$}_k(g \rightarrow \$))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5744}%
$\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^k g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5748}%
$g \wedge
\circleddash ^{n} c$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10561}%
\includegraphics[width=0.65\textwidth]{figures/unachievablegoal}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10565}%
\includegraphics[width=0.65\textwidth]{figures/unachievablecondition}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5754}%
$\circleddash ^{k} c$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5768}%
$\neg g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5772}%
$(\neg g : r)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5774}%
$\neg
c$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10586}%
\includegraphics[width=0.65\textwidth]{figures/unrewardinggoal}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10590}%
\includegraphics[width=0.65\textwidth]{figures/unrewardingcondition}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

\stepcounter{subsection}
\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5784}%
$P_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5786}%
$ServedP_i \wedge \circleddash \boxminus \neg ServedP_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5790}%
$\neg ServedP_i \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(ServedP_i \wedge \mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5794}%
$NonStopP_i \wedge \circleddash \circleddash \neg BoardedP_i \wedge \circleddash \circleddash \neg ServedP_i
\wedge ServedP_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5806}%
$\mbox{$\Box$}((NonStopP_i \wedge \neg BoardedP_i \wedge \neg ServedP_i
\wedge \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\raisebox{0.6mm}{$\scriptstyle \bigcirc$}ServedP_i) \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5810}%
$(BoardedP_i \wedge SupervisedP_i)
\rightarrow (BoardedP_j \wedge SupervisorP_jP_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5812}%
$ServedP_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5816}%
$\neg q \makebox[1em]{$\mathbin{\mbox{\sf U}}$}((\neg p
\wedge \neg q) \vee (q \wedge \mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5822}%
$P_j$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5824}%
$SupervisedP_i \wedge SupervisorP_jP_i \wedge ServedP_i \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5826}%
$\circleddash \boxminus \neg ServedP_i \wedge \boxminus (BoardedP_i \rightarrow BoardedP_j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5830}%
$\neg ServedP_i \makebox[1em]{$\mathbin{\mbox{\sf U}}$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5832}%
$((BoardedP_i \wedge SupervisedP_i \wedge
                        \neg(BoardedP_j \wedge SupervisorP_jP_i) \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5834}%
$~\neg ServedP_i) \vee
                         (ServededP_i \wedge \mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5838}%
$DirectP_i \wedge ServedP_i \wedge \circleddash \neg ServedP_i \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5840}%
$((\bigvee_j \bigvee_{k > j} (AtFloor_k \wedge \circleddash AtFloor_j))\mathbin{\mbox{\sf S}}
(BoardedP_i \wedge \circleddash \neg BoardedP_i))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5846}%
$\mbox{$\Box$}((DirectP_i \wedge BoardedP_i) \rightarrow (\neg ServedP_i \makebox[1em]{$\mathbin{\mbox{\sf U}}$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5850}%
$((\neg (\bigvee_j \bigvee_{k > i} AtFloor_j \wedge \raisebox{0.6mm}{$\scriptstyle \bigcirc$}AtFloor_k) \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5852}%
$~\neg ServedP_i) \vee
                                                            (servedP_i \wedge \mbox{\$}))))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5858}%
$\circleddash \boxminus \neg
ServedP_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5860}%
$\top$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10660}%
\includegraphics[width=0.65\textwidth]{figures/miconicsimpletime}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10664}%
\includegraphics[width=0.65\textwidth]{figures/miconicsimplespace}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10668}%
\includegraphics[width=0.65\textwidth]{figures/miconicheuristictime}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10672}%
\includegraphics[width=0.65\textwidth]{figures/miconicheuristicspace}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10676}%
\includegraphics[width=0.65\textwidth]{figures/miconichardtime}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap10680}%
\includegraphics[width=0.65\textwidth]{figures/miconichardspace}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5862}%
$50*n$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5866}%
$\geq$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5882}%
$g_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5884}%
$g_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\appendix
\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5908}%
$m$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{eqnarraystar1403}%
\begin{eqnarray*}
     \mbox{{\sf delay}}[f]       & = & \raisebox{0.6mm}{$\scriptstyle \bigcirc$}f         \\
     \mbox{{\sf cond}}[m,f]      & = & m \rightarrow f \\
     \mbox{{\sf loop}}[m,f]      & = & f \makebox[1em]{$\mathbin{\mbox{\sf U}}$}m      \\
     \mbox{{\sf union}}[f_1,f_2] & = & f_1 \wedge f_2
\end{eqnarray*}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5918}%
$\{\mbox{\$}\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5928}%
$\mbox{{\sf loop}}[\mbox{$\bot$},\mbox{{\sf cond}}[p,\mbox{\$}]]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5936}%
$\mbox{$\Box$}((p \wedge
\raisebox{0.6mm}{$\scriptstyle \bigcirc$}q) \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{\$})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5946}%
$\mbox{$\Box$}(p \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}(q \rightarrow \mbox{\$}))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5950}%
$\mbox{{\sf loop}}[\mbox{$\bot$},\mbox{{\sf cond}}[p,\mbox{{\sf
    delay}}[\mbox{{\sf cond}}[q,\mbox{\$}]]]]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5962}%
$(p \rightarrow \mbox{\$})
\wedge (\raisebox{0.6mm}{$\scriptstyle \bigcirc$}(p \rightarrow \mbox{\$}) \makebox[1em]{$\mathbin{\mbox{\sf U}}$}p)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5976}%
$(\Gamma,i+1)
\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{Prog}(b, \Gamma_i,f)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5982}%
$f=\mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5986}%
$f=\mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5988}%
$f = p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline5998}%
$\Gamma_{i+1}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6010}%
$f = \neg p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6012}%
$f = \mbox{\$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6026}%
$\mbox{Prog}(b,\Gamma_i,f) = \mbox{$\top$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6034}%
$f = g \wedge h$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6046}%
$(\Gamma,i) \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6052}%
$(\Gamma,i) \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} h$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6058}%
$(\Gamma,i+1) \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{Prog}(b, \Gamma_i,g)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6064}%
$(\Gamma,i+1) \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{Prog}(b, \Gamma_i,h)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6070}%
$(\Gamma,i+1) \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \mbox{Prog}(b, \Gamma_i,g) \wedge
  \mbox{Prog}(b, \Gamma_i,h)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6078}%
$f = g \vee h$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6082}%
$f = \raisebox{0.6mm}{$\scriptstyle \bigcirc$}g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6086}%
$f = g \makebox[1em]{$\mathbin{\mbox{\sf U}}$}h$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6094}%
$h \vee (g \wedge \raisebox{0.6mm}{$\scriptstyle \bigcirc$}(g \makebox[1em]{$\mathbin{\mbox{\sf U}}$}h)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6102}%
$\mbox{Prog}(b, \Gamma_i, f)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6150}%
$b_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6158}%
$\Gamma \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6196}%
$\Gamma \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6202}%
$\Gamma \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} h$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6206}%
$h$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6250}%
$g'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6256}%
$g' \vee
    \mbox{$\bot$}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6278}%
$\Gamma
    = \Gamma_0;\Delta$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6280}%
$B' = \{\gamma| \Gamma_0;\gamma \in
    B\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6286}%
$\Delta \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B'$}}\:$} g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6292}%
$B'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6318}%
$j$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6324}%
$(\Gamma,j) \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6326}%
$i \leq j$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6332}%
$(\Gamma,i) \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} h$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6336}%
$j=0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6358}%
$h \vee (g \wedge f')$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6364}%
$f'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6368}%
$f' = \raisebox{0.6mm}{$\scriptstyle \bigcirc$}f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6374}%
$\Gamma \mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} g$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6386}%
$h \vee (g \wedge \raisebox{0.6mm}{$\scriptstyle \bigcirc$}f)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6412}%
$\Gamma \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B$}}\:$} \raisebox{0.6mm}{$\scriptstyle \bigcirc$}f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6422}%
$\Delta
    \mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize$B'$}}\:$} f$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6424}%
$j-1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6472}%
$D^c$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6476}%
${\Gamma}1(i) \equiv {\Gamma}2(j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6478}%
${\Gamma}1_i = {\Gamma}2_j$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6482}%
${\Gamma}1(i);\Delta \in
  \widetilde{D}(s_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6484}%
$R({\Gamma}1(i);\Delta) =
  R({\Gamma}2(j);\Delta)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6486}%
$[\Gamma(i)]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6490}%
${\cal E}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6492}%
${\cal A}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6498}%
$A(\Gamma_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6502}%
$\Delta(j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6504}%
$a \in {\cal A}([\Gamma(i)])$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6506}%
${\cal T}( [\Gamma(i)],a,[\Delta(j)] )$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6508}%
$\Pr(\Gamma_i,a,s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6510}%
$[\Delta(j)] = [\Gamma(i);\langle s \rangle]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6512}%
${\cal
    T}( [\Gamma(i)],a,[\Delta(j)] ) = 0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6514}%
${\cal R}([\Gamma(i)])$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6524}%
$D^c = \langle {\cal E}, [\langle s_0 \rangle], {\cal A}, {\cal
    T}, {\cal R} \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6528}%
$\tau([\Gamma(i)])=\Gamma_i$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6530}%
$D''$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6536}%
$\cal E$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6556}%
$\Gamma{1}(i) \equiv
\Gamma{2}(j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6560}%
${\cal T}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6562}%
${\cal R}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6568}%
$\Gamma{1}_i = \Gamma{2}_j$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6572}%
$\Delta = \langle \Gamma{1}_i \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6574}%
$\tau([s_0]) =
s_{0}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6576}%
${\cal A}([\Gamma(i)])= A(\Gamma_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6580}%
${\cal
  R}([\Gamma(i)]) = R(\Gamma(i))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6590}%
$\Gamma(i) \in
  \widetilde{D}(s_0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6592}%
$\Gamma_i = s_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6594}%
$[\Delta(j)] \in {\cal E}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6596}%
$\Delta_j = s_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6600}%
${\cal
    T}([\Gamma(i)],a,[\Delta[j]]) = \Pr(s_1,a,s_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6602}%
$\Pr(s_1,\alpha,s_2) > 0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6610}%
$\Gamma(i);\langle s_2 \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6614}%
$[\Gamma(i);\langle s_2 \rangle]$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6620}%
$\tau(X) = s_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6622}%
$a \in
  A(\Gamma_i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6624}%
${\cal T}( [\Gamma(i)],a,X ) = \Pr(s_1,a,s_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6628}%
${\cal T} ( [ \Gamma(i) ],a, [\Gamma(i);\langle s_2 \rangle] ) =
\Pr(\Gamma_i,a,s_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6630}%
$\cal T$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6650}%
$M$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6654}%
$s_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6656}%
$s_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6664}%
$\tau(X) = s_1$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6666}%
$Y$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6670}%
$\tau(Y) =
s_2$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6688}%
$\approx_M$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6692}%
$\Gamma(i) \approx_M \Delta(j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6706}%
$\equiv$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6710}%
$\Gamma(i) \equiv \Delta(j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6732}%
$\Gamma{1}(i)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6734}%
$\Gamma{2}(j)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6740}%
$s_0'$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6748}%
$\tau(s'_1) =
\Gamma{1}_i = \Gamma{2}_j = \tau(s'_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6750}%
$\mu(s'_1) \neq
\mu(s'_2)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6752}%
$\Delta(k) \in
\widetilde{D}(s)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6754}%
$R(\Gamma{1}(i-1);\Delta(k)) \neq
R(\Gamma{2}(j-1);\Delta(k))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6776}%
$s = \tau(\langle s, \phi \rangle)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6786}%
$\Delta_0 = s$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6790}%
$\sum_{(f:r) \in \phi} \{r\mid \Delta \in
  B_{f}\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline6796}%
$\langle s, \phi' \rangle$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline11536}%
$^*$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}


\end{document}
