

\newtheorem{definition}{\color{red}Definition}
\newtheorem{theorem}{\color{red}Theorem}
\newtheorem{example}{\color{red}Example}


\newcommand{\head}[1]{\begin{center}{\color{blue} \bf #1}\end{center}}
\newcommand{\sol}{\mbox{\bf Solution: }}
\newcommand{\myComment}[1]{}
\newcommand{\ul}{\underline}


\newcommand{\defeq}{\stackrel {\mathsf{def}}{=}}
\newcommand{\defequiv}{\stackrel {\mathit{def}}{\Leftrightarrow}}
\newcommand{\set}[1]{\left\{ #1 \right\}}
\newcommand{\setdef}[2]{\left\{ #1 \mid #2 \right\}}


\newcommand{\length}[1]{\left| #1 \right|}
\newcommand{\size}[1]{\left| #1 \right|}
\newcommand{\eclass}[1]{\left[ #1 \right]}


%\newcommand{\Not}[1]{\neg #1}
%\newcommand{\Or}[2]{#1 \vee #2}
%\newcommand{\And}[2]{#1 \wedge #2}
%\newcommand{\Implies}[2]{#1 \Rightarrow #2}
%\newcommand{\Equiv}[2]{#1 \Leftrightarrow #2}


\newcommand{\In}[2]{#1 \in #2}
\newcommand{\Notin}[2]{#1 \not\in #2}

\newcommand{\Union}[2]{#1 \cup #2}
\newcommand{\Intersect}[2]{#1 \cap #2}
\newcommand{\Product}[2]{#1 \times #2}
\newcommand{\Concat}[2]{#1 \cdot #2}
\newcommand{\Ast}[1]{{#1}^\ast}
\newcommand{\Astplus}[1]{{#1}^+}
\newcommand{\Pow}[1]{2^{#1}}
\newcommand{\Subset}[2]{#1 \subseteq #2}
\newcommand{\Pset}[1]{\mathcal{P}(#1)}


\newcommand{\Mapping}[3]{#1 : #2 \rightarrow #3}
\newcommand{\refa}[2]{\alpha^{#1}_{#2}}
\newcommand{\subst}[3]{{\bf s}^{#1}_{#2} (#3)}
\newcommand{\Prod}[2]{#1 \rightarrow #2}
\newcommand{\OSDeriv}[2]{#1 \rightarrow_G #2}
\newcommand{\Deriv}[2]{#1 \rightarrow^{\ast}_G #2}
\newcommand{\Labprod}[3]{#1 \stackrel{#2}{\hookrightarrow} #3}
\newcommand{\Labtrans}[3]{#1 \stackrel{#2}{\longrightarrow} #3}
\newcommand{\Trans}[2]{#1 \rightarrow #2}
\newcommand{\STrans}[2]{#1 \rightarrow_S #2}
\newcommand{\SOSTrans}[2]{#1 \Rightarrow #2}
\newcommand{\SOSLabTrans}[3]{#1 \stackrel{#2}{\Longrightarrow} #3}
\newcommand{\AMTrans}[2]{#1 \rightarrow_{AM} #2}
\newcommand{\amtrans}[2]{#1 \rhd #2}
\newcommand{\RTtrans}[2]{#1 \rightarrow^{\ast} #2}
\newcommand{\RecCbvTrans}[2]{#1 \rightarrow^{d}_{va} #2}
\newcommand{\RecCbvOsTrans}[2]{#1 \stackrel{1}{\longrightarrow}^{d}_{va} #2}
\newcommand{\RecCbvAstTrans}[2]{#1 \stackrel{\ast}{\longrightarrow}^{d}_{va} #2}
\newcommand{\config}[2]{\left< #1, #2 \right>}
\newcommand{\amconfig}[3]{\left< #1, #2, #3 \right>}
\newcommand{\tmconfig}[3]{\left< #1, #2, #3 \right>}
\newcommand{\BSConfTrans}[3]{\Trans{\config{#1}{#2}}{#3}}
\newcommand{\BSConfATrans}[3]{\Labtrans{\config{#1}{#2}}{\Join}{#3}}
\newcommand{\SSConfTrans}[4]{\STrans{\config{#1}{#2}}{\config{#3}{#4}}}
\newcommand{\SSConfFinTrans}[3]{\STrans{\config{#1}{#2}}{#3}}
\newcommand{\SOSConfTrans}[4]{\SOSTrans{\config{#1}{#2}}{\config{#3}{#4}}}
\newcommand{\SOSConfFinTrans}[3]{\SOSTrans{\config{#1}{#2}}{#3}}
\newcommand{\SOSConfLabTrans}[5]{\SOSLabTrans{\config{#1}{#2}}{#3}{\config{#4}{#5}}}
\newcommand{\AMConfTrans}[4]{\AMTrans{\config{#1}{#2}}{\config{#3}{#4}}}
\newcommand{\amconftrans}[6]{\amtrans{\amconfig{#1}{#2}{#3}}{\amconfig{#4}{#5}{#6}}}
\newcommand{\assert}[1]{\left\{ #1 \right\}}
\newcommand{\Hoare}[3]{\assert{#1} #2 \assert{#3}}
\newcommand{\Wlp}[2]{\mathit{wlp} (#1, #2)}
\newcommand{\Vcg}[3]{\mbox{\em vcg} \denot{#1} (#2, #3)}
\newcommand{\VCG}[1]{\mbox{\em VCG} (#1)}
\newcommand{\denot}[1]{\left[\!\left[#1\right]\!\right]}
\newcommand{\arexdenot}[1]{{\cal A}\!\denot{#1}}
\newcommand{\bexdenot}[1]{{\cal B}\!\denot{#1}}
\newcommand{\comdenot}[1]{{\cal C}\!\denot{#1}}
\newcommand{\stmdenot}[1]{{\cal S}_{ds}\!\denot{#1}}
\newcommand{\eoarexdenot}[1]{{\cal EA}\!\denot{#1}}
\newcommand{\eobexdenot}[1]{{\cal EB}\!\denot{#1}}
\newcommand{\eostmdenot}[1]{{\cal ES}\!\denot{#1}}
\newcommand{\dsstmdenot}[1]{{\cal DS}\!\denot{#1}}
\newcommand{\deriv}[1]{\parallel\!\!\!- \> #1}
\newcommand{\problig}[2]{\models #1 \>\Rightarrow\> #2}


\newcommand{\REC}{\mbox{\bf REC}}
\newcommand{\IMP}{\mbox{\bf IMP}}
\newcommand{\WHILE}{\mbox{\bf While}}
\newcommand{\AM}{\mbox{\bf AM}}
\newcommand{\AExp}{\mbox{\bf AExp}}
\newcommand{\BExp}{\mbox{\bf BExp}}
\newcommand{\Stm}{\mbox{\bf Stm}}
\newcommand{\Code}{\mbox{\bf Code}}
\newcommand{\Assn}{\mbox{\bf Assn}}

\newcommand{\True}{\mbox{\bf true}}
\newcommand{\False}{\mbox{\bf false}}
\newcommand{\Brand}{\mbox{\bf brand}}
\newcommand{\Skip}{\mbox{\bf skip}}
\newcommand{\Break}{\mbox{\bf break}}
\newcommand{\If}{\mbox{\bf if}}
\newcommand{\Then}{\mbox{\bf then}}
\newcommand{\Else}{\mbox{\bf else}}
\newcommand{\While}{\mbox{\bf while}}
\newcommand{\Do}{\mbox{\bf do}}
\newcommand{\Repeat}{\mbox{\bf repeat}}
\newcommand{\Until}{\mbox{\bf until}}
\newcommand{\For}{\mbox{\bf for}}
\newcommand{\Inn}{\mbox{\bf in}}
\newcommand{\Read}{\mbox{\bf read}}
\newcommand{\Write}{\mbox{\bf write}}
\newcommand{\Thread}{\mbox{\bf thread}}
\newcommand{\End}{\mbox{\bf end}}
\newcommand{\Try}{\mbox{\bf try}}
\newcommand{\Catch}{\mbox{\bf catch}}
\newcommand{\Or}{\mbox{\bf or}}
\newcommand{\Array}{\mbox{\bf array}}

\newcommand{\Op}{\mbox{\bf op}}
\newcommand{\op}{\mbox{op}}
\newcommand{\true}{\mbox{\em true}}
\newcommand{\false}{\mbox{\em false}}
\newcommand{\even}{\mbox{\em even}}
\newcommand{\odd}{\mbox{\em odd}}
\newcommand{\Fib}{\mbox{\em Fib}}
\newcommand{\cond}{\mbox{\sf cond}}
\newcommand{\undef}{\mbox{\underline{undef}}}


\newcommand{\ttt}{\mbox{\bf tt}}
\newcommand{\fff}{\mbox{\bf ff}}
\newcommand{\Z}{\mbox{\bf Z}}
\newcommand{\T}{\mbox{\bf T}}
\newcommand{\State}{\mbox{\bf State}}
\newcommand{\EState}{\mbox{\bf EState}}
\newcommand{\PState}{\mbox{\bf PState}}
\newcommand{\fix}{\mbox{\em fix}}
\newcommand{\INIT}{\mbox{\sc INIT}}
\newcommand{\TOP}{\mbox{\sc TOP}}
\newcommand{\NONE}{\mbox{\sc NONE}}
\newcommand{\NEG}{\mbox{\sc NEG}}
\newcommand{\ZERO}{\mbox{\sc ZERO}}
\newcommand{\POS}{\mbox{\sc POS}}
\newcommand{\EVEN}{\mbox{\sc EVEN}}
\newcommand{\ODD}{\mbox{\sc ODD}}
\newcommand{\ANY}{\mbox{\sc ANY}}
\newcommand{\TTT}{\mbox{\sc TT}}
\newcommand{\FFF}{\mbox{\sc FF}}
\newcommand{\EO}{\mbox{\bf EO}}
\newcommand{\I}{\mbox{\bf I}}
\newcommand{\PP}{\mbox{\bf P}}
\newcommand{\TT}{\mbox{\bf TT}}

\newcommand{\RuleDef}[3]{
   \begin{tabular}{cc}
       ${#1}$ &
       \begin{tabular}{c}
          ${#2}$ \\ \hline
          ${#3}$ 
       \end{tabular}
    \end{tabular}}

\newcommand{\Rule}[3]{
   \begin{tabular}{cc}
      {\sc {#1}}
        &
       \begin{tabular}{c}
          ${#2}$ \\ \hline
          ${#3}$ 
       \end{tabular}
    \end{tabular}}

\newcommand{\TreeOne}[2]{
    \begin{tabular}{c}
          ${#1}$ \\ \hline
          ${#2}$ 
    \end{tabular}}

\newcommand{\TreeTwo}[3]{
    \begin{tabular}{c}
          ${#1}$ \hspace{10truemm} ${#2}$ \\ \hline
          ${#3}$ 
    \end{tabular}}

\newcommand{\TreeThree}[4]{
    \begin{tabular}{c}
          ${#1}$ \hspace{10truemm} ${#2}$ \hspace{10truemm} ${#3}$ \\ \hline
          ${#4}$ 
    \end{tabular}}

\newcommand{\TreeSpace}[2]{
    \begin{tabular}{c}
          ${#1}$ \\ 
          ${#2}$ 
    \end{tabular}}
