%\DeclareSymbolFont{stmary}{U}{stmary}{m}{n}
%\DeclareFontFamily{U}{stmary}{}%
%\DeclareFontShape{U}{stmary}{m}{n}{<-6>stmary5<6-8>stmary7<8->stmary10}{}%
%\DeclareMathSymbol{\odb}{\mathopen}{stmary}{"4A}
%\DeclareMathSymbol{\cdb}{\mathclose}{stmary}{"4B}

\usepackage{amssymb}
\usepackage{stmaryrd}

% LOGIC  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

% utilities

\def\cv{\,]}
\def\ov{[\,}
\def\spc{\hspace{1em}} % 0.25em per la tesi
\def\nop{{}}
\def\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}
\def\gdlap#1#2{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
\def\?#1{\mathord{#1}}

% inference trees

\def\imain#1{{\offinterlineskip\lineskip=2pt\noindent
  \hbox{$\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
\def\itree#1{{\offinterlineskip\lineskip=2pt\noindent
  \hbox{$\vbox{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}

\def\setnames@#1#2{&\gdlap{\kern2pt$#1$}{#2}} 
\def\iname#1 {\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
\def\inames#1 {\cr\hrulefill\cr\hrulefill\setnames@{#1}{-1.2ex}\cr}
\def\ivrule{\cr\vrule height 3ex \cr}
\def\discharge#1#2 {\iname{#1\,#2} }
\def\assume#1#2{\ov #1\cv\rlap{$^{#2}$}}

% single rules

\def\irule#1#2#3{\imain{#1 \iname{#2} #3 }}   % "single step"
\def\irules#1#2#3{\imain{#1 \inames{#2} #3 }} % "multistep"

\def\drule#1#2#3{\itree{#1 \iname{#2} #3 }}   % "single step"
\def\drules#1#2#3{\itree{#1 \inames{#2} #3 }} % "multistep"

\def\cirule#1#2#3{$\vcenter{\irule{#1}{#2}{#3}}$}   % "single step"
\def\cirules#1#2#3{$\vcenter{\irules{#1}{#2}{#3}}$} % "multistep"

% MATHEMATICS  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\a{\phi}
\def\b{\psi}
\def\c{\xi}
\def\d{\eta}
\def\A{\Phi}
\def\B{\Psi}
\def\C{\Xi}
\def\jolly{\mathbin\square}
\def\lall{\forall}
\def\lex{\exists}
\def\lbot{{\bot}}
\def\lexcl{\mathrel\leftarrow}
\def\limp{\mathrel\rightarrow}
\def\liff{\mathrel\leftrightarrow}
\def\lone{1}
\def\lplus{\mathrel\oplus}
\def\ltimes{\mathrel\otimes}
\def\ltop{{\top}}
\def\lzero{0}
\def\lpar{\mathrel\bindnasrepma}
\def\lamp{\mathrel\binampersand}

\def\meet{\between}
\def\bigsor{\bigcup}
\def\bigsand{\bigcap}
\def\sand{\cap}
\def\sdor{\sqcup}
\def\sor{\cup}
\def\simp{\Rightarrow}
\def\snot{-}
\def\sub{\subseteq}
\def\sup{\supseteq}
\def\sbot{\emptyset}
\def\stop{\ltop}

\def\after{\mathbin\circ}
\def\app{\mathbin @}
\def\e{\mathrel\epsilon}
\def\oft{\mathrel :}
\def\p{{^\prime}}
\def\st{\mathrel |}
\def\subset#1{\{#1\}}
\def\yld{\mathrel\vdash}
\def\Frm{\textsf{Frm}}
\def\Trm{\textsf{Trm}}
\def\LB{{\bf B}}
\def\LBm{{\bf B}$^-$}
\def\LBmi{{\bf B}$^-_{\limp}$}
\def\LBmiq{{\bf B}$^-_{\limp\lexcl\lall\lex}$}
\def\LBLS{{\bf BLS}}
\def\P{{\cal P}}

\def\mand{\mathrel{\textbf{and}}}
\def\miff{\mathrel{\textbf{iff}}}
\def\mimp{\mathrel{\textbf{implies}}}
\def\mpiff{\mathrel{\textbf{\frenchspacing prim. iff}}}
\def\mpimp{\mathrel{\textbf{\frenchspacing prim. implies}}}
\def\mtrue{\mathord{\textbf{true}}}
\def\mall{\mathrel{\textbf{all}}}

% TEXT  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\EM#1{\noindent\hbox{\frenchspacing\em #1}}
\def\TT#1{\noindent\hbox{\frenchspacing\tt #1}}
\def\RM#1{\noindent\hbox{\frenchspacing\rm #1}}
\def\URI#1{\texttt{<#1>}}

\def\ie{{\frenchspacing i.e.}}
\def\df#1{{\bf #1}}
\long\def\xcomment#1{}
\def\proc{{\frenchspacing proc.}}
\def\etc{{\frenchspacing etc.}}
\def\po{{\frenchspacing p.o.}}
