1 %\DeclareSymbolFont{stmary}{U}{stmary}{m}{n}
2 %\DeclareFontFamily{U}{stmary}{}%
3 %\DeclareFontShape{U}{stmary}{m}{n}{<-6>stmary5<6-8>stmary7<8->stmary10}{}%
4 %\DeclareMathSymbol{\odb}{\mathopen}{stmary}{"4A}
5 %\DeclareMathSymbol{\cdb}{\mathclose}{stmary}{"4B}
10 % LOGIC %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16 \def\spc{\hspace{1em}} % 0.25em per la tesi
18 \def\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}
19 \def\gdlap#1#2{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
20 \def\?#1{\mathord{#1}}
24 \def\imain#1{{\offinterlineskip\lineskip=2pt\noindent
25 \hbox{$\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
26 \def\itree#1{{\offinterlineskip\lineskip=2pt\noindent
27 \hbox{$\vbox{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
29 \def\setnames@#1#2{&\gdlap{\kern2pt$#1$}{#2}}
30 \def\iname#1 {\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
31 \def\inames#1 {\cr\hrulefill\cr\hrulefill\setnames@{#1}{-1.2ex}\cr}
32 \def\ivrule{\cr\vrule height 3ex \cr}
33 \def\discharge#1#2 {\iname{#1\,#2} }
34 \def\assume#1#2{\ov #1\cv\rlap{$^{#2}$}}
38 \def\irule#1#2#3{\imain{#1 \iname{#2} #3 }} % "single step"
39 \def\irules#1#2#3{\imain{#1 \inames{#2} #3 }} % "multistep"
41 \def\drule#1#2#3{\itree{#1 \iname{#2} #3 }} % "single step"
42 \def\drules#1#2#3{\itree{#1 \inames{#2} #3 }} % "multistep"
44 \def\cirule#1#2#3{$\vcenter{\irule{#1}{#2}{#3}}$} % "single step"
45 \def\cirules#1#2#3{$\vcenter{\irules{#1}{#2}{#3}}$} % "multistep"
47 % MATHEMATICS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
56 \def\jolly{\mathbin\square}
60 \def\lexcl{\mathrel\leftarrow}
61 \def\limp{\mathrel\rightarrow}
62 \def\liff{\mathrel\leftrightarrow}
64 \def\lplus{\mathrel\oplus}
65 \def\ltimes{\mathrel\otimes}
68 \def\lpar{\mathrel\bindnasrepma}
69 \def\lamp{\mathrel\binampersand}
77 \def\simp{\Rightarrow}
84 \def\after{\mathbin\circ}
86 \def\e{\mathrel\epsilon}
91 \def\yld{\mathrel\vdash}
92 \def\Frm{\textsf{Frm}}
93 \def\Trm{\textsf{Trm}}
96 \def\LBmi{{\bf B}$^-_{\limp}$}
97 \def\LBmiq{{\bf B}$^-_{\limp\lexcl\lall\lex}$}
101 \def\mand{\mathrel{\textbf{and}}}
102 \def\miff{\mathrel{\textbf{iff}}}
103 \def\mimp{\mathrel{\textbf{implies}}}
104 \def\mpiff{\mathrel{\textbf{\frenchspacing prim. iff}}}
105 \def\mpimp{\mathrel{\textbf{\frenchspacing prim. implies}}}
106 \def\mtrue{\mathord{\textbf{true}}}
107 \def\mall{\mathrel{\textbf{all}}}
109 % TEXT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
111 \def\EM#1{\noindent\hbox{\frenchspacing\em #1}}
112 \def\TT#1{\noindent\hbox{\frenchspacing\tt #1}}
113 \def\RM#1{\noindent\hbox{\frenchspacing\rm #1}}
114 \def\URI#1{\texttt{<#1>}}
116 \def\ie{{\frenchspacing i.e.}}
118 \long\def\xcomment#1{}
119 \def\proc{{\frenchspacing proc.}}
120 \def\etc{{\frenchspacing etc.}}
121 \def\po{{\frenchspacing p.o.}}