-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathnotation.tex
More file actions
143 lines (108 loc) · 4.7 KB
/
notation.tex
File metadata and controls
143 lines (108 loc) · 4.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
%!TEX root = dissertation.tex
\usepackage{amsmath,amssymb,amsthm}
\usepackage{graphicx}
\usepackage{stmaryrd}
\usepackage{nicefrac}
\theoremstyle{plain}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{proposition}{Proposition}
\newtheorem{conjecture}{Conjecture}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\theoremstyle{remark}
\newtheorem{note}{Note}
\newtheorem*{remark}{Remark}
\newcommand{\bnfbar}{\ensuremath{~|~}}
\newcommand{\bnfdef}{\ensuremath{~::=~}}
%% set notation
\newcommand{\set}[1]{\left\lbrace #1 \right\rbrace}
\newcommand{\setof}[2]{\set{#1 \mid #2}}
\newcommand{\bigset}[1]{\left\lbrace #1 \right\rbrace}
\newcommand{\bigsetof}[2]{\bigset{#1 \mid #2}}
\DeclareMathOperator{\funcompat}{\smile}
\newcommand{\mtab}{\ensuremath{\;\;\;}}
\newcommand{\powerset}[1]{\ensuremath{\mathcal{P}(#1)}}
\newcommand{\zorch}{\ensuremath{\lightning}}
\DeclareMathOperator{\opdom}{\mathrm{dom}}
\newcommand{\dom}[1]{\ensuremath{\opdom(#1)}}
\newcommand{\bvt}{\ensuremath{\mathbf{t}}}
\newcommand{\bvf}{\ensuremath{\mathbf{f}}}
\newcommand{\llen}[1]{\ensuremath{|#1|}}
\newcommand{\llit}[1]{\ensuremath{\left[#1\right]}}
\newcommand{\lnil}[0]{\ensuremath{\varepsilon}}
\newcommand{\arnil}[0]{\ensuremath{\mathcal{E}}}
\newcommand{\elems}[1]{\ensuremath{|\!|#1|\!|}}
\newcommand{\funof}[1]{\ensuremath{\overline{#1}}}
\DeclareMathOperator{\lapp}{+\!\!\!+}
\DeclareMathOperator{\lcons}{:\!:}
\newcommand{\lhead}[1]{\ensuremath{\mathit{hd}(#1)}}
\newcommand{\ltail}[1]{\ensuremath{\mathit{tl}(#1)}}
\newcommand{\nth}[2]{\ensuremath{#2 ! #1}}
\newcommand{\listof}[1]{\ensuremath{#1~\mathsf{list}}}
\newcommand{\relset}[1]{\ensuremath{|#1|}}
\newcommand{\ext}[1]{\ensuremath{\hat{#1}}}
\newcommand{\restrict}[2]{\ensuremath{#1 |_{#2}}}
\newcommand{\proj}[2]{\ensuremath{#1 |_{#2}}}
\newcommand{\reclit}[1]{\ensuremath{\set{#1}}}
\DeclareMathOperator{\tfun}{\rightarrow}
\DeclareMathOperator{\pfun}{\rightharpoonup}
\DeclareMathOperator{\fpfun}{\pfun_{\mathrm{fin}}}
\DeclareMathOperator{\st}{\,:\,}
\newcommand{\ptup}[2]{\ensuremath{#1 \shortleftarrow #2}}
\newcommand{\funup}[2]{\ensuremath{#1\! \left[ #2 \right]}}
\newcommand{\fundel}[2]{\ensuremath{#1 \setminus#2 }}
\newcommand{\recup}[3]{\funup{#1}{\ptup{#2}{#3}}}
\newcommand{\ptapp}[2]{\ensuremath{#1 \lapp #2}}
\DeclareMathOperator{\conj}{\,\wedge\,}
\DeclareMathOperator{\disj}{\,\vee\,}
\DeclareMathOperator{\onlyif}{\,\Rightarrow\,}
%\DeclareMathOperator{\ifandonlyif}{\,\Longleftrightarrow\,}
\renewcommand{\iff}{\ensuremath{\Leftrightarrow}}
\newcommand{\fresh}[1]{\ensuremath{\mathrm{fresh}(#1)}}
\newcommand{\subst}[2]{\ensuremath{\left[#1 / #2\right]}}
\newcommand{\unsubst}[2]{\ensuremath{\left[#1 \backslash #2\right]}}
\newcommand{\eqclass}[1]{\ensuremath{\left[ #1 \right]}}
\DeclareMathOperator{\downop}{\downarrow}
\newcommand{\downo}[2]{\ensuremath{\downop_{#1}\!#2}}
\newcommand{\down}[1]{\ensuremath{\downop #1}}
%% Calculational proofs
\newcommand{\Calc}[1]{\begin{description}
\item \begin{tabbing}\qquad\=\quad\=\kill
\> \> #1\end{tabbing}
\end{description}}
\newcommand{\Sketch}[1]{\begin{description}
\item \begin{tabbing}\qquad\=\quad\=\kill
#1\end{tabbing}
%\> \> #1\end{tabbing}
\end{description}}
\newcommand{\aconn}[1]{\{#1\}\\ }
\newcommand{\aconnl}[1]{\{#1\} }
\newcommand{\aconnt}[1]{\{#1\} $\therefore$\\ }
\newcommand{\aconni}[1]{\> \{#1\}\\ }
\newcommand{\acomm}[1]{\> #1 \\}
\newcommand{\conn}[2]{\\*$#1 $\> \{#2\}\\\> \>}
\newcommand{\Conn}[1]{\conn{=}{#1}}
\newcommand{\ident}[1]{\ensuremath{\mathit{Id}_{#1}}}
\DeclareMathOperator{\rcomp}{\circ}
\newcommand{\relexp}[2]{\ensuremath{\stackrel{#2}{#1}}}
\newcommand{\tcl}[1]{\overset{+}{#1}}
\newcommand{\rtcl}[1]{\overset{\ast}{#1}}
\newcommand{\image}[2]{\ensuremath{#1\left[#2\right]}}
\newcommand{\invimage}[2]{\ensuremath{#1^{-1}\left[#2\right]}}
\newcommand{\lift}[1]{\ensuremath{\mathit{lift}_{#1}}}
\renewcommand{\merge}{\ensuremath{\uplus}}
% \newcommand{\override}{\reflectbox{\rotatebox[origin=c]{180}{\ensuremath{\,\oslash\,}}}}
\newcommand{\override}{\ensuremath{\backslash\!\!\backslash}}
\newcommand{\sentails}{\ensuremath{\,\models\,}}
\newcommand{\satisfies}{\ensuremath{\,\models\,}}
\newcommand{\sequiv}{\ensuremath{\,\equiv\,}}
\newcommand{\fixme}[1]{\todo{FIXME: #1}}
\DeclareMathOperator{\eqdef}{\;=_{\mathit{df}}\;}
\DeclareMathOperator{\iffdef}{\;\equiv_{\mathit{df}}\;}
\newcommand{\card}[1]{\left|#1\right|}
\newcommand{\cmpl}[1]{\ensuremath{\overline{#1}}}
\newcommand{\refines}{\ensuremath{\sqsubseteq}}
\newcommand{\range}[1]{\ensuremath{\mathit{range}(#1)}}
\newcommand{\fun}[1]{\ensuremath{\lambda#1\,.\,}}