\parskip=5pt
\newcommand{\n}{\par \noindent}
\newcommand{\writeread}{\mbox{{\it writeread \/}}}

\newcommand{\writereadi}{\mbox{{\it writeread$_i$ \/}}}

\newcommand{\writereadv}{\mbox{{\it writeread($v,S$)$_{i,IS_x}$ \/}}}
\newcommand{\writereadvS}{\mbox{{\it writeread($v,S$)$_{i,IS_x}$ \/}}}
\newcommand{\inv}{\mbox{{\it inv\_writeread($v$)$_{i,IS_x}$ \/}}}
\newcommand{\start}{\mbox{{\it start \/}}}
\newcommand{\finish}{\mbox{{\it finish \/}}}
\newcommand{\starti}{\mbox{{\it start($v$)$_i$ \/}}}
\newcommand{\finishi}{\mbox{{\it finish($S$)$_i$ \/}}}
\newcommand{\isfinal}{\mbox{{\it is\_final\_state($v$)$_i$ \/}}}
\newcommand{\ret}{\mbox{{\it ret\_writeread($S$)$_{i,IS_x}$ \/}}}
\newcommand{\update}{\mbox{{\it update($\cU$) \/}}}
\newcommand{\ivalue}{\mbox{{\it input\_value \/}}}
\newcommand{\rvalue}{\mbox{{\it return\_value \/}}}
\newcommand{\interface}{\mbox{{\it interface \/}}}
\newcommand{\memory}{\mbox{{\it memory \/}}}
\newcommand{\ls}{\mbox{{\it local\_state \/}}}
\newcommand{\counter}{\mbox{{\it counter \/}}}
\newcommand{\isf}{\mbox{{\it is\_final\_state \/}}}
\newcommand{\decide}{\mbox{{\it decide \/}}}
\newcommand{\rvaluei}{\mbox{{\it return\_value[i] \/}}}
\newcommand{\ivaluei}{\mbox{{\it input\_value[i] \/}}}
\newcommand{\interfacei}{\mbox{{\it interface[i] \/}}}
\newcommand{\memoryi}{\mbox{{\it memory[i]\/}}}
%\newcommand{\dim}{\mbox{{\it dim\/}}}

\newcommand{\inva}{\mbox{{\it inv\_writeread($v$)$_{i,A}$ \/}}}
\newcommand{\reta}{\mbox{{\it ret\_writeread($S$)$_{i,A}$ \/}}}

