-
Notifications
You must be signed in to change notification settings - Fork 32
/
pvs-tex.sub
275 lines (258 loc) · 7.42 KB
/
pvs-tex.sub
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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
-> key 2 \rightarrow
<- key 2 \leftarrow
exists key 1 \exists
forall key 1 \forall
lambda key 1 \lambda
| key 2 \mbox{ }|\mbox{ }
=> id 2 \Rightarrow
>= id 2 \geq
> id 1 >
<= id 2 \leq
< id 1 <
/= id 2 \neq
= id 2 =
& id 1 \&
<=> id 2 \Leftrightarrow
* id 1 \times
+ id 1 +
- id 1 -
/ id 1 /
<< id 1 \ll
>> id 1 \gg
IMPLIES id 1 {\pvskey{IMPLIES}}
AND id 1 {\pvskey{AND}}
OR id 1 {\pvskey{OR}}
NOT id 1 {\pvskey{NOT}}
IFF id 2 {\pvskey{IFF}}
XOR id 3 {\pvskey{XOR}}
WHEN id 4 {\pvskey{WHEN}}
FALSE id 5 {\pvskey{FALSE}}
TRUE id 4 {\pvskey{TRUE}}
IF id 2 {\pvskey{IF}}
/\ id 1 \wedge
\/ id 1 \vee
== id 1 \equiv
[] id 1 \Box
<> id 1 \Diamond
~ id 1 {\char126}
<| id 1 \lhd
|> id 1 \rhd
|= id 1 \models
alpha id 1 \alpha
beta id 1 \beta
gamma id 1 \gamma
delta id 1 \delta
epsilon id 1 \varepsilon
zeta id 1 \zeta
eta id 1 \eta
theta id 1 \theta
iota id 1 \iota
kappa id 1 \kappa
mu id 1 \mu
nu id 1 \nu
xi id 1 \xi
pi id 1 \pi
rho id 1 \rho
sigma id 1 \sigma
tau id 1 \tau
upsilon id 1 \upsilon
phi id 1 \phi
chi id 1 \chi
psi id 1 \psi
omega id 1 \omega
Gamma id 1 \Gamma
Delta id 1 \Delta
Theta id 1 \Theta
Xi id 1 \Xi
Pi id 1 \Pi
Sigma id 1 \Sigma
Upsilon id 1 \Upsilon
Phi id 1 \Phi
Psi id 1 \Psi
Omega id 1 \Omega
GAMMA id 1 \Gamma
DELTA id 1 \Delta
THETA id 1 \Theta
XI id 1 \Xi
PI id 1 \Pi
SIGMA id 1 \Sigma
UPSILON id 1 \Upsilon
PHI id 1 \Phi
PSI id 1 \Psi
OMEGA id 1 \Omega
+ 2 1 {#1+#2}
- 2 1 {#1-#2}
- 1 1 {-#1}
* 2 1 {#1\times#2}
/ 2 1 {#1 / #2}
O 2 1 {#1\circ#2}
sets.member 2 1 {(#1 \in #2)}
sets.member 0 4 {(\star1 \in \star2)}
emptyset id 1 {\emptyset}
sets.subset? 2 1 {(#1 \subseteq #2)}
sets.strict_subset? 2 1 {(#1 \subset #2)}
sets.union 2 1 {(#1 \cup #2)}
sets.intersection 2 1 {(#1 \cap #2)}
sets.complement 1 1 {\overline{#1}}
sets.difference 2 1 {(#1 \setminus #2)}
sets.add 2 2 {(#2 \cup \{#1\})}
sets.remove 2 2 {(#2 \setminus \{#1\})}
sets.Union 1 1 {\bigcup #1}
sets.Intersection 1 1 {\bigcap #1}
indexed_sets.IUnion 1 1 {\bigcup #1}
indexed_sets.IIntersection 1 1 {\bigcap #1}
[ id 1 {\pvsbracketl}
] id 1 {\pvsbracketr}
[# id 2 {\pvsrectypel}
#] id 2 {\pvsrectyper}
\( id 1 {\pvsparenl}
\) id 1 {\pvsparenr}
[| id 1 {\pvsbrackvbarl}
|] id 1 {\pvsbrackvbarr}
\(| id 1 {\pvsparenvbarl}
|\) id 1 {\pvsparenvbarr}
{| id 1 {\pvsbracevbarl}
|} id 1 {\pvsbracevbarr}
\(: id 1 {\pvslistl}
:\) id 1 {\pvslistr}
\(# id 2 {\pvsrecexprl}
#\) id 2 {\pvsrecexprr}
cal_A id 1 {\cal{A}}
cal_B id 1 {\cal{B}}
cal_C id 1 {\cal{C}}
cal_D id 1 {\cal{D}}
cal_E id 1 {\cal{E}}
cal_F id 1 {\cal{F}}
cal_G id 1 {\cal{G}}
cal_H id 1 {\cal{H}}
cal_I id 1 {\cal{I}}
cal_J id 1 {\cal{J}}
cal_K id 1 {\cal{K}}
cal_L id 1 {\cal{L}}
cal_M id 1 {\cal{M}}
cal_N id 1 {\cal{N}}
cal_O id 1 {\cal{O}}
cal_P id 1 {\cal{P}}
cal_Q id 1 {\cal{Q}}
cal_R id 1 {\cal{R}}
cal_S id 1 {\cal{S}}
cal_T id 1 {\cal{T}}
cal_U id 1 {\cal{U}}
cal_V id 1 {\cal{V}}
cal_W id 1 {\cal{W}}
cal_X id 1 {\cal{X}}
cal_Y id 1 {\cal{Y}}
cal_Z id 1 {\cal{Z}}
^ 2 1 {\pvssuperscript{#1}{#2}}
expt 2 1 {\pvssuperscript{#1}{#2}}
sq 1 1 {\pvssuperscript{#1}{2}}
sqrt 1 1 {\sqrt{#1}}
root 2 1 {\sqrt[#2]{#1}}
abs 1 1 {\left|{#1}\right|}
floor 1 1 {\lfloor{#1}\rfloor}
ceiling 1 1 {\lceil{#1}\rceil}
sigma 2 1 {\sum_{#1} {#2}}
sigma 3 1 {\sum_{#1}^{#2} #3}
open 2 1 (#1,~#2)
closed 2 1 {\left[#1,~#2\right]}
open_inf 1 1 (#1,~\infty)
inf_open 1 1 (-\infty,~#1)
closed_inf 1 1 {\left[#1,~\infty\right)}
inf_closed 1 1 {\left(-\infty,~#1\right]}
phi 1 1 {\pvssubscript{\phi}{#1}}
lambda_ id 1 {\lambda}
norm 1 1 {\left||{#1}\right||}
integral 1 1 {\int#1}
integral 2 1 {\int_{#1} #2}
integral 3 1 {\int_{#1}^{#2} #3}
integral id 1 {\int}
dot 2 1 {#1\bullet#2}
ast 1 1 {{#1}^{\ast}}
plus 1 1 {{#1}^{+}}
minus 1 1 {{#1}^{-}}
ast 2 1 {#1\ast#2}
x 2 1 {#1\times#2}
P 1 1 {\mathbb{P}(#1)}
P 2 1 {\mathbb{P}(#1~|~#2)}
E 1 1 {\mathbb{E}(#1)}
E 2 1 {\mathbb{E}(#1~|~#2)}
complex id 1 \mathbb{C}
nonzero_complex id 1 {\pvssubscript{\mathbb{C}}{{\not=}0}}
nzcomplex id 1 {\pvssubscript{\mathbb{C}}{{\not=}0}}
complex_i id 1 {\imath}
Re 1 1 {\Re(#1)}
Im 1 1 {\Im(#1)}
c_add 2 1 {#1+#2}
c_neg 1 1 {-#1}
c_sub 2 1 {#1-#2}
c_mul 2 1 {#1\times#2}
c_div 2 1 {#1/#2}
conjugate 1 1 {\overline{#1}}
real id 1 \mathbb{R}
nonzero_real id 1 {\pvssubscript{\mathbb{R}}{{\not=}0}}
nzreal id 1 {\pvssubscript{\mathbb{R}}{{\not=}0}}
nonneg_real id 1 {\pvssubscript{\mathbb{R}}{{\geq}0}}
nnreal id 1 {\pvssubscript{\mathbb{R}}{{\geq}0}}
nonpos_real id 1 {\pvssubscript{\mathbb{R}}{{\leq}0}}
npreal id 1 {\pvssubscript{\mathbb{R}}{{\leq}0}}
posreal id 1 {\pvssubscript{\mathbb{R}}{{>}0}}
negreal id 1 {\pvssubscript{\mathbb{R}}{{<}0}}
rational id 1 \mathbb{Q}
rat id 1 \mathbb{Q}
nonzero_rational id 1 {\pvssubscript{\mathbb{Q}}{{\not=}0}}
nzrat id 1 {\pvssubscript{\mathbb{Q}}{{\not=}0}}
nonneg_rat id 1 {\pvssubscript{\mathbb{Q}}{{\geq}0}}
nnrat id 1 {\pvssubscript{\mathbb{Q}}{{\geq}0}}
nonpos_rat id 1 {\pvssubscript{\mathbb{Q}}{{\leq}0}}
nprat id 1 {\pvssubscript{\mathbb{Q}}{{\leq}0}}
posrat id 1 {\pvssubscript{\mathbb{Q}}{{>}0}}
negrat id 1 {\pvssubscript{\mathbb{Q}}{{<}0}}
int id 1 \mathbb{Z}
integer id 1 \mathbb{Z}
nonzero_int id 1 {\pvssubscript{\mathbb{Z}}{{\not=}0}}
nzint id 1 {\pvssubscript{\mathbb{Z}}{{\not=}0}}
nonneg_int id 1 \mathbb{N}
nonpos_int id 1 {\pvssubscript{\mathbb{Z}}{{\not=}0}}
posint id 1 {\pvssubscript{\mathbb{N}}{{>}0}}
negint id 1 {\pvssubscript{\mathbb{Z}}{{<}0}}
nat id 1 \mathbb{N}
naturalnumber id 1 \mathbb{N}
posnat id 1 {\pvssubscript{\mathbb{N}}{{>}0}}
posreals id 1 {\pvssubscript{\mathbb{R}}{{>}0}}
negreals id 1 {\pvssubscript{\mathbb{R}}{{<}0}}
nnreals id 1 {\pvssubscript{\mathbb{R}}{{\geq}0}}
npreals id 1 {\pvssubscript{\mathbb{R}}{{\leq}0}}
cross_product 2 1 {#1 \times #2}
convergence 2 2 {#1 \longrightarrow #2}
convergence? 2 2 {#1 \longrightarrow #2}
converges_upto? 2 2 {#1 \nearrow #2}
converges_downto? 2 2 {#1 \searrow #2}
pointwise_convergence? 2 2 {#1 \longrightarrow #2}
pointwise_converges_upto? 2 2 {#1 \nearrow #2}
pointwise_converges_downto? 2 2 {#1 \searrow #2}
extended_nnreal id 1 {\pvssubscript{\overline{\mathbb{R}}}{{\geq}0}}
x_inf 1 1 {\pvsid{inf}(#1)}
x_sup 1 1 {\pvsid{sup}(#1)}
x_sigma 3 1 {\sum_{#1}^{#2} #3}
x_sum 1 1 {\sum #1}
x_limit 1 1 {\pvsid{limit}(#1)}
x_add 2 1 {#1 + #2}
x_times 2 1 {#1 \times #2}
x_eq 2 1 {#1 = #2}
x_le 2 1 {#1 \leq #2}
x_lt 2 1 {#1 < #2}
ae_0? 1 3 {#1 = 0~\mbox{\it a.e.}}
ae_nonneg? 1 3 {#1 \geq 0~\mbox{\it a.e.}}
ae_pos? 1 3 {#1> 0~\mbox{\it a.e.}}
ae_le? 2 3 {#1 \leq #2~\mbox{\it a.e.}}
ae_eq? 2 3 {#1 = #2~\mbox{\it a.e.}}
ae_convergence? 2 3 {#1 \longrightarrow #2~\mbox{\it a.e.}}
ae_increasing? 1 3 {\pvsid{increasing?}(#1)~\mbox{\it a.e.}}
ae_decreasing? 1 3 {\pvsid{decreasing?}(#1)~\mbox{\it a.e.}}
generated_sigma_algebra 1 1 {{\cal S}(#1)}
generated_subset_algebra 1 1 {{\cal A}(#1)}
sigma_times 2 1 {#1 \times #2}
fm_times 2 1 {#1 \times #2}
m_times 2 1 {#1 \times #2}
□ id 1 \Box
◇ id 1 \Diamond