-
Notifications
You must be signed in to change notification settings - Fork 0
/
Name.tex
100 lines (97 loc) · 8.55 KB
/
Name.tex
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
% The following substitutions are from the file:
% /home/augusto/Desktop/PVS/pvs-tex.sub
\def\munderscoretimestwofn#1#2{{#1 \times #2}}% How to print function m_times with arity (2)
\def\fmunderscoretimestwofn#1#2{{#1 \times #2}}% How to print function fm_times with arity (2)
\def\sigmaunderscoretimestwofn#1#2{{#1 \times #2}}% How to print function sigma_times with arity (2)
\def\generatedunderscoresubsetunderscorealgebraonefn#1{{{\cal A}(#1)}}% How to print function generated_subset_algebra with arity (1)
\def\generatedunderscoresigmaunderscorealgebraonefn#1{{{\cal S}(#1)}}% How to print function generated_sigma_algebra with arity (1)
\def\aeunderscoredecreasingotheronefn#1{{\pvsid{decreasing?}(#1)~\mbox{\it a.e.}}}% How to print function ae_decreasing? with arity (1)
\def\aeunderscoreincreasingotheronefn#1{{\pvsid{increasing?}(#1)~\mbox{\it a.e.}}}% How to print function ae_increasing? with arity (1)
\def\aeunderscoreconvergenceothertwofn#1#2{{#1 \longrightarrow #2~\mbox{\it a.e.}}}% How to print function ae_convergence? with arity (2)
\def\aeunderscoreeqothertwofn#1#2{{#1 = #2~\mbox{\it a.e.}}}% How to print function ae_eq? with arity (2)
\def\aeunderscoreleothertwofn#1#2{{#1 \leq #2~\mbox{\it a.e.}}}% How to print function ae_le? with arity (2)
\def\aeunderscoreposotheronefn#1{{#1> 0~\mbox{\it a.e.}}}% How to print function ae_pos? with arity (1)
\def\aeunderscorenonnegotheronefn#1{{#1 \geq 0~\mbox{\it a.e.}}}% How to print function ae_nonneg? with arity (1)
\def\aeunderscorezerootheronefn#1{{#1 = 0~\mbox{\it a.e.}}}% How to print function ae_0? with arity (1)
\def\xunderscorelttwofn#1#2{{#1 < #2}}% How to print function x_lt with arity (2)
\def\xunderscoreletwofn#1#2{{#1 \leq #2}}% How to print function x_le with arity (2)
\def\xunderscoreeqtwofn#1#2{{#1 = #2}}% How to print function x_eq with arity (2)
\def\xunderscoretimestwofn#1#2{{#1 \times #2}}% How to print function x_times with arity (2)
\def\xunderscoreaddtwofn#1#2{{#1 + #2}}% How to print function x_add with arity (2)
\def\xunderscorelimitonefn#1{{\pvsid{limit}(#1)}}% How to print function x_limit with arity (1)
\def\xunderscoresumonefn#1{{\sum #1}}% How to print function x_sum with arity (1)
\def\xunderscoresigmathreefn#1#2#3{{\sum_{#1}^{#2} #3}}% How to print function x_sigma with arity (3)
\def\xunderscoresuponefn#1{{\pvsid{sup}(#1)}}% How to print function x_sup with arity (1)
\def\xunderscoreinfonefn#1{{\pvsid{inf}(#1)}}% How to print function x_inf with arity (1)
\def\pointwiseunderscoreconvergesunderscoredowntoothertwofn#1#2{{#1 \searrow #2}}% How to print function pointwise_converges_downto? with arity (2)
\def\pointwiseunderscoreconvergesunderscoreuptoothertwofn#1#2{{#1 \nearrow #2}}% How to print function pointwise_converges_upto? with arity (2)
\def\pointwiseunderscoreconvergenceothertwofn#1#2{{#1 \longrightarrow #2}}% How to print function pointwise_convergence? with arity (2)
\def\convergesunderscoredowntoothertwofn#1#2{{#1 \searrow #2}}% How to print function converges_downto? with arity (2)
\def\convergesunderscoreuptoothertwofn#1#2{{#1 \nearrow #2}}% How to print function converges_upto? with arity (2)
\def\convergenceothertwofn#1#2{{#1 \longrightarrow #2}}% How to print function convergence? with arity (2)
\def\convergencetwofn#1#2{{#1 \longrightarrow #2}}% How to print function convergence with arity (2)
\def\crossunderscoreproducttwofn#1#2{{#1 \times #2}}% How to print function cross_product with arity (2)
\def\conjugateonefn#1{{\overline{#1}}}% How to print function conjugate with arity (1)
\def\cunderscoredivtwofn#1#2{{#1/#2}}% How to print function c_div with arity (2)
\def\cunderscoremultwofn#1#2{{#1\times#2}}% How to print function c_mul with arity (2)
\def\cunderscoresubtwofn#1#2{{#1-#2}}% How to print function c_sub with arity (2)
\def\cunderscorenegonefn#1{{-#1}}% How to print function c_neg with arity (1)
\def\cunderscoreaddtwofn#1#2{{#1+#2}}% How to print function c_add with arity (2)
\def\Imonefn#1{{\Im(#1)}}% How to print function Im with arity (1)
\def\Reonefn#1{{\Re(#1)}}% How to print function Re with arity (1)
\def\Etwofn#1#2{{\mathbb{E}(#1~|~#2)}}% How to print function E with arity (2)
\def\Eonefn#1{{\mathbb{E}(#1)}}% How to print function E with arity (1)
\def\Ptwofn#1#2{{\mathbb{P}(#1~|~#2)}}% How to print function P with arity (2)
\def\Ponefn#1{{\mathbb{P}(#1)}}% How to print function P with arity (1)
\def\xtwofn#1#2{{#1\times#2}}% How to print function x with arity (2)
\def\asttwofn#1#2{{#1\ast#2}}% How to print function ast with arity (2)
\def\minusonefn#1{{{#1}^{-}}}% How to print function minus with arity (1)
\def\plusonefn#1{{{#1}^{+}}}% How to print function plus with arity (1)
\def\astonefn#1{{{#1}^{\ast}}}% How to print function ast with arity (1)
\def\dottwofn#1#2{{#1\bullet#2}}% How to print function dot with arity (2)
\def\integralthreefn#1#2#3{{\int_{#1}^{#2} #3}}% How to print function integral with arity (3)
\def\integraltwofn#1#2{{\int_{#1} #2}}% How to print function integral with arity (2)
\def\integralonefn#1{{\int#1}}% How to print function integral with arity (1)
\def\normonefn#1{{\left||{#1}\right||}}% How to print function norm with arity (1)
\def\phionefn#1{{\pvssubscript{\phi}{#1}}}% How to print function phi with arity (1)
\def\infunderscoreclosedonefn#1{{\left(-\infty,~#1\right]}}% How to print function inf_closed with arity (1)
\def\closedunderscoreinfonefn#1{{\left[#1,~\infty\right)}}% How to print function closed_inf with arity (1)
\def\infunderscoreopenonefn#1{(-\infty,~#1)}% How to print function inf_open with arity (1)
\def\openunderscoreinfonefn#1{(#1,~\infty)}% How to print function open_inf with arity (1)
\def\closedtwofn#1#2{{\left[#1,~#2\right]}}% How to print function closed with arity (2)
\def\opentwofn#1#2{(#1,~#2)}% How to print function open with arity (2)
\def\sigmathreefn#1#2#3{{\sum_{#1}^{#2} #3}}% How to print function sigma with arity (3)
\def\sigmatwofn#1#2{{\sum_{#1} {#2}}}% How to print function sigma with arity (2)
\def\ceilingonefn#1{{\lceil{#1}\rceil}}% How to print function ceiling with arity (1)
\def\flooronefn#1{{\lfloor{#1}\rfloor}}% How to print function floor with arity (1)
\def\absonefn#1{{\left|{#1}\right|}}% How to print function abs with arity (1)
\def\roottwofn#1#2{{\sqrt[#2]{#1}}}% How to print function root with arity (2)
\def\sqrtonefn#1{{\sqrt{#1}}}% How to print function sqrt with arity (1)
\def\sqonefn#1{{\pvssuperscript{#1}{2}}}% How to print function sq with arity (1)
\def\expttwofn#1#2{{\pvssuperscript{#1}{#2}}}% How to print function expt with arity (2)
\def\opcarettwofn#1#2{{\pvssuperscript{#1}{#2}}}% How to print function ^ with arity (2)
\def\indexedunderscoresetsotherIIntersectiononefn#1{{\bigcap #1}}% How to print function indexed_sets.IIntersection with arity (1)
\def\indexedunderscoresetsotherIUniononefn#1{{\bigcup #1}}% How to print function indexed_sets.IUnion with arity (1)
\def\setsotherIntersectiononefn#1{{\bigcap #1}}% How to print function sets.Intersection with arity (1)
\def\setsotherUniononefn#1{{\bigcup #1}}% How to print function sets.Union with arity (1)
\def\setsotherremovetwofn#1#2{{(#2 \setminus \{#1\})}}% How to print function sets.remove with arity (2)
\def\setsotheraddtwofn#1#2{{(#2 \cup \{#1\})}}% How to print function sets.add with arity (2)
\def\setsotherdifferencetwofn#1#2{{(#1 \setminus #2)}}% How to print function sets.difference with arity (2)
\def\setsothercomplementonefn#1{{\overline{#1}}}% How to print function sets.complement with arity (1)
\def\setsotherintersectiontwofn#1#2{{(#1 \cap #2)}}% How to print function sets.intersection with arity (2)
\def\setsotheruniontwofn#1#2{{(#1 \cup #2)}}% How to print function sets.union with arity (2)
\def\setsotherstrictunderscoresubsetothertwofn#1#2{{(#1 \subset #2)}}% How to print function sets.strict_subset? with arity (2)
\def\setsothersubsetothertwofn#1#2{{(#1 \subseteq #2)}}% How to print function sets.subset? with arity (2)
\def\setsothermembertwofn#1#2{{(#1 \in #2)}}% How to print function sets.member with arity (2)
\def\opohtwofn#1#2{{#1\circ#2}}% How to print function O with arity (2)
\def\opdividetwofn#1#2{{\frac{#1}{#2}}}% How to print function / with arity (2)
\def\optimestwofn#1#2{{#1\times#2}}% How to print function * with arity (2)
\def\opdifferenceonefn#1{{-#1}}% How to print function - with arity (1)
\def\opdifferencetwofn#1#2{{#1-#2}}% How to print function - with arity (2)
\def\opplustwofn#1#2{{#1+#2}}% How to print function + with arity (2)
\begin{alltt}
\pvsid{Name}: \pvskey{THEORY}
\pvskey{BEGIN}
\pvsid{Name}: \pvskey{TYPE}\vspace*{\pvsdeclspacing}
\pvsid{Configuration}: \pvskey{TYPE} = \pvsid{set}\({\pvsbracketl}\)\pvsid{Name}\({\pvsbracketr}\)\vspace*{\pvsdeclspacing}
\pvskey{END} \pvsid{Name}\end{alltt}