blob: ed34c4164434276274a9bfc41b759deae0b4a2f6 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
\usepackage{prooftree}
\newenvironment{while}{\medskip\noindent}{\medskip}
\def\whskip{\texttt{skip}}
\def\whass#1#2{\texttt{#1 := #2}}
\def\whcomp#1#2{#1\texttt{;} #2}
\def\whif#1#2#3{\texttt{if~}#1\texttt{~then~}#2\texttt{~else~}#3}
\def\whwhile#1#2{\texttt{while~}#1\texttt{~do~}#2}
\def\whnot#1{\texttt{$\lnot$#1}}
\def\whnotp#1{\texttt{$\lnot$(#1)}}
\def\whle#1#2{\texttt{#1$\le$#2}}
\def\axjustifies{\thickness0em\justifies}
\def\trans#1#2#3{\left\langle#1,#2\right\rangle\rightarrow#3}
\def\smbox#1{\mbox{\footnotesize{#1}}}
\def\rcompns{[\mbox{comp}_{\smbox{ns}}]}
\def\rassns{[\mbox{ass}_{\smbox{ns}}]}
\def\rifttns{[\mbox{if}^{\smbox{tt}}_{\smbox{ns}}]}
|
