ref-2-id-99
|
exist {MissingArg} indeed {MissingArg}
|
ref-2-id-102
|
{MissingArg} imply {MissingArg}
|
ref-0-id-0
|
kvanti
|
ref-0-id-1
|
lemma uniqueMember
|
ref-0-id-2
|
lemma uniqueMember(Type)
|
ref-0-id-3
|
lemma sameSeries
|
ref-0-id-4
|
lemma a4
|
ref-0-id-5
|
lemma sameMember
|
ref-0-id-6
|
1rule Qclosed(Addition)
|
ref-0-id-7
|
1rule Qclosed(Multiplication)
|
ref-0-id-8
|
1rule fromCartProd(1)
|
ref-0-id-9
|
1rule fromCartProd(2)
|
ref-0-id-10
|
constantRationalSeries( {MissingArg} )
|
ref-0-id-11
|
cartProd( {MissingArg} , {MissingArg} )
|
ref-0-id-12
|
P( {MissingArg} )
|
ref-0-id-13
|
binaryUnion( {MissingArg} , {MissingArg} )
|
ref-0-id-14
|
setOfRationalSeries
|
ref-0-id-15
|
isSubset( {MissingArg} , {MissingArg} )
|
ref-0-id-16
|
(p {MissingArg} , {MissingArg} )
|
ref-0-id-17
|
(s {MissingArg} )
|
ref-0-id-18
|
cdots
|
ref-0-id-19
|
object-var
|
ref-0-id-20
|
ex-var
|
ref-0-id-21
|
ph-var
|
ref-0-id-22
|
vaerdi
|
ref-0-id-23
|
variabel
|
ref-0-id-24
|
op {MissingArg} end op
|
ref-0-id-25
|
op2 {MissingArg} comma {MissingArg} end op2
|
ref-0-id-26
|
define-equal {MissingArg} comma {MissingArg} end equal
|
ref-0-id-27
|
contains-empty {MissingArg} end empty
|
ref-0-id-28
|
Nat( {MissingArg} )
|
ref-0-id-29
|
1deduction {MissingArg} conclude {MissingArg} end 1deduction
|
ref-0-id-30
|
1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
|
ref-0-id-31
|
1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
|
ref-0-id-32
|
1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
|
ref-0-id-33
|
1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
|
ref-0-id-34
|
1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-35
|
1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-36
|
1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-37
|
1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-38
|
1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-39
|
1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-40
|
1deduction seven {MissingArg} end 1deduction
|
ref-0-id-41
|
1deduction eight {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-42
|
1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
|
ref-0-id-43
|
ex1
|
ref-0-id-44
|
ex2
|
ref-0-id-45
|
ex3
|
ref-0-id-46
|
ex10
|
ref-0-id-47
|
ex20
|
ref-0-id-48
|
existential var {MissingArg} end var
|
ref-0-id-49
|
{MissingArg} is existential var
|
ref-0-id-50
|
exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-51
|
exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-52
|
exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-53
|
exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-54
|
ph1
|
ref-0-id-55
|
ph2
|
ref-0-id-56
|
ph3
|
ref-0-id-57
|
placeholder-var {MissingArg} end var
|
ref-0-id-58
|
{MissingArg} is placeholder-var
|
ref-0-id-59
|
ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-60
|
ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-61
|
ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-62
|
ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-63
|
meta-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-64
|
meta-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-65
|
meta-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-66
|
var big set
|
ref-0-id-67
|
object big set
|
ref-0-id-68
|
meta big set
|
ref-0-id-69
|
zermelo empty set
|
ref-0-id-70
|
system Q
|
ref-0-id-71
|
1rule mp
|
ref-0-id-72
|
1rule gen
|
ref-0-id-73
|
1rule repetition
|
ref-0-id-74
|
1rule ad absurdum
|
ref-0-id-75
|
1rule deduction
|
ref-0-id-76
|
1rule exist intro
|
ref-0-id-77
|
axiom extensionality
|
ref-0-id-78
|
axiom empty set
|
ref-0-id-79
|
axiom pair definition
|
ref-0-id-80
|
axiom union definition
|
ref-0-id-81
|
axiom power definition
|
ref-0-id-82
|
axiom separation definition
|
ref-0-id-83
|
prop lemma add double neg
|
ref-0-id-84
|
prop lemma remove double neg
|
ref-0-id-85
|
prop lemma and commutativity
|
ref-0-id-86
|
prop lemma auto imply
|
ref-0-id-87
|
prop lemma contrapositive
|
ref-0-id-88
|
prop lemma first conjunct
|
ref-0-id-89
|
prop lemma second conjunct
|
ref-0-id-90
|
prop lemma from contradiction
|
ref-0-id-91
|
prop lemma from disjuncts
|
ref-0-id-92
|
prop lemma iff commutativity
|
ref-0-id-93
|
prop lemma iff first
|
ref-0-id-94
|
prop lemma iff second
|
ref-0-id-95
|
prop lemma imply transitivity
|
ref-0-id-96
|
prop lemma join conjuncts
|
ref-0-id-97
|
prop lemma mp2
|
ref-0-id-98
|
prop lemma mp3
|
ref-0-id-99
|
prop lemma mp4
|
ref-0-id-100
|
prop lemma mp5
|
ref-0-id-101
|
prop lemma mt
|
ref-0-id-102
|
prop lemma negative mt
|
ref-0-id-103
|
prop lemma technicality
|
ref-0-id-104
|
prop lemma weakening
|
ref-0-id-105
|
prop lemma weaken or first
|
ref-0-id-106
|
prop lemma weaken or second
|
ref-0-id-107
|
lemma formula2pair
|
ref-0-id-108
|
lemma pair2formula
|
ref-0-id-109
|
lemma formula2union
|
ref-0-id-110
|
lemma union2formula
|
ref-0-id-111
|
lemma formula2separation
|
ref-0-id-112
|
lemma separation2formula
|
ref-0-id-113
|
lemma formula2power
|
ref-0-id-114
|
lemma subset in power set
|
ref-0-id-115
|
lemma power set is subset0
|
ref-0-id-116
|
lemma power set is subset
|
ref-0-id-117
|
lemma power set is subset0-switch
|
ref-0-id-118
|
lemma power set is subset-switch
|
ref-0-id-119
|
lemma set equality suff condition
|
ref-0-id-120
|
lemma set equality suff condition(t)0
|
ref-0-id-121
|
lemma set equality suff condition(t)
|
ref-0-id-122
|
lemma set equality skip quantifier
|
ref-0-id-123
|
lemma set equality nec condition
|
ref-0-id-124
|
lemma reflexivity0
|
ref-0-id-125
|
lemma reflexivity
|
ref-0-id-126
|
lemma symmetry0
|
ref-0-id-127
|
lemma symmetry
|
ref-0-id-128
|
lemma transitivity0
|
ref-0-id-129
|
lemma transitivity
|
ref-0-id-130
|
lemma er is reflexive
|
ref-0-id-131
|
lemma er is symmetric
|
ref-0-id-132
|
lemma er is transitive
|
ref-0-id-133
|
lemma empty set is subset
|
ref-0-id-134
|
lemma member not empty0
|
ref-0-id-135
|
lemma member not empty
|
ref-0-id-136
|
lemma unique empty set0
|
ref-0-id-137
|
lemma unique empty set
|
ref-0-id-138
|
lemma ==Reflexivity
|
ref-0-id-139
|
lemma ==Symmetry
|
ref-0-id-140
|
lemma ==Transitivity0
|
ref-0-id-141
|
lemma ==Transitivity
|
ref-0-id-142
|
lemma transfer ~is0
|
ref-0-id-143
|
lemma transfer ~is
|
ref-0-id-144
|
lemma pair subset0
|
ref-0-id-145
|
lemma pair subset1
|
ref-0-id-146
|
lemma pair subset
|
ref-0-id-147
|
lemma same pair
|
ref-0-id-148
|
lemma same singleton
|
ref-0-id-149
|
lemma union subset
|
ref-0-id-150
|
lemma same union
|
ref-0-id-151
|
lemma separation subset
|
ref-0-id-152
|
lemma same separation
|
ref-0-id-153
|
lemma same binary union
|
ref-0-id-154
|
lemma intersection subset
|
ref-0-id-155
|
lemma same intersection
|
ref-0-id-156
|
lemma auto member
|
ref-0-id-157
|
lemma eq-system not empty0
|
ref-0-id-158
|
lemma eq-system not empty
|
ref-0-id-159
|
lemma eq subset0
|
ref-0-id-160
|
lemma eq subset
|
ref-0-id-161
|
lemma equivalence nec condition0
|
ref-0-id-162
|
lemma equivalence nec condition
|
ref-0-id-163
|
lemma none-equivalence nec condition0
|
ref-0-id-164
|
lemma none-equivalence nec condition1
|
ref-0-id-165
|
lemma none-equivalence nec condition
|
ref-0-id-166
|
lemma equivalence class is subset
|
ref-0-id-167
|
lemma equivalence classes are disjoint
|
ref-0-id-168
|
lemma all disjoint
|
ref-0-id-169
|
lemma all disjoint-imply
|
ref-0-id-170
|
lemma bs subset union(bs/r)
|
ref-0-id-171
|
lemma union(bs/r) subset bs
|
ref-0-id-172
|
lemma union(bs/r) is bs
|
ref-0-id-173
|
theorem eq-system is partition
|
ref-0-id-174
|
var x1
|
ref-0-id-175
|
var x2
|
ref-0-id-176
|
var y1
|
ref-0-id-177
|
var y2
|
ref-0-id-178
|
var v1
|
ref-0-id-179
|
var v2
|
ref-0-id-180
|
var v3
|
ref-0-id-181
|
var v4
|
ref-0-id-182
|
var v2n
|
ref-0-id-183
|
var m1
|
ref-0-id-184
|
var m2
|
ref-0-id-185
|
var n1
|
ref-0-id-186
|
var n2
|
ref-0-id-187
|
var n3
|
ref-0-id-188
|
var ep
|
ref-0-id-189
|
var ep1
|
ref-0-id-190
|
var ep2
|
ref-0-id-191
|
var fep
|
ref-0-id-192
|
var fx
|
ref-0-id-193
|
var fy
|
ref-0-id-194
|
var fz
|
ref-0-id-195
|
var fu
|
ref-0-id-196
|
var fv
|
ref-0-id-197
|
var fw
|
ref-0-id-198
|
var rx
|
ref-0-id-199
|
var ry
|
ref-0-id-200
|
var rz
|
ref-0-id-201
|
var ru
|
ref-0-id-202
|
var sx
|
ref-0-id-203
|
var sx1
|
ref-0-id-204
|
var sy
|
ref-0-id-205
|
var sy1
|
ref-0-id-206
|
var sz
|
ref-0-id-207
|
var sz1
|
ref-0-id-208
|
var su
|
ref-0-id-209
|
var su1
|
ref-0-id-210
|
var fxs
|
ref-0-id-211
|
var fys
|
ref-0-id-212
|
var crs1
|
ref-0-id-213
|
var f1
|
ref-0-id-214
|
var f2
|
ref-0-id-215
|
var f3
|
ref-0-id-216
|
var f4
|
ref-0-id-217
|
var op1
|
ref-0-id-218
|
var op2
|
ref-0-id-219
|
var r1
|
ref-0-id-220
|
var s1
|
ref-0-id-221
|
var s2
|
ref-0-id-222
|
meta x1
|
ref-0-id-223
|
meta x2
|
ref-0-id-224
|
meta y1
|
ref-0-id-225
|
meta y2
|
ref-0-id-226
|
meta v1
|
ref-0-id-227
|
meta v2
|
ref-0-id-228
|
meta v3
|
ref-0-id-229
|
meta v4
|
ref-0-id-230
|
meta v2n
|
ref-0-id-231
|
meta m1
|
ref-0-id-232
|
meta m2
|
ref-0-id-233
|
meta n1
|
ref-0-id-234
|
meta n2
|
ref-0-id-235
|
meta n3
|
ref-0-id-236
|
meta ep
|
ref-0-id-237
|
meta ep1
|
ref-0-id-238
|
meta ep2
|
ref-0-id-239
|
meta fx
|
ref-0-id-240
|
meta fy
|
ref-0-id-241
|
meta fz
|
ref-0-id-242
|
meta fu
|
ref-0-id-243
|
meta fv
|
ref-0-id-244
|
meta fw
|
ref-0-id-245
|
meta fep
|
ref-0-id-246
|
meta rx
|
ref-0-id-247
|
meta ry
|
ref-0-id-248
|
meta rz
|
ref-0-id-249
|
meta ru
|
ref-0-id-250
|
meta sx
|
ref-0-id-251
|
meta sx1
|
ref-0-id-252
|
meta sy
|
ref-0-id-253
|
meta sy1
|
ref-0-id-254
|
meta sz
|
ref-0-id-255
|
meta sz1
|
ref-0-id-256
|
meta su
|
ref-0-id-257
|
meta su1
|
ref-0-id-258
|
meta fxs
|
ref-0-id-259
|
meta fys
|
ref-0-id-260
|
meta f1
|
ref-0-id-261
|
meta f2
|
ref-0-id-262
|
meta f3
|
ref-0-id-263
|
meta f4
|
ref-0-id-264
|
meta op1
|
ref-0-id-265
|
meta op2
|
ref-0-id-266
|
meta r1
|
ref-0-id-267
|
meta s1
|
ref-0-id-268
|
meta s2
|
ref-0-id-269
|
object ep
|
ref-0-id-270
|
object crs1
|
ref-0-id-271
|
object f1
|
ref-0-id-272
|
object f2
|
ref-0-id-273
|
object f3
|
ref-0-id-274
|
object f4
|
ref-0-id-275
|
object n1
|
ref-0-id-276
|
object n2
|
ref-0-id-277
|
object op1
|
ref-0-id-278
|
object op2
|
ref-0-id-279
|
object r1
|
ref-0-id-280
|
object s1
|
ref-0-id-281
|
object s2
|
ref-0-id-282
|
ph4
|
ref-0-id-283
|
ph5
|
ref-0-id-284
|
ph6
|
ref-0-id-285
|
NAT
|
ref-0-id-286
|
RATIONAL_SERIES
|
ref-0-id-287
|
SERIES
|
ref-0-id-288
|
setOfReals
|
ref-0-id-289
|
setOfFxs
|
ref-0-id-290
|
N
|
ref-0-id-291
|
Q
|
ref-0-id-292
|
X
|
ref-0-id-293
|
xs
|
ref-0-id-294
|
xsF
|
ref-0-id-295
|
ysF
|
ref-0-id-296
|
us
|
ref-0-id-297
|
usF
|
ref-0-id-298
|
0
|
ref-0-id-299
|
1
|
ref-0-id-300
|
(-1)
|
ref-0-id-301
|
2
|
ref-0-id-302
|
3
|
ref-0-id-303
|
1/2
|
ref-0-id-304
|
1/3
|
ref-0-id-305
|
2/3
|
ref-0-id-306
|
0f
|
ref-0-id-307
|
1f
|
ref-0-id-308
|
00
|
ref-0-id-309
|
01
|
ref-0-id-310
|
(--01)
|
ref-0-id-311
|
02
|
ref-0-id-312
|
01//02
|
ref-0-id-313
|
lemma plusAssociativity(R)
|
ref-0-id-314
|
lemma plusAssociativity(R)XX
|
ref-0-id-315
|
lemma plus0(R)
|
ref-0-id-316
|
lemma negative(R)
|
ref-0-id-317
|
lemma times1(R)
|
ref-0-id-318
|
lemma lessAddition(R)
|
ref-0-id-319
|
lemma plusCommutativity(R)
|
ref-0-id-320
|
lemma leqAntisymmetry(R)
|
ref-0-id-321
|
lemma leqTransitivity(R)
|
ref-0-id-322
|
lemma leqAddition(R)
|
ref-0-id-323
|
lemma distribution(R)
|
ref-0-id-324
|
axiom a4
|
ref-0-id-325
|
axiom induction
|
ref-0-id-326
|
axiom equality
|
ref-0-id-327
|
axiom eqLeq
|
ref-0-id-328
|
axiom eqAddition
|
ref-0-id-329
|
axiom eqMultiplication
|
ref-0-id-330
|
axiom QisClosed(reciprocal)
|
ref-0-id-331
|
lemma QisClosed(reciprocal)
|
ref-0-id-332
|
axiom QisClosed(negative)
|
ref-0-id-333
|
lemma QisClosed(negative)
|
ref-0-id-334
|
axiom leqReflexivity
|
ref-0-id-335
|
axiom leqAntisymmetry
|
ref-0-id-336
|
axiom leqTransitivity
|
ref-0-id-337
|
axiom leqTotality
|
ref-0-id-338
|
axiom leqAddition
|
ref-0-id-339
|
axiom leqMultiplication
|
ref-0-id-340
|
axiom plusAssociativity
|
ref-0-id-341
|
axiom plusCommutativity
|
ref-0-id-342
|
axiom negative
|
ref-0-id-343
|
axiom plus0
|
ref-0-id-344
|
axiom timesAssociativity
|
ref-0-id-345
|
axiom timesCommutativity
|
ref-0-id-346
|
axiom reciprocal
|
ref-0-id-347
|
axiom times1
|
ref-0-id-348
|
axiom distribution
|
ref-0-id-349
|
axiom 0not1
|
ref-0-id-350
|
lemma eqLeq(R)
|
ref-0-id-351
|
lemma timesAssociativity(R)
|
ref-0-id-352
|
lemma timesCommutativity(R)
|
ref-0-id-353
|
1rule adhoc sameR
|
ref-0-id-354
|
lemma separation2formula(1)
|
ref-0-id-355
|
lemma separation2formula(2)
|
ref-0-id-356
|
axiom cauchy
|
ref-0-id-357
|
axiom plusF
|
ref-0-id-358
|
axiom reciprocalF
|
ref-0-id-359
|
1rule from==
|
ref-0-id-360
|
1rule to==
|
ref-0-id-361
|
1rule fromInR
|
ref-0-id-362
|
lemma plusR(Sym)
|
ref-0-id-363
|
axiom reciprocalR
|
ref-0-id-364
|
1rule lessMinus1(N)
|
ref-0-id-365
|
axiom nonnegative(N)
|
ref-0-id-366
|
axiom US0
|
ref-0-id-367
|
1rule nextXS(upperBound)
|
ref-0-id-368
|
1rule nextXS(noUpperBound)
|
ref-0-id-369
|
1rule nextUS(upperBound)
|
ref-0-id-370
|
1rule nextUS(noUpperBound)
|
ref-0-id-371
|
1rule expZero
|
ref-0-id-372
|
1rule expPositive
|
ref-0-id-373
|
1rule expZero(R)
|
ref-0-id-374
|
1rule expPositive(R)
|
ref-0-id-375
|
1rule base(1/2)Sum zero
|
ref-0-id-376
|
1rule base(1/2)Sum positive
|
ref-0-id-377
|
1rule UStelescope zero
|
ref-0-id-378
|
1rule UStelescope positive
|
ref-0-id-379
|
1rule adhoc eqAddition(R)
|
ref-0-id-380
|
1rule fromLimit
|
ref-0-id-381
|
1rule toUpperBound
|
ref-0-id-382
|
1rule fromUpperBound
|
ref-0-id-383
|
axiom USisUpperBound
|
ref-0-id-384
|
axiom 0not1(R)
|
ref-0-id-385
|
1rule expUnbounded
|
ref-0-id-386
|
1rule fromLeq(Advanced)(N)
|
ref-0-id-387
|
1rule fromLeastUpperBound
|
ref-0-id-388
|
1rule toLeastUpperBound
|
ref-0-id-389
|
axiom XSisNotUpperBound
|
ref-0-id-390
|
axiom ysFGreater
|
ref-0-id-391
|
axiom ysFLess
|
ref-0-id-392
|
1rule smallInverse
|
ref-0-id-393
|
axiom natType
|
ref-0-id-394
|
axiom rationalType
|
ref-0-id-395
|
axiom seriesType
|
ref-0-id-396
|
axiom max
|
ref-0-id-397
|
axiom numerical
|
ref-0-id-398
|
axiom numericalF
|
ref-0-id-399
|
axiom memberOfSeries
|
ref-0-id-400
|
prop lemma doubly conditioned join conjuncts
|
ref-0-id-401
|
prop lemma imply negation
|
ref-0-id-402
|
prop lemma tertium non datur
|
ref-0-id-403
|
prop lemma from negated imply
|
ref-0-id-404
|
prop lemma to negated imply
|
ref-0-id-405
|
prop lemma from negated double imply
|
ref-0-id-406
|
prop lemma from negated and
|
ref-0-id-407
|
prop lemma from negated or
|
ref-0-id-408
|
prop lemma to negated or
|
ref-0-id-409
|
prop lemma from negations
|
ref-0-id-410
|
prop lemma from three disjuncts
|
ref-0-id-411
|
prop lemma from two times two disjuncts
|
ref-0-id-412
|
prop lemma negate first disjunct
|
ref-0-id-413
|
prop lemma negate second disjunct
|
ref-0-id-414
|
prop lemma expand disjuncts
|
ref-0-id-415
|
lemma set equality nec condition(1)
|
ref-0-id-416
|
lemma set equality nec condition(2)
|
ref-0-id-417
|
lemma lessLeq(R)
|
ref-0-id-418
|
lemma memberOfSeries
|
ref-0-id-419
|
lemma memberOfSeries(Type)
|
ref-0-id-420
|
{MissingArg} ^ {MissingArg}
|
ref-0-id-421
|
R( {MissingArg} )
|
ref-0-id-422
|
--R( {MissingArg} )
|
ref-0-id-423
|
1/ {MissingArg}
|
ref-0-id-424
|
eq-system of {MissingArg} modulo {MissingArg}
|
ref-0-id-425
|
intersection {MissingArg} comma {MissingArg} end intersection
|
ref-0-id-426
|
[ {MissingArg} ; {MissingArg} ]
|
ref-0-id-427
|
union {MissingArg} end union
|
ref-0-id-428
|
binary-union {MissingArg} comma {MissingArg} end union
|
ref-0-id-429
|
power {MissingArg} end power
|
ref-0-id-430
|
zermelo singleton {MissingArg} end singleton
|
ref-0-id-431
|
stateExpand( {MissingArg} , {MissingArg} , {MissingArg} )
|
ref-0-id-432
|
extractSeries( {MissingArg} )
|
ref-0-id-433
|
setOfSeries( {MissingArg} )
|
ref-0-id-434
|
--Macro( {MissingArg} )
|
ref-0-id-435
|
expandList( {MissingArg} , {MissingArg} , {MissingArg} )
|
ref-0-id-436
|
**Macro( {MissingArg} )
|
ref-0-id-437
|
++Macro( {MissingArg} )
|
ref-0-id-438
|
<
|
ref-0-id-439
|
||Macro( {MissingArg} )
|
ref-0-id-440
|
01//Macro( {MissingArg} )
|
ref-0-id-441
|
upperBound( {MissingArg} , {MissingArg} )
|
ref-0-id-442
|
leastUpperBound( {MissingArg} , {MissingArg} )
|
ref-0-id-443
|
base(1/2)Sum( {MissingArg} , {MissingArg} )
|
ref-0-id-444
|
UStelescope( {MissingArg} , {MissingArg} )
|
ref-0-id-445
|
( {MissingArg} )
|
ref-0-id-446
|
|f {MissingArg} |
|
ref-0-id-447
|
|r {MissingArg} |
|
ref-0-id-448
|
limit( {MissingArg} , {MissingArg} )
|
ref-0-id-449
|
U( {MissingArg} )
|
ref-0-id-450
|
isOrderedPair( {MissingArg} , {MissingArg} , {MissingArg} )
|
ref-0-id-451
|
isRelation( {MissingArg} , {MissingArg} , {MissingArg} )
|
ref-0-id-452
|
isFunction( {MissingArg} , {MissingArg} , {MissingArg} )
|
ref-0-id-453
|
isSeries( {MissingArg} , {MissingArg} )
|
ref-0-id-454
|
isNatural( {MissingArg} )
|
ref-0-id-455
|
(o {MissingArg} , {MissingArg} )
|
ref-0-id-456
|
typeNat( {MissingArg} )
|
ref-0-id-457
|
typeNat0( {MissingArg} )
|
ref-0-id-458
|
typeRational( {MissingArg} )
|
ref-0-id-459
|
typeRational0( {MissingArg} )
|
ref-0-id-460
|
typeSeries( {MissingArg} , {MissingArg} )
|
ref-0-id-461
|
typeSeries0( {MissingArg} , {MissingArg} )
|
ref-0-id-462
|
zermelo pair {MissingArg} comma {MissingArg} end pair
|
ref-0-id-463
|
zermelo ordered pair {MissingArg} comma {MissingArg} end pair
|
ref-0-id-464
|
- {MissingArg}
|
ref-0-id-465
|
-f {MissingArg}
|
ref-0-id-466
|
-- {MissingArg}
|
ref-0-id-467
|
1f/ {MissingArg}
|
ref-0-id-468
|
01// {MissingArg}
|
ref-0-id-469
|
{MissingArg} is related to {MissingArg} under {MissingArg}
|
ref-0-id-470
|
{MissingArg} is reflexive relation in {MissingArg}
|
ref-0-id-471
|
{MissingArg} is symmetric relation in {MissingArg}
|
ref-0-id-472
|
{MissingArg} is transitive relation in {MissingArg}
|
ref-0-id-473
|
{MissingArg} is equivalence relation in {MissingArg}
|
ref-0-id-474
|
equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
|
ref-0-id-475
|
{MissingArg} is partition of {MissingArg}
|
ref-0-id-476
|
{MissingArg} * {MissingArg}
|
ref-0-id-477
|
{MissingArg} *f {MissingArg}
|
ref-0-id-478
|
{MissingArg} ** {MissingArg}
|
ref-0-id-479
|
{MissingArg} + {MissingArg}
|
ref-0-id-480
|
{MissingArg} - {MissingArg}
|
ref-0-id-481
|
{MissingArg} +f {MissingArg}
|
ref-0-id-482
|
{MissingArg} -f {MissingArg}
|
ref-0-id-483
|
{MissingArg} ++ {MissingArg}
|
ref-0-id-484
|
R( {MissingArg} ) -- R( {MissingArg} )
|
ref-0-id-485
|
{MissingArg} in0 {MissingArg}
|
ref-0-id-486
|
| {MissingArg} |
|
ref-0-id-487
|
if( {MissingArg} , {MissingArg} , {MissingArg} )
|
ref-0-id-488
|
max( {MissingArg} , {MissingArg} )
|
ref-0-id-489
|
maxR( {MissingArg} , {MissingArg} )
|
ref-0-id-490
|
{MissingArg} = {MissingArg}
|
ref-0-id-491
|
{MissingArg} != {MissingArg}
|
ref-0-id-492
|
{MissingArg} <= {MissingArg}
|
ref-0-id-493
|
{MissingArg} < {MissingArg}
|
ref-0-id-494
|
{MissingArg}
|
ref-0-id-495
|
{MissingArg} <=f {MissingArg}
|
ref-0-id-496
|
{MissingArg} sameF {MissingArg}
|
ref-0-id-497
|
{MissingArg} == {MissingArg}
|
ref-0-id-498
|
{MissingArg} !!== {MissingArg}
|
ref-0-id-499
|
{MissingArg} << {MissingArg}
|
ref-0-id-500
|
{MissingArg} <<== {MissingArg}
|
ref-0-id-501
|
{MissingArg} zermelo is {MissingArg}
|
ref-0-id-502
|
{MissingArg} is subset of {MissingArg}
|
ref-0-id-503
|
not0 {MissingArg}
|
ref-0-id-504
|
{MissingArg} zermelo ~in {MissingArg}
|
ref-0-id-505
|
{MissingArg} zermelo ~is {MissingArg}
|
ref-0-id-506
|
{MissingArg} and0 {MissingArg}
|
ref-0-id-507
|
{MissingArg} or0 {MissingArg}
|
ref-0-id-508
|
exist0 {MissingArg} indeed {MissingArg}
|
ref-0-id-509
|
{MissingArg} iff {MissingArg}
|
ref-0-id-510
|
the set of ph in {MissingArg} such that {MissingArg} end set
|