\def\mybigsqcap{\mathop{\rule[-0.2ex]{.07em}{2.17ex}
                \rule[1.8ex]{0.5em}{.17ex}
                \rule[-0.2ex]{.07em}{2.17ex}}}

% comment a region

\newcommand{\punt}[1]{}

\newcommand{\remove}[1]{}


% a word should not be broken across lines

\newcommand{\nosplit}[1]{\linebreak \mbox{#1}}

% ~ character

\newcommand{\tilda}{\symbol{126}}


% use for defining a concept first time

%\newcommand{\defn}[1]{{\em #1}}

% useful mathematical symbols

\newcommand{\ang}[1]{\langle #1 \rangle}
\newcommand{\ceil}[1]{\lceil #1 \rceil}
\newcommand{\floor}[1]{\lfloor #1 \rfloor}


% for formally defining a notion

\newcommand{\defined}{\;\stackrel{\triangle}{=}\;}

%\newcommand{\implies}{\Rightarrow}
\newcommand{\follows}{\Leftarrow}
\newcommand{\ra}{\rightarrow}
\newcommand{\myequiv}{\simeq}

% theorem environment

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}
%\newtheorem{proposition}{Proposition}
%\newtheorem{obs}{Observation}

\newcommand{\bfr}{\begin{flushright}}
\newcommand{\efr}{\end{flushright}}

\newcommand{\ep}{\bfr {\ \rule{2mm}{2mm}} \efr} 
\newcommand{\rae}{\underline {\rightarrow}}
\newcommand{\cut}[1]{\newtie{#1}}

\newenvironment{proof}{{\bf Proof:}}{\ep}
\newcommand{\ind}{\null\quad}
\newcommand{\Ra}{\Rightarrow}

\newtheorem{condition}{Condition}
% environment for writing a proof

%\newcommand{\proof}[1][]{\noindent{\itshape Proof{#1}:}\hspace*{0.5em}}

\newcommand{\proofsketch}[1][]{\noindent{\itshape Proof Sketch{#1}:}\hspace*{0.5em}}
% \newcommand{\qed}{\hspace*{\fill}\nolinebreak[1]~~~\hspace*{\fill}
%                   \rule{5pt}{5pt}\vspace*{\topsep}\vspace*{\parskip}
%                   \vspace*{\partopsep}}   

%\def\qed{\quad \vrule height7.5pt width4.17pt depth0pt} 

%\newcommand{\qed}{\hspace*{\fill}\nolinebreak[1]~~~\hspace*{\fill}
%                  \rule{5pt}{5pt}\vspace*{\topsep}\vspace*{\parskip}
%                  \vspace*{\partopsep}}
                     
\newcommand{\eosqed}{\hfill \rule{5pt}{5pt}}


% various references

\newcommand{\secref}[1]{Section~\ref{sec:#1}}
\newcommand{\figref}[1]{Figure~\ref{fig:#1}}
\newcommand{\tabref}[1]{Table~\ref{tab:#1}}
\newcommand{\stref}[1]{step~\ref{step:#1}}
\newcommand{\thmref}[1]{Theorem~\ref{thm:#1}}
\newcommand{\lemref}[1]{Lemma~\ref{lem:#1}}
\newcommand{\mcorref}[1]{Corollary~\ref{cor:#1}}
\newcommand{\defref}[1]{Definition~\ref{def:#1}}
%\newcommand{\eqref}[1]{Equation~(\ref{eq:#1})}
\newcommand{\eqvref}[1]{Equivalence~(\ref{eqv:#1})}
\newcommand{\ineqref}[1]{Inequality~(\ref{ineq:#1})}

\newcommand{\compt}{\langle E, \rightarrow \rangle}
%\newcommand{\compt}{G}
\newcommand{\final}{\cal{E}}
\newcommand{\C}{{\cal C}}
\newcommand{\mypath}{{\cal P}}
\newcommand{\cpath}{\mypath(\compt)}
\newcommand{\rcut}{\mathcal{R}(p)}
\newcommand{\unroll}[1]{\mathscr{U}(Q, #1)}
\newcommand{\iso}[1]{\mathcal{I}_{#1}}
\newcommand{\onext}[1]{\mathbf{next} \{ #1 \}}
\newcommand{\tr}{\;{ \triangleright }\;}
\newcommand{\treq}{\;\underline{ \triangleright }\;}

\newcommand{\A}{\mathbf{A}}
\newcommand{\E}{\mathbf{E}}
\newcommand{\U}{\mathbf{U}}
\newcommand{\AF}{\mathbf{AF}}
\newcommand{\AG}{\mathbf{AG}}
\newcommand{\EF}{\mathbf{EF}}
\newcommand{\EG}{\mathbf{EG}}
\newcommand{\EU}{\mathbf{EU}}
\newcommand{\AU}{\mathbf{AU}}
\newcommand{\EX}{\mathbf{EX}}
\newcommand{\AX}{\mathbf{AX}}
\newcommand{\possibly}[1]{{possibly\!:}\:{#1}}
\newcommand{\Possibly}[1]{{Possibly\!:}\:{#1}}
\newcommand{\definitely}[1]{{de\!f\!initely\!:}\:{#1}}
\newcommand{\Definitely}[1]{{De\!f\!initely\!:}\:{#1}}
\newcommand{\controllable}[1]{{contr\!ollable\!:}\:{#1}}
\newcommand{\Controllable}[1]{{Contr\!ollable\!:}\:{#1}}
\newcommand{\invariant}[1]{{invariant\!:}\:{#1}}
\newcommand{\Invariant}[1]{{Invariant\!:}\:{#1}}

% modalities

\newcommand{\Mdefinitely}{{de\!f\!initely}}
\newcommand{\Mpossibly}{{possibly}}
\newcommand{\Minvariant}{{invariant}}
\newcommand{\Mcontrollable}{{contr\!ollable}}

\newcommand{\until}{\textit{until} }
%\newcommand{\depgraph}{\mathit{dependency\_graph}}
%\newcommand{\compgraph}{\mathit{complementary\_graph}}
\newcommand{\depgraph}{G_{(e,f)}}
\newcommand{\compgraph}{G_{(e,f)}^c}

\newcommand{\hb}{\rightarrow}
\newcommand{\hbeq}{\reflexive{\hb}}
\newcommand{\nhb}{\!\not\hb}
\newcommand{\nhbeq}{\!\not\!\!\reflexive{\hb}}

\newcommand{\comptn}[3][]{\ang{{#2},{#3}}_{#1}}


\newcommand{\po}[1]{\arrows{#1}{P}}
\newcommand{\poeq}[1]{\arrows{\reflexive{#1}}{P}}

\newcommand{\arrows}[2]{\stackrel{\mbox{\tiny $#2$}}{#1}}
\newcommand{\arrowseq}[2]{\stackrel{\mbox{\tiny $#2$}}{\reflexive{#1}}} 

\newcommand{\reflexive}[1]{\underline{#1}}
\newcommand{\frontier}[1]{f\!rontier(#1)}
\newcommand{\exref}[1]{Example~\ref{ex:#1}}
\newcommand{\apnref}[1]{Appendix~\ref{apn:#1}}
\newcommand{\slice}[2]{\mbox{\sf slice}(#1,#2)}
% predicates true and false

\newcommand{\true}{\ensuremath {\sf true }}
\newcommand{\false}{\ensuremath {\sf false }}

%\newtheorem{example}{Example}
%\renewcommand{\theexample}{\arabic{example}}


% lattice notions

\newcommand{\join}{\, \sqcup \,}
\newcommand{\meet}{\, \sqcap \,}
\newcommand{\sjoin}{\mbox{\Large $\sqcup$}\:}
\newcommand{\smeet}{\mbox{\Large $\sqcap$}\:}



% In case the example is immediately followed by the start of a new section

\newcommand{\Figref}[1]{Figure~\ref{fig:#1}}


% notions associated with an event

\newcommand{\proc}[1]{proc(#1)}
\renewcommand{\succ}[1]{succ(#1)}
\newcommand{\pred}[1]{pred(#1)}


\newcommand{\vertices}[1]{\mbox{\sf V}({#1})}
\newcommand{\edges}[1]{\mbox{\sf E}({#1})}
\newcommand{\cuts}[2][]{\mathcal{C}_{#1}({#2})}
\newcommand{\cutsz}[1][]{\mathcal{C}_{#1}}
\newcommand{\paths}[1]{\mathcal{P}({#1})}
\newcommand{\ji}[1]{\mathcal{JI}({#1})}
\newcommand{\joins}[2][]{\mathcal{J}_{#1}({#2})}
\newcommand{\skeletal}[2][]{\mathcal{S}_{#1}(#2)}
\newcommand{\canonical}[2][]{\mathcal{G}_{#1}(#2)}


\newcommand{\fvector}[2][]{F_{#1}(#2)}
\newcommand{\jvector}[2][]{J_{#1}(#2)}
\newcommand{\kvector}[2][]{K_{#1}(#2)}

\newcommand{\fvectorz}[1][]{F_{#1}}
\newcommand{\jvectorz}[1][]{J_{#1}}
\newcommand{\kvectorz}[1][]{K_{#1}}

\newcommand{\jvectorx}[3][]{J_{#1}^{#3}(#2)}
\newcommand{\fvectorx}[3][]{F_{#1}^{#3}(#2)}

\newcommand{\found}{f\!ound}

\newcommand{\addpath}[3]{{#1}[#2,#3]}



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
