\input{vijay-macros} 

\def\OO{{\cal O}}
\def\DD{{\cal D}}
\def\AA{{\cal A}}
\def\PP{{\cal P}}
\def\CC{{\cal C}}

\def\tcc{{\ccfont tcc}}
\def\SKIP{{\bf skip}}
\def\Lustre{{\sc Lustre}}
\def\Signal{{\sc Signal}}
\def\Esterel{{\sc Esterel}}
\def\halt{\mbox{\bf halt}}
\def\always{\mbox{\bf always }}
\def\Obs{{\bf Obs}}
\def\OBS{{\bf Obs}}
\def\PROC{{\bf Proc}}
\def\CHAOS{{\bf Chaos}}
\def\by#1#2#3#4{#1\ \mbox{\bf by}\ #2\ \mbox{\bf then}\ #3\ \mbox{\bf else}\ #4}
\def\nowte#1\then#2\else#3{\mbox{\bf now}\ #1\ \mbox{\bf then}\ #2\  \mbox{\bf else}\ #3}
\def\do#1\watching#2\timeout#3{\mbox{\bf do}\ #1\ \mbox{\bf watching}\ #2\  \mbox{\bf timeout}\ #3}
\def\dow#1\watching#2{\mbox{\bf do}\ #1\ \mbox{\bf watching}\ #2}
\def\att#1#2\then#3{\mbox{\bf at}\ #1\ #2\ \mbox{\bf then}\  #3}
\def\ate#1#2\else#3{\mbox{\bf at}\ #1\ #2\ \mbox{\bf else}\  #3}
\def\case#1\do#2{\mbox{\bf case}\ #1\ \mbox{\bf do} #2}
\def\lub{\sqcup}
\def\loop#1\end{\mbox{\bf loop}\ #1\ \mbox{\bf end}}
\def\ccfd{{\sf cc}({\cc FD})}
\def\nowt#1\then#2{\mbox{\bf now}\ #1\ \mbox{\bf then}\ #2}
\def\whenever#1\do#2{\mbox{\bf whenever}\ #1\ \mbox{\bf do}\ #2}
\def\nowe#1\else#2{\mbox{\bf now}\ #1\ \mbox{\bf else}\ #2}
\def\next#1{\mbox{\bf next}\ #1}
\def\default#1{\mbox{\bf default}\ #1}
\def\within#1#2\then#3\else#4{#2\ \mbox{\bf in}\ #1\ \mbox{\bf then}\ #3\ \mbox{\bf else}\ #4}
\def\withint#1#2\then#3{#2\ \mbox{\bf in}\ #1\ \mbox{\bf then}\ #3}
\def\withine#1#2\else#3{#2\ \mbox{\bf in}\ #1\ \mbox{\bf else}\ #3}
\def\defeq{\withmath{\stackrel{d}{=}}}
% \def\within#1#2#3#4{#1\ \mbox{\bf in}\ #2\ \mbox{\bf then}\ #3\ \mbox{\bf else}\ #4}

\newcommand{\derivrule}[3]{\begin{array}{c} #1\\ \hline #2\end{array}
\mbox{ (#3)}}
\newcommand{\sequent}[2]{#1 \hspace{1mm}\vdash\hspace{.5mm} #2}


\makeatletter 
{\@definecounter{MetaNote}\@addtoreset{MetaNote}{section}% 
\expandafter\xdef\csname theMetaNote\endcsname{\expandafter\noexpand 
  \csname thesection\endcsname \@thmcountersep \@thmcounter{MetaNote}}% 
\global\long\def\MetaNote#1{{\@thm{MetaNote}{MetaNote} #1\@endtheorem}}} 
{\@definecounter{TechComm}\@addtoreset{TechComm}{section}% 
\expandafter\xdef\csname theTechComm\endcsname{\expandafter\noexpand 
  \csname thesection\endcsname \@thmcountersep \@thmcounter{TechComm}}% 
\global\long\def\TechComm#1{{\@thm{TechComm}{Note to Reviewer:} #1\@endtheorem}}} 
 
%% In case you want Meta-notes not to  appear in the printed 
%% text. e.g. in final version, remove the following %% signs: 
%% \long\def\MetaNote#1{\relax} 
\makeatother 
\def\dn{\downarrow}
\def\do#1\watching#2\timeout#3{\mbox{\bf do}\ #1\ \mbox{\bf watching}\ #2\
\mbox{\bf timeout}\ #3}
\newcommand{\Now}{\mbox{ \bf now }}
\newcommand{\Case}{\mbox{ \bf case }}
\newcommand{\Default}{\mbox{ \bf default }}
\newcommand{\Next}{\mbox{ \bf next }}
\newcommand{\Then}{\mbox{ \bf then }}
\newcommand{\Else}{\mbox{ \bf else }}
\newcommand{\Before}{\mbox{ \bf before }}
\newcommand{\Watching}{\mbox{ \bf watching }}
\newcommand{\While}{\mbox{ \bf while }}
\newcommand{\Do}{\mbox{ \bf do }}
\newcommand{\Timeout}{\mbox{ \bf timeout }}
\newcommand{\Whenever}{\mbox{ \bf whenever }}

\newcommand{\timederives}{\withmath{\leadsto}}
\def\nowtm#1\then#2{\mbox{\bf now}_e\ #1\ \mbox{\bf then}_e\ #2}
\def\nowem#1\else#2{\mbox{\bf now}_e\ #1\ \mbox{\bf else}_e\ #2}
\newcommand{\dowt}[3]{\mbox{\bf do}\ #1\ \mbox{\bf watching}\ #2\  \mbox{\bf timeout}\ #3}