MML/mizar.dct at master · MizarSystem/MML · GitHub

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
¯0 #)
Z1 $1
Z2 $2
Z3 $3
Z4 $4
Z5 $5
Z6 $6
Z7 $7
Z8 $8
Z9 $9
Z10 $10
&0 &
(0 (
®0 (#
)0 )
,0 ,
Ó0 ->
.0 ...
Á0 .=
:0 :
;0 ;
=0 =
@0 @proof
[0 [
]0 ]
a0 according
ý0 aggregate
þ0 and
Å0 antonym
Ô0 as
X4 associativity
Ê0 assume
X8 asymmetry
¬0 attr
x0 axiom
Ö0 be
²0 begin
¡0 being
'0 by
¤0 canceled
ç0 case
â0 cases
«0 cluster
Y1 coherence
X6 commutativity
Y2 compatibility
X7 connectedness
Î0 consider
Y3 consistency
D7 constructors
%0 contradiction
‡0 correctness
Q1 def
ú0 deffunc
Ÿ0 define
+0 definition
D3 definitions
ù0 defpred
¦0 does
>0 end
°0 environ
e0 equals
œ0 ex
î0 exactly
Y4 existence
0 for
"0 from
ñ0 func
Ì0 given
¹0 hence
¼0 hereby
õ0 holds
X9 idempotence
#0 identify
Œ0 if
ð0 iff
ó0 implies
X10 involutiveness
X3 irreflexivity
0 is
ê0 it
È0 let
÷0 means
ï0 mode
©0 non
ª0 not
-0 notation
D2 notations
<0 now
ø0 of
§0 or
“0 otherwise
¢0 over
ã0 per
ò0 pred
è0 prefix
X11 projectivity
/0 proof
ö0 provided
Õ0 qua
æ0 reconsider
å0 redefine
c0 reduce
Y6 reducibility
X2 reflexivity
*0 registration
D6 registrations
D8 requirements
×0 reserve
Q2 sch
ä0 scheme
D5 schemes
s0 section
á0 selector
à0 set
X12 sethood
ô0 st
í0 struct
û0 such
Í0 suppose
X1 symmetry
Ä0 synonym
É0 take
ü0 that
é0 the
À0 then
ì0 theorem
D4 theorems
$0 thesis
Ë0 thus
t0 to
X5 transitivity
Y5 uniqueness
D1 vocabularies
r0 wrt
¨0 where
w0 when
h0 with
{0 {
}0 }