\renewcommand{\perp}{\bot}
\newcommand{\lf}{logical framework}
\newcommand{\defp}{\mbox{\textrm{def}}}
\newcommand{\xrq}{x R^i q}
%\renewcommand{\bar}{\|}
\newcommand{\ecs}{\circ}
\newcommand{\cS}{{\cal S}}
\newcommand{\ins}{<}
\newcommand{\block}[1]{\lceil #1\rceil}
\newcommand{\some}[1]{\mbox{\textrm{SOME}} \ {#1} .\, }
\newcommand{\sla}{\setminus}
\newcommand{\gap}{\GG';\cD'}
\newcommand{\inss}{\ins\cS}
\newcommand{\dsats}{\models_{\!\cS\bar\cS'} \!}
\newcommand{\dsato}{\models_{\!\cS_1} \!}
\newcommand{\dsat}{\models_{\!\cS} \!}
\newcommand{\dsatt}{\models_{\!\cS_2} \!}
\newcommand{\insss}{\ins\cS\bar\cS'}
%\renewcommand{\Box}{}
\newcommand{\mbar}{\|}
\newcommand{\gapp}{\GG\vd\GG';\cD'}
\newcommand{\eq}{\eqd}  
\newcommand{\yield}{\Rightarrow}
\renewcommand{\neq}{\not\eqd}
\newcommand{\alg}{aug_{\mbox{\tiny \textrm{G}}}}
\newcommand{\ald}{aug_{\mbox{\tiny \textrm{D}}}}
\newcommand{\gfald}{\ga\vd_{\!\Phi}\ald} %changed
\newcommand{\gfalg}{\Gamma;\cD\prv_{\!\Phi}\alg}
\newcommand{\mnota}{{\rm Not}_{\mbox{$\alpha$} }}
\newcommand{\mnotd}{{\rm Not}_{\rm D}  }
\newcommand{\mnotg}{{\rm Not}_{\rm G}  }
 \newcommand{\mnotxi}{\mnot^i_x}
\renewcommand{\sp}{\vd_{\!\cP}}
\newcommand{\PP}{\cP}
\newcommand{\PM}{\cP}
\newcommand{\spp}{\vd_{\!\PP}}
\newcommand{\snp}{\vd_{\!\PM}\mnotg}
\newcommand{\sn}{\vd_{\!\PM}}
%\newcommand{\PIXA}{\Pi x\!:\!A.\,}
%\newcommand{\exa}{\exists x\!:\!A.\,}
%\newcommand{\allxa}{\forall x\!:\!A.\,}
\newcommand{\fpp}{\nvd_{\!\PP}}
\newcommand{\fnp}{\nvd_{\!\PM}\mnotg }
\newcommand{\fn}{\nvd_{\!\PM}}
\newcommand{\fp}{\nvd_{\!\cP}}
\newcommand{\cA}{{\cal A}}
\newcommand{\cT}{{\cal T}}
\newcommand{\cJ}{{\cal J}}
\newcommand{\tensor}{\oplus}
\newcommand{\ga}{\Gamma;\cD }
\newcommand{\gna}{ \Gamma;\cD }
\newcommand{\vS}{\vec{S}}
%\newcommand{\vM}{\vec{M}}
\newcommand{\PA}{\mid \cP\mid}
\newcommand{\eqd}{\stackrel{\cdot}{=}}
\newcommand{\neqd}{\not\stackrel{\cdot}{=}}
\newcommand{\imm}{\mbox{$>\!\!>$}}
\newcommand{\notimm}{\mbox{$\not >\!\!>$}}
\newcommand{\nimm}{\imm}
\newcommand{\IP}{{\cal I}^{+}}
\newcommand{\IM}{{\cal I}^{-}}
\newcommand{\SP}{{\cal S}^{+}}
\newcommand{\SM}{{\cal S}^{-}}
%\newcommand{\gf}{\Gamma;\cD\vd_{\!\Phi}^{\! Q}} CHANGE (Input
%variables \Phi
\newcommand{\gf}{\Gamma\vd}
%\newcommand{\gf}{\Gamma\vd^{\! Q}}
\newcommand{\fa}{ \,\ \mbox{\rm {f.a.\ }}}
\newcommand{\gfq}{\GG\vd}
%\newcommand{\gfq}{q\oftp \An\Imp\prop\vd}
% \newcommand{\vdf}{\vd_{\!\Phi}} input variables
\newcommand{\vdf}{\vd_{\!\cP}}
\newcommand{\foq}{\mbox{\textrm{for all }$ \q$  }}
%\renewcommand{\emp}{\cdot;\top}
\newcommand{\csa}{\cS^a}
\newcommand{\yd}{\stackrel{\mbox{\tiny{$D$}}}{\Longrightarrow}}
\newcommand{\yg}{\stackrel{\mbox{\tiny{$G$}}}{\Longrightarrow}}
\newcommand{\less}{\prec} 
\newcommand{\boxarray}[1]{\[\fbox{$\begin{array}
      {c}\mbox{}\vsk #1\mbox{}\vsk\end{array}$}\]}
% call with the context of the array
\newcommand{\fixed}{}
\newcommand{\added}{}
%\newcommand{\fixed}{\footnote{\normalsize\textbf{FIXED}}}
%\newcommand{\added}{\footnote{\normalsize\textbf{ADDED}}}
\newcommand{\lop}{-\!\!\circ}
\newcommand{\pol}{\circ\!\!-}
\renewcommand{\Pi}{\forall}  %%% all for pi
\newcommand{\Pixa}{\PI{x}{a}D}
\newcommand{\qmx}{q \ \ol{M_{\ex}^i}}
\newcommand{\inn}{\sqsubseteq}

