HomePage RecentChanges

mmj2UnifyingOverloads

Hi Norm,

There are 598 out of 5398 theorems (6/26/2006 set.mm) with the weq, wel,wsb problem. I believe these are the steps involved – 2078 proof steps. List enclosed below… All remaining theorems are satisfactorily unified (without being told the Ref label on each step, I might add.)

Notice that opeq2 is used by fcoi2 but both of these are class only assertions! So, inside the proofs they descend to the set variable level even though then end result is all class variables. Hmmm.

My problem with "DisableGrammarRule?" is that wcel, etc. are defined much later than wel etc. So the intervening statements fail in the parse step. And, if I try moving wcel to be right after wel that seems to cause problems in existing proofs because the order of hypotheses changes.

And, hardcoding for weq, wel, and wsb is problematic because I don't know exactly when to do it! I cannot do it all the time because weq has its own uses, and so I almost have to wait for unification failure before trying to do fix-up on the parse tree, and how do I know that the error is not caused by something else, like a user error.

So this is the old ambiguity problem again – set.mm requires two different parse trees for a given expression, depending on the context of its use. It wants "x = y" to be considered as "set = set" in the formula the user sees, but the proof may need it parsed as either "class = class" or "set = set", depending on which theorem is used as justification.

It seems as if there ought to be a way to create alternate proofs that don't run into this problem – alternate set only versions of assertions such as eleq1, opeq2, etc. But there are 317!

I'm about ready to declare victory and withdraw my troops on this one, and document the "feature" that the mmj2 GUI Proof Assistant cannot unify conflicting overloaded operators.

    "Ref","Theorem","Step","ID"
    "eleq1","cleqf","6",1
    "eleq1","cleqf","7",2
    "eleq1","hblem","2",3
    "eleq1","hblem","3",4
    "hbeq","hbel","4",5
    "hbel","hbeleq","4",6
    "hbeq","hbeleq","qed",7
    "eqeq1","clelab","9",8
    "hbel","sbabel","5",9
    "eqab","sbabel","18",10
    "eqab","sbabel","20",11
    "eleq1","rgen2","5",12
    "eleq1","rgen2","15",13
    "hbel","hbrab","4",14
    "eleq1","ralcom2","3",15
    "eleq1","ralcom2","9",16
    "eleq1","ralcom2","19",17
    "eleq1","ralcom2","28",18
    "eleq1","cbvralf","12",19
    "eleq1","cbvrex","8",20
    "eleq1","cbvreuv","4",21
    "eleq1","reu2","10",22
    "eqid","visset","1",23
    "eqeq1","vtoclgf","9",24
    "eqeq1","cla4gf","8",25
    "eqeq2","eqvinc","10",26
    "eqeq1","eqvinc","13",27
    "eqeq1","eqvinc","14",28
    "eqeq1","eqvincf","9",29
    "eqeq1","eqvincf","10",30
    "eqeq2","alexeq","2",31
    "eqeq2","alexeq","5",32
    "eqeq2","ceqex","4",33
    "eqeq2","ceqex","5",34
    "alexeq","ceqex","15",35
    "elabf","cbvab","8",36
    "hbel","cbvrab","7",37
    "hbel","cbvrab","10",38
    "eleq1","cbvrab","12",39
    "eqtr3t","eueq","1",40
    "eqeq1","eueq","5",41
    "eqeq2","moeq3","4",42
    "eueq3","moeq3","11",43
    "eueq3","moeq3","16",44
    "eqeq2","mo2icl","1",45
    "eleq1","ru","2",46
    "eleq12d","ru","5",47
    "df-nel","ru","7",48
    "eqab","ru","12",49
    "eqeq1","vsbcint","3",50
    "ceqsexv","vsbcint","4",51
    "raleq","sbralie","8",52
    "dfsbcq","sbceq1","1",53
    "dfsbcq","a4sbc","1",54
    "dfsbcq","hbsbcg","2",55
    "hbeq","hbsbcg","4",56
    "dfsbcq","hbsbcg","5",57
    "dfsbcq","sbcco","1",58
    "dfsbcq","sbcco","2",59
    "eqcom","sbcco2","3",60
    "dfsbcq","sbcn","1",61
    "dfsbcq","sbcn","2",62
    "dfsbcq","sbcim","1",63
    "dfsbcq","sbcim","2",64
    "dfsbcq","sbcim","3",65
    "dfsbcq","sbcan","1",66
    "dfsbcq","sbcan","2",67
    "dfsbcq","sbcan","3",68
    "dfsbcq","sbcor","1",69
    "dfsbcq","sbcor","2",70
    "dfsbcq","sbcor","3",71
    "dfsbcq","sbcbi","1",72
    "dfsbcq","sbcbi","2",73
    "dfsbcq","sbcbi","3",74
    "dfsbcq","sbcal","1",75
    "dfsbcq","sbcal","2",76
    "dfsbcq","sbcex","1",77
    "dfsbcq","sbcex","2",78
    "eleq2","axrep","2",79
    "eleq2","axrep","27",80
    "vtocl","axrep","32",81
    "vtoclf","axrep2","qed",82
    "hbeq","zfrepclf","5",83
    "eleq2","zfrepclf","6",84
    "hbeq","zfrepclf","13",85
    "eleq2","zfrepclf","14",86
    "eqab","zfrep4","11",87
    "eleq1","zfaus","15",88
    "ceqsexv","zfaus","17",89
    "zfaus","bm1.3ii","8",90
    "zfaus","nalset","3",91
    "dfcleq","nvelv","5",92
    "eleq1","dfss2f","6",93
    "eleq1","dfss2f","7",94
    "dfcleq","inex1","3",95
    "eqid","dfnul2","4",96
    "eqid","dfnul3","2",97
    "eqid","noel","1",98
    "eleq1","abn0","4",99
    "eq0","0el","2",100
    "zfaus","zfnul","2",101
    "hbel","hbif","5",102
    "hbel","hbif","8",103
    "hbel","hbpw","4",104
    "hbss","hbpw","5",105
    "dfss2","pwex","5",106
    "eqab","pwex","13",107
    "eleq2","el","4",108
    "eleq2","rext","4",109
    "eleq2","rext","5",110
    "elsn","rext","9",111
    "df-sn","moabex","3",112
    "elsn","exss","20",113
    "dfss2","pwpw0","1",114
    "n0","pwpw0","7",115
    "df-clel","pwpw0","8",116
    "eqeq2","dtru","3",117
    "eqeq2","dtru","8",118
    "eqcom","dtru","13",119
    "dfpr2","zfpair","1",120
    "opth","copsexg","8",121
    "ceqex","copsexg","10",122
    "ceqex","copsexg","11",123
    "opth","copsexg","18",124
    "opth2","moop2","4",125
    "hbop","moop2","11",126
    "opeq2","moop2","16",127
    "elsn","eusn","2",128
    "sneq","eusn","11",129
    "eleq1","eluni","5",130
    "hbel","hbuni","4",131
    "eluni","hbuni","7",132
    "eluni","hbuni","8",133
    "eleq2","eluniab","6",134
    "eleq1","eluniab","7",135
    "clel3","unpr","10",136
    "clel3","unpr","13",137
    "eluni","uniun","7",138
    "eluni","uniun","8",139
    "eluni","uniun","11",140
    "eluni","uniin","2",141
    "eluni","uniin","10",142
    "eluni","uniin","11",143
    "eluni","ssuni","5",144
    "dfss2","ssuni","9",145
    "n0","uni0b","6",146
    "eluni2","uni0b","8",147
    "eluni","unissb","2",148
    "dfss2","unissb","13",149
    "sseq1","unisseq","6",150
    "elrab","unisseq","7",151
    "eluni","uniex","5",152
    "dfcleq","uniex","11",153
    "hbeq","euuni","10",154
    "eqeq2","euuni","12",155
    "eluni","unipw","1",156
    "ssel","unipw","4",157
    "eleq2","unipw","13",158
    "eluni","unipw","20",159
    "eleq1","elint","2",160
    "eleq1","elintg","2",161
    "elint2","elintg","6",162
    "eleq1","elinti","1",163
    "elint","elinti","5",164
    "hbel","hbint","3",165
    "elint","hbint","8",166
    "elint","hbint","10",167
    "eleq1","elintab","7",168
    "eleq2","elintab","10",169
    "eqid","int0","4",170
    "eleq2","intss1","2",171
    "elint","intss1","7",172
    "elint2","ssint","3",173
    "dfss3","ssint","6",174
    "sseq2","ssintub","2",175
    "elrab","ssintub","3",176
    "eleq2","intmin","3",177
    "elintrab","intmin","8",178
    "elint","intss","4",179
    "elint","intss","6",180
    "elint","intun","8",181
    "elint","intun","10",182
    "elint","intun","14",183
    "clel4","intpr","10",184
    "clel4","intpr","11",185
    "elint","intpr","15",186
    "clel3","dfiun2","3",187
    "eqeq1","dfiun2","16",188
    "elab","dfiun2","18",189
    "clel4","dfiin2","3",190
    "eqeq1","dfiin2","15",191
    "elab","dfiin2","17",192
    "elrabsf","iunrab","13",193
    "df-iun","uniiun","2",194
    "df-iin","intiin","2",195
    "elun","iinuni","2",196
    "elint2","iinuni","5",197
    "elun","iununi","13",198
    "eluni2","iununi","17",199
    "eluni","iununi","24",200
    "eluni","dftr2","4",201
    "df-ral","dftr5","5",202
    "eleq2","trel","6",203
    "breq1","brab1","2",204
    "elab","brab1","3",205
    "opth","opabid","13",206
    "opeq1","opabid","30",207
    "opeq2","opabid","40",208
    "eqid","biopabi","2",209
    "opeq12","cbvopab","14",210
    "opeq1","cbvopab1","10",211
    "opeq1","cbvopab1s","6",212
    "opeq1","cbvopab1v","2",213
    "opeq2","cbvopab2v","2",214
    "opeq12","opabsb","16",215
    "eleq1","epelc","3",216
    "epelc","epel","qed",217
    "eqeq1","ideqg","1",218
    "eqeq1","solin","2",219
    "eqid","so","2",220
    "eleq1","so","5",221
    "eqeq2","so","7",222
    "breq1","so","8",223
    "breq2","so","10",224
    "eleq1","so","20",225
    "eleq1","so","37",226
    "eleq1","supmo","2",227
    "breq1","supmo","3",228
    "breq2","supmo","6",229
    "breq1","supmo","12",230
    "breq1","supmo","13",231
    "rcla4v","supmo","16",232
    "breq2","supmo","20",233
    "breq1","supmo","30",234
    "breq1","supmo","31",235
    "rcla4v","supmo","34",236
    "breq2","supmo","38",237
    "sotrieq2","supmo","49",238
    "breq2","supub","5",239
    "rcla4v","supub","7",240
    "breq1","suplub","7",241
    "breq1","suplub","8",242
    "rcla4v","suplub","11",243
    "breq1","dffr2","4",244
    "elab","dffr2","5",245
    "breq2","dffr2","10",246
    "elsn","frirr","10",247
    "breq2","frirr","11",248
    "breq1","frirr","16",249
    "elab","frirr","17",250
    "breq2","fr2nr","5",251
    "breq2","fr2nr","18",252
    "elpr","fr2nr","33",253
    "breq2","fr3nr","6",254
    "breq2","fr3nr","19",255
    "breq2","fr3nr","32",256
    "eltp","fr3nr","47",257
    "eleq1","efrirr","2",258
    "frirr","efrirr","7",259
    "abid2","dfepfr","4",260
    "abid2","epfrc","6",261
    "solin","dfwe2","2",262
    "breq2","dfwe2","10",263
    "breq2","dfwe2","45",264
    "eqeq2","dfwe2","46",265
    "breq1","dfwe2","47",266
    "solin","wecmpep","1",267
    "ineq2","wefrc","2",268
    "rcla4ev","wefrc","4",269
    "elin","wefrc","15",270
    "elin","wefrc","32",271
    "dfss3","wefrc","37",272
    "solin","wereu","5",273
    "breq1","wereu","18",274
    "rcla4v","wereu","20",275
    "breq1","wereu","21",276
    "rcla4v","wereu","23",277
    "breq2","wereu","35",278
    "trel3","ordelord","11",279
    "trel","ordelord","20",280
    "dftr2","ordelord","33",281
    "eleq1","tz7.7","25",282
    "trel","tz7.7","32",283
    "ssrdv","tz7.7","46",284
    "ineq2","onfr","2",285
    "rcla4ev","onfr","4",286
    "ssel","onfr","7",287
    "sseli","onfr","20",288
    "trss","onfr","21",289
    "sseli","onfr","23",290
    "ra4e","onfr","39",291
    "n0","onfr","50",292
    "ordelord","ordon","3",293
    "ssrdv","ordon","11",294
    "ordtri3or","ordon","15",295
    "hbral","tfis","6",296
    "eleq1","tfis","10",297
    "raleq","tfis","11",298
    "elrabsf","tfis","18",299
    "elrabsf","tfis","25",300
    "trss","ssorduni","8",301
    "eluni2","ssorduni","16",302
    "ordelord","ssorduni","23",303
    "eluni2","ssorduni","31",304
    "sseq2","ordunidif","24",305
    "rcla4ev","ordunidif","25",306
    "ontri1","onint","2",307
    "ssel","onint","3",308
    "disj","onint","10",309
    "elint2","onint","12",310
    "ssrdv","onint","20",311
    "eleq2","onminex","15",312
    "eleq1","onminex","31",313
    "elab","onminex","33",314
    "df-ral","onminex","46",315
    "dfcleq","sucel","2",316
    "eluni2","unon","1",317
    "onelon","unon","2",318
    "limeq","limuni2","1",319
    "rcla4v","limuni2","2",320
    "limeq","limuni2","12",321
    "rcla4v","limuni2","13",322
    "limeq","limuni2","22",323
    "rcla4v","limuni2","23",324
    "limsuc","limuni2","25",325
    "eluni2","limuni2","33",326
    "ontri1","dfom2","5",327
    "limeq","dfom2","8",328
    "elrab","dfom2","10",329
    "eleq1","elom","3",330
    "eleq1","elomg","3",331
    "elom","elomg","8",332
    "elom","omsson","2",333
    "eleq2","limomss","4",334
    "elom","limomss","8",335
    "ordelord","ordom","2",336
    "trel","ordom","6",337
    "elom","ordom","16",338
    "elom","ordom","22",339
    "limeq","omssnlim","4",340
    "elrab","omssnlim","6",341
    "eleq2","peano5","22",342
    "minel","peano5","28",343
    "elab","finds","11",344
    "sseq2","findsg","22",345
    "elab","finds2","13",346
    "dfsbcq","findes","3",347
    "dfsbcq","findes","5",348
    "eleq1","findes","14",349
    "suceq","findes","16",350
    "finds","findes","qed",351
    "rcla4v","tfinds","44",352
    "sseq2","tfindsg","23",353
    "onelon","tfindsg2","33",354
    "biraldva","tfindsg2","39",355
    "dfsbcq","tfindes","4",356
    "dfsbcq","tfindes","6",357
    "eleq1","tfindes","15",358
    "suceq","tfindes","17",359
    "tfinds","tfindes","qed",360
    "sbcel1","tfinds2","14",361
    "sbcie","tfinds2","22",362
    "suceq","tfinds2","28",363
    "limeq","tfinds2","37",364
    "hbel","hbxp","5",365
    "hbel","hbxp","7",366
    "opth","opelxp","12",367
    "df-clel","opelxp","24",368
    "ssel","weinxp","1",369
    "ssel","weinxp","2",370
    "biraldva","weinxp","11",371
    "birexdva","weinxp","12",372
    "eluni2","reluni","2",373
    "dfss2","reluni","7",374
    "hbbr","hbco","5",375
    "hbbr","hbco","8",376
    "hbbr","hbcnv","5",377
    "opeq2","dfdmf","7",378
    "opeq1","dfdmf","15",379
    "eqid","dm0","3",380
    "eqid","dmsn0","6",381
    "eqid","dmsnsn0","12",382
    "ideq","dmi","4",383
    "eqcom","dmi","5",384
    "eqid","dmi","9",385
    "opeq1","dfrnf","7",386
    "opeq2","dfrnf","15",387
    "hbel","hbrn","4",388
    "ideq","iss","5",389
    "ideq","iss","13",390
    "eqcom","iss","17",391
    "opeq2","iss","22",392
    "ceqsexv","iss","24",393
    "opeq2","iss","30",394
    "ideq","iss","40",395
    "hbel","hbima","4",396
    "hbop","hbima","7",397
    "ideq","imai","5",398
    "eleq1","imai","12",399
    "ceqsexv","imai","13",400
    "ideq","intasym","18",401
    "opeq2","intirr","10",402
    "ceqsexv","intirr","12",403
    "ideq","intirr","19",404
    "eqcom","intirr","21",405
    "opeq1","cnvopab","13",406
    "opeq2","cnvopab","15",407
    "opeq2","cnvopab","25",408
    "opeq1","cnvopab","27",409
    "eqcom","cnvi","3",410
    "ideq","cnvi","7",411
    "ideq","cnvi","15",412
    "eluni","imaiun","1",413
    "elima3","imaiun","15",414
    "ideq","coi1","7",415
    "eqcom","coi1","8",416
    "breq1","coi1","13",417
    "ceqsexv","coi1","14",418
    "breq12d","cnvpo","20",419
    "eqcom","cnvso","6",420
    "breq2","dffun3","2",421
    "hbbr","dffunmof","6",422
    "breq2","dffunmof","8",423
    "hbbr","dffunmof","16",424
    "breq1","dffunmof","20",425
    "eqtr3t","funsn","5",426
    "funeq","fununi","32",427
    "sseq1","fununi","33",428
    "sseq2","fununi","34",429
    "sseq2","fununi","37",430
    "sseq1","fununi","38",431
    "sseq1","fununi","43",432
    "sseq2","fununi","44",433
    "funeq","fununi","49",434
    "sseq2","fununi","50",435
    "sseq1","fununi","51",436
    "cnveq","funcnvuni","1",437
    "sseq1","funcnvuni","4",438
    "sseq2","funcnvuni","5",439
    "rcla4v","funcnvuni","9",440
    "sseq2","funcnvuni","13",441
    "sseq1","funcnvuni","14",442
    "rcla4v","funcnvuni","16",443
    "cnveq","funcnvuni","35",444
    "eqeq1","funcnvuni","42",445
    "elab","funcnvuni","44",446
    "eqeq1","funcnvuni","47",447
    "elab","funcnvuni","49",448
    "dfima3","funimaexg","9",449
    "eqab","funimaexg","11",450
    "rexeqf","zfrep6","9",451
    "df-rab","zfrep6","21",452
    "df-ral","zfrep6","31",453
    "df-rab","zfrep6","43",454
    "eleq2d","zfrep6","46",455
    "r19.21ai","zfrep6","60",456
    "opeq2","fnopabg","38",457
    "ideq","fcoi1","15",458
    "eqcom","fcoi1","17",459
    "opeq1","fcoi1","26",460
    "ceqsexv","fcoi1","29",461
    "ideq","fcoi2","16",462
    "opeq2","fcoi2","25",463
    "eleq1","fcoi2","27",464
    "ceqsexv","fcoi2","29",465
    "elsn","fv2","14",466
    "elfv","fv3","2",467
    "breq2","fv3","6",468
    "ceqsalv","fv3","7",469
    "eleq2","fv3","11",470
    "breq2","fv3","12",471
    "eqrd","tz6.12-1","qed",472
    "opeq2","tz6.12f","3",473
    "opeq2","tz6.12f","8",474
    "eqeq2","tz6.12f","13",475
    "elab","tz6.12-2","5",476
    "eleq1","fnopabfv","15",477
    "fveq2","fnopabfv","16",478
    "eqeq1","fnopabfv","19",479
    "opelopab","fnopabfv","21",480
    "eqeq1","fvopabn","13",481
    "opelopabg","fvopabn","14",482
    "eqvincf","fvopabgf","6",483
    "eqeqan12rd","fvopabgf","24",484
    "eqvincf","fvopabnf","6",485
    "eqeqan12rd","fvopabnf","24",486
    "hbfv","fvopab2","5",487
    "hbfv","cleqfvf","5",488
    "hbfv","cleqfvf","7",489
    "fveq2","cleqfvf","10",490
    "fveq2","cleqfvf","11",491
    "hbfv","elrnopab","13",492
    "fveq2","elrnopab","17",493
    "eleq1","chfnrn","5",494
    "eluni2","chfnrn","10",495
    "opeq1","fvrn","8",496
    "cla4ev","fvrn","10",497
    "eqid","fvi","9",498
    "ideq","fvi","12",499
    "fveq2","fconstfv","17",500
    "rcla4v","fconstfv","19",501
    "fveq2","fvresex","4",502
    "fvopab","fvresex","5",503
    "hbfv","abrexexlem2","17",504
    "hbeq","abrexexlem2","18",505
    "fveq2","abrexexlem2","19",506
    "hbfv","abrexexlem2","29",507
    "hbeq","abrexexlem2","30",508
    "eqeq1","abrexexlem2","32",509
    "breq1","f1fv","45",510
    "hbfv","f1fvf","5",511
    "hbfv","f1fvf","7",512
    "fveq2","f1fvf","14",513
    "eqeq2","f1fvf","16",514
    "hbfv","f1fvf","22",515
    "hbfv","f1fvf","24",516
    "fveq2","f1fvf","30",517
    "eqeq1","f1fvf","32",518
    "eqeq1","f1fveq","3",519
    "hbel","hbiso","8",520
    "hbel","hbiso","10",521
    "hbbr","hbiso","13",522
    "hbfv","hbiso","15",523
    "hbfv","hbiso","17",524
    "breq1","isotr","28",525
    "fveq2","isotr","29",526
    "breq2","isotr","32",527
    "fveq2","isotr","33",528
    "rcla42v","isotr","36",529
    "ssel","isofrlem","20",530
    "funfvima","isofrlem","21",531
    "n0","isofrlem","29",532
    "ssel","isofrlem","51",533
    "r19.22dv","isofrlem","67",534
    "f1fveq","isowe","3",535
    "eqeq1","isowe","29",536
    "f1fveq","f1oiso","3",537
    "eqcom","f1oiso","4",538
    "breq1","f1oiso","14",539
    "ceqsrexv","f1oiso","17",540
    "f1fveq","f1oiso","20",541
    "eqcom","f1oiso","21",542
    "breq2","f1oiso","26",543
    "ceqsrexv","f1oiso","27",544
    "fveq2","f1owe","2",545
    "fveq2","f1owe","4",546
    "brabg","f1owe","6",547
    "funfvima2","f1oweALT","18",548
    "n0","f1oweALT","22",549
    "fvres","f1oweALT","45",550
    "fvres","f1oweALT","46",551
    "fveq2","f1oweALT","50",552
    "fveq2","f1oweALT","52",553
    "brab","f1oweALT","54",554
    "biraldva","f1oweALT","57",555
    "birexa","f1oweALT","58",556
    "fveq2","f1oweALT","79",557
    "fveq2","f1oweALT","81",558
    "brab","f1oweALT","83",559
    "f1fveq","f1oweALT","85",560
    "fveq2","f1oweALT","89",561
    "fveq2","f1oweALT","91",562
    "brab","f1oweALT","93",563
    "eqeq2","f1oweALT","104",564
    "fveq2","canth","5",565
    "eleq12d","canth","6",566
    "elrab","canth","8",567
    "sseq1","tfrlem1","8",568
    "raleq","tfrlem1","10",569
    "raleq","tfrlem1","12",570
    "onelsst","tfrlem1","14",571
    "ssel","tfrlem1","19",572
    "ra4","tfrlem1","20",573
    "r19.21ad","tfrlem1","22",574
    "r19.21adv","tfrlem1","26",575
    "onelsst","tfrlem1","27",576
    "r19.20dva","tfrlem1","41",577
    "raleq","tfrlem1","46",578
    "fveq2","tfrlem1","47",579
    "fveq2","tfrlem1","48",580
    "fveq2","tfrlem2","9",581
    "fveq2","tfrlem2","10",582
    "rcla4v","tfrlem2","12",583
    "eqeq12","tfrlem2","32",584
    "fneq1","tfrlem3","3",585
    "fveq1","tfrlem3","4",586
    "reseq1","tfrlem3","5",587
    "elab","tfrlem3","11",588
    "fneq2","tfrlem3","12",589
    "raleq","tfrlem3","13",590
    "r19.26m","tfrlem5","20",591
    "elin","tfrlem5","23",592
    "fnop","tfrlem8","16",593
    "ontr1","tfrlem8","43",594
    "ssel","tfrlem8","44",595
    "onelon","tfrlem8","60",596
    "fnop","tfrlem8","63",597
    "fnop","tfrlem9","12",598
    "ra4","tfrlem9","19",599
    "eleq2d","tfrlem9","22",600
    "fveq2","tfr2","3",601
    "reseq2","tfr2","4",602
    "vtoclga","tfr2","qed",603
    "fveq2","tfr3","11",604
    "fveq2","tfr3","12",605
    "hbeq","hbrdg","15",606
    "hbral","hbrdg","20",607
    "fveq2","rdglem1","3",608
    "reseq2","rdglem1","4",609
    "opeq1","rdglem2","1",610
    "eqeq1","rdglem2","3",611
    "eqeq1","rdglem2","5",612
    "dmeq","rdglem2","6",613
    "dmeq","rdglem2","11",614
    "fveq1","rdglem2","15",615
    "dmeq","rdglem2","20",616
    "rneq","rdglem2","23",617
    "ordtri3","tz7.48lem","17",618
    "r2al","tz7.48lem","38",619
    "eleq1","tz7.48lem","41",620
    "fveq2","tz7.48lem","42",621
    "eleq2","tz7.48lem","48",622
    "fveq2","tz7.48lem","49",623
    "eleq1","tz7.48lem","55",624
    "fveq2","tz7.48lem","56",625
    "eleq2","tz7.48lem","62",626
    "fveq2","tz7.48lem","63",627
    "onelon","tz7.48-2","2",628
    "elin","tz7.48-2","6",629
    "fvres","tz7.48-2","15",630
    "r19.21aiv","tz7.48-2","34",631
    "imaeq2","tz7.49","9",632
    "ra4","tz7.49","21",633
    "onelon","tz7.49","23",634
    "imaeq2","tz7.49","24",635
    "fveq2","tz7.49","28",636
    "imaeq2","tz7.49","29",637
    "rcla4v","tz7.49","33",638
    "r19.23ad","tz7.49","47",639
    "ssel","tz7.49","65",640
    "funfvima2","tz7.49","72",641
    "ra4","tz7.49","76",642
    "ssel","tz7.49","79",643
    "imaeq2","tz7.49","80",644
    "fveq2","tz7.49","84",645
    "imaeq2","tz7.49","85",646
    "rcla4v","tz7.49","89",647
    "r2al","tz7.49","105",648
    "fveq2","abianfplem","5",649
    "hbrdg","abianfplem","20",650
    "hbfv","abianfplem","26",651
    "rdgsucopab","abianfplem","29",652
    "iuneq2i","abianfplem","42",653
    "fveq2","abianfp","76",654
    "eqeq12d","abianfp","78",655
    "eqid","bioprabi","2",656
    "opeq12","cbvoprab12","18",657
    "eqcoms","oprabval4g","4",658
    "eqcoms","oprabval4g","7",659
    "eleq1","oprabval4g","22",660
    "eleq1","oprabval4g","23",661
    "eqcoms","oprabval4g","27",662
    "eqcoms","oprabval4g","30",663
    "oprabval2g","oprabval4g","36",664
    "opeq1","elrnoprab","20",665
    "opeq2","elrnoprab","35",666
    "eqeq2","caoprcan","13",667
    "eleq1","caoprmo","8",668
    "opreq2","caoprmo","9",669
    "opreq1","caoprmo","14",670
    "eqeq12d","caoprmo","16",671
    "vtoclga","caoprmo","17",672
    "opreq1","caoprmo","30",673
    "eqeq12d","caoprmo","32",674
    "vtoclga","caoprmo","33",675
    "eqtr3d","caoprmo","41",676
    "eqid","1st2val","6",677
    "oprabval2","1st2val","13",678
    "fnoprab2","df1st2","7",679
    "opreq2","oacl","3",680
    "opreq2","omcl","3",681
    "opreq2","oecl","21",682
    "opreq2","oa0r","4",683
    "eqeq12d","oa0r","6",684
    "opreq2","om0r","3",685
    "opreq2","om1r","4",686
    "eqeq12d","om1r","6",687
    "opreq2","oe1m","3",688
    "opreq2","oaordi","10",689
    "opreq2","oawordri","4",690
    "opreq2","oawordri","5",691
    "opreq2","oawordeulem","49",692
    "onnminsb","oawordeulem","51",693
    "opreq2","oawordeulem","88",694
    "onnminsb","oawordeulem","90",695
    "oacan","oawordeulem","154",696
    "opreq2","oawordeulem","160",697
    "opreq2","oaass","5",698
    "opreq2","oaass","6",699
    "oaord","oaass","91",700
    "r19.22dv2","oaass","103",701
    "onelon","oaass","117",702
    "birexdva","oaass","128",703
    "oaordi","oaass","140",704
    "r19.23adv","oaass","147",705
    "opreq2","oarec","6",706
    "rexeq","oarec","7",707
    "elsuc","oarec","37",708
    "df-rex","oarec","45",709
    "opreq2","oarec","47",710
    "ceqsexv","oarec","49",711
    "ordtr1","oarec","75",712
    "r19.22dv2","oarec","81",713
    "r19.23adv","oarec","83",714
    "hbrex","oarec","87",715
    "limsuc","oarec","88",716
    "sucidg","oarec","90",717
    "eleq2","oarec","94",718
    "ra4e","oarec","97",719
    "r19.23ad","oarec","103",720
    "eleq2","omordi","7",721
    "opreq2","omordi","8",722
    "opreq2","omwordri","4",723
    "opreq2","omwordri","5",724
    "opreq2","odi","6",725
    "opreq2","odi","8",726
    "oaord","odi","96",727
    "omordi","odi","150",728
    "opreq2","odi","158",729
    "opreq2","odi","160",730
    "rcla4v","odi","163",731
    "oaordi","odi","197",732
    "ordelon","odi","213",733
    "opreq2","odi","219",734
    "opreq2","odi","221",735
    "rcla4v","odi","224",736
    "ordelon","odi","234",737
    "r19.23adv","odi","249",738
    "opreq2","omass","5",739
    "opreq2","omass","6",740
    "omordi","omass","56",741
    "r19.21aiv","omass","69",742
    "onelon","omass","92",743
    "r19.22dv","omass","103",744
    "opreq2","oen0","3",745
    "opreq2","oeordi","4",746
    "opreq2","oewordri","4",747
    "opreq2","oewordri","5",748
    "opreq2","oeworde","5",749
    "sseq12d","oeworde","6",750
    "opreq2","oelim2","85",751
    "opreq2","nnacl","4",752
    "opreq2","nnmcl","4",753
    "opreq1","nnacom","5",754
    "opreq2","nnacom","6",755
    "opreq2","nnacom","26",756
    "opreq2","nnacom","27",757
    "opreq2","nnmsucr","7",758
    "opreq2","nnmsucr","8",759
    "opreq12d","nnmsucr","10",760
    "opreq1","nnmcom","5",761
    "opreq2","nnmcom","6",762
    "opreq2","oaabs","11",763
    "eqeq12d","oaabs","13",764
    "ordelon","oaabs","47",765
    "eldif","oaabs","57",766
    "biraldv2","oaabs","62",767
    "eleq2","omsmolem","1",768
    "eleq2","omsmolem","5",769
    "fveq2","omsmolem","6",770
    "eleq2","omsmolem","9",771
    "fveq2","omsmolem","16",772
    "suceq","omsmolem","17",773
    "rcla4v","omsmolem","20",774
    "fveq2","omsmolem","38",775
    "fveq2","omsmolem","40",776
    "suceq","omsmolem","41",777
    "rcla4v","omsmolem","44",778
    "elsuc","omsmolem","52",779
    "ordtri3","omsmo","31",780
    "ideq","ider","4",781
    "ideq","ider","7",782
    "eqtrt","ider","9",783
    "ideq","ider","12",784
    "ideq","ider","15",785
    "ideq","ider","19",786
    "eleq1","ecelqsi","6",787
    "eceq2","ecelqsi","7",788
    "eqeq2i","qsid","5",789
    "eqcom","qsid","6",790
    "risset","qsid","9",791
    "eqeq12","th3qlem1","35",792
    "eqeq1","th3qlem1","76",793
    "eceq2","th3qlem1","79",794
    "eceq2","th3qlem1","81",795
    "opreq12","th3qlem1","84",796
    "opbrop","oprec","17",797
    "opbrop","oprec","18",798
    "oprabval3","oprec","20",799
    "oprabval3","oprec","21",800
    "hbfv","dom2d","16",801
    "eleq1","dom2d","20",802
    "eleq1","dom2d","23",803
    "fveq2","dom2d","28",804
    "ideq","idssen","4",805
    "f1oeq3","idssen","6",806
    "eqeq1","2dom","6",807
    "eqeq1","fundmen","18",808
    "opeq1","fundmen","25",809
    "eqeq1","fundmen","34",810
    "opeq1","fundmen","41",811
    "eqeq2d","mapsnen","19",812
    "eleq1","mapsnen","30",813
    "opeq2","mapsnen","31",814
    "ceqsexv","mapsnen","35",815
    "f1fveq","xpdom2","65",816
    "opth","xpdom2","71",817
    "eqeq12","xpdom2","79",818
    "opth","xpdom2","83",819
    "elin","pw2en","41",820
    "eleq1","pw2en","44",821
    "eleq1","pw2en","45",822
    "opelopab","pw2en","52",823
    "eleq2","pw2en","112",824
    "eleq2","pw2en","143",825
    "cleqfvf","pw2en","193",826
    "sseq1","sbth","12",827
    "imaeq2","sbth","13",828
    "difeq2","sbth","18",829
    "sneqr","canth2","7",830
    "sneq","canth2","8",831
    "coeq2","mapenlem1","7",832
    "fvopab4","mapenlem1","15",833
    "cleqfv","mapenlem2","51",834
    "unineq","mapdom2","42",835
    "breq1","ssenen","27",836
    "elab","ssenen","28",837
    "breq1","ssenen","65",838
    "elab","ssenen","66",839
    "suc11","limenpsi","14",840
    "eqeq1","nneneq","6",841
    "breq1","nneneq","9",842
    "eqeq1","nneneq","10",843
    "eqeq1","nneneq","14",844
    "eqeq1","nneneq","18",845
    "suceq","nneneq","51",846
    "breq2","nneneq","64",847
    "eqeq2","nneneq","65",848
    "breq2","php3","94",849
    "breq2","ominf","1",850
    "psseq2","pssnn","13",851
    "rexeq","pssnn","14",852
    "eleq1","pssnn","30",853
    "sseld","pssnn","35",854
    "elsuci","pssnn","36",855
    "ssrdv","pssnn","45",856
    "dfpss2","pssnn","47",857
    "elelsuc","pssnn","49",858
    "r19.22i2","pssnn","51",859
    "eleq2","pssnn","65",860
    "eldifi","pssnn","66",861
    "elsuci","pssnn","69",862
    "eleq1a","pssnn","71",863
    "pssnel","pssnn","80",864
    "psseq1","pssnn","87",865
    "breq1","pssnn","88",866
    "ordsucelsuc","pssnn","103",867
    "snssi","pssnn","108",868
    "elnn","pssnn","133",869
    "df-rex","pssnn","143",870
    "breq2","pssnn","144",871
    "eqelsuc","pssnn","152",872
    "breq2","pssnn","156",873
    "rcla4ev","pssnn","157",874
    "breq2","ssfi","37",875
    "eleq1","unblem1","27",876
    "fveq2","unblem2","5",877
    "eleq1","unblem2","14",878
    "hbfv","unblem2","36",879
    "frsucopab","unblem2","43",880
    "hbfv","unblem3","23",881
    "frsucopab","unblem3","30",882
    "sucssel","unbnn2","7",883
    "ordtri1","isfinite2","16",884
    "ssel2","isfinite2","17",885
    "biraldva","isfinite2","23",886
    "opreq2","unfilem2","13",887
    "fvopab4","unfilem2","15",888
    "opreq2","unfilem2","16",889
    "fvopab4","unfilem2","18",890
    "nnacan","unfilem2","20",891
    "breq2","unfi","27",892
    "breq2","unfi","34",893
    "ineq1","fiint","1",894
    "ineq2","fiint","5",895
    "breq1","fiint","13",896
    "eleq2","zfregcl","2",897
    "eleq2","zfregcl","4",898
    "df-ral","zfregcl","11",899
    "df-rex","zfregcl","13",900
    "eleq1","eirrv","1",901
    "elsn","eirrv","11",902
    "eleq1","eirrv","15",903
    "rcla4v","eirrv","17",904
    "eleq2","eirr","1",905
    "eleq1","en2lp","1",906
    "eleq2","en2lp","2",907
    "hbrdg","inf0","22",908
    "hbfv","inf0","26",909
    "frsucopab","inf0","30",910
    "eleq2","inf0","43",911
    "eleq2","inf0","60",912
    "eleq2","inf0","61",913
    "eleq2","inf0","62",914
    "eleq1","inf0","70",915
    "eleq1","inf0","71",916
    "n0i","inf1","2",917
    "dfss2","inf2","3",918
    "eluni","inf2","4",919
    "sseq2","inf3lema","6",920
    "ineq1","inf3lema","8",921
    "eqeqan12rd","inf3lema","12",922
    "inf3lema","inf3lemd","13",923
    "ssrdv","inf3lemd","16",924
    "fveq2","inf3lem1","9",925
    "suceq","inf3lem1","10",926
    "inf3lema","inf3lem1","30",927
    "inf3lema","inf3lem1","41",928
    "fveq2","inf3lem2","9",929
    "ssel","inf3lem2","28",930
    "eluni","inf3lem2","29",931
    "inf3lema","inf3lem2","36",932
    "elin","inf3lem2","39",933
    "eleq2","inf3lem2","42",934
    "pssnel","inf3lem2","58",935
    "eldifi","inf3lem3","13",936
    "inf3lema","inf3lem3","19",937
    "fveq2","inf3lem5","14",938
    "inf3lem5","inf3lem6","7",939
    "inf3lem5","inf3lem6","16",940
    "ordtri3","inf3lem6","28",941
    "eleq2","inf4","8",942
    "df-rex","inf4","16",943
    "sucel","inf4","18",944
    "df-rex","inf4","19",945
    "df-rex","zfinf","3",946
    "sucel","zfinf","5",947
    "df-rex","zfinf","6",948
    "df-ral","zfinf","9",949
    "peano5","omex","2",950
    "r19.20i2","omex","4",951
    "suceq","dfom3","5",952
    "rcla4v","dfom3","7",953
    "elintab","dfom3","13",954
    "elintab","dfom3","26",955
    "eleq2","dfom3","32",956
    "elom3","dfom4","1",957
    "suceq","infensuc","6",958
    "breq12d","infensuc","7",959
    "ordeirr","infensuc","27",960
    "disjsn","infensuc","29",961
    "hbfv","trcl","40",962
    "hbfv","trcl","51",963
    "frsucopab","trcl","57",964
    "elunii","trcl","62",965
    "fveq2","trcl","73",966
    "fveq2","trcl","87",967
    "hbfv","trcl","122",968
    "hbfv","trcl","133",969
    "frsucopab","trcl","139",970
    "fveq2","trcl","149",971
    "trel","zfregs","4",972
    "elin","zfregs","10",973
    "sseli","zfregs","20",974
    "elin","zfregs","32",975
    "sseq1","setind","1",976
    "eleq1","setind","2",977
    "fveq2","r1tr","4",978
    "ssel","r1tr","24",979
    "ssrdv","r1tr","33",980
    "ra4","r1tr","48",981
    "r19.22d","r1tr","51",982
    "eleq2","r1ord","5",983
    "fveq2","r1ord","6",984
    "eleq1","tz9.12lem1","8",985
    "eqeq1","tz9.12lem1","12",986
    "opelopab","tz9.12lem1","13",987
    "fveq2","tz9.12lem3","3",988
    "rcla4ev","tz9.12lem3","5",989
    "eleq1","tz9.12lem3","11",990
    "eqeq1","tz9.12lem3","15",991
    "opelopab","tz9.12lem3","16",992
    "fveq2","tz9.12lem3","43",993
    "rcla4ev","tz9.12lem3","45",994
    "eleq1","tz9.12lem3","50",995
    "fvopabg","tz9.12lem3","53",996
    "hbfv","tz9.12lem3","71",997
    "hbfv","tz9.12lem3","84",998
    "hbel","tz9.12lem3","86",999
    "ssel","tz9.13","3",1000
    "eleq1","tz9.13","5",1001
    "elab","tz9.13","7",1002
    "r19.21aiv","tz9.13","9",1003
    "eleq1","tz9.13","14",1004
    "elab","tz9.13","16",1005
    "suceq","rankr1","33",1006
    "onintss","rankr1","36",1007
    "suceq","rankr1","61",1008
    "onintss","rankr1","64",1009
    "fveq2","r1pwcl","25",1010
    "eluni2","rankuni","12",1011
    "rankel","rankuni","19",1012
    "elintrab","rankun","7",1013
    "eleq2","rankun","24",1014
    "fveq2","rankonid","1",1015
    "eqeq12d","rankonid","3",1016
    "eleq1","rankonid","7",1017
    "dfss3","rankonid","11",1018
    "fveq2","scottex","19",1019
    "elrab","scottex","21",1020
    "fveq2","scott0","51",1021
    "rcla4ev","scott0","53",1022
    "fveq2","scottexs","7",1023
    "fveq2","scott0s","9",1024
    "elin","cp","4",1025
    "hbin","cp","12",1026
    "df-rex","cp","14",1027
    "elin","bnd2","18",1028
    "birex2","bnd2","22",1029
    "breq1","kardex","4",1030
    "elab","kardex","5",1031
    "breq1","kardex","8",1032
    "elab","kardex","9",1033
    "breq1","karden","20",1034
    "fveq2","karden","21",1035
    "breq1","karden","26",1036
    "fveq2","karden","27",1037
    "breq1","karden","43",1038
    "elab","karden","44",1039
    "breq1","karden","47",1040
    "elab","karden","48",1041
    "eleq1","aceq1","3",1042
    "eleq1","aceq1","12",1043
    "reueqd","aceq1","15",1044
    "raleqd","aceq1","16",1045
    "eleq1","aceq1","18",1046
    "reueqd","aceq1","21",1047
    "raleqd","aceq1","22",1048
    "df-reu","aceq1","32",1049
    "df-rex","aceq1","38",1050
    "eleq1","aceq1","39",1051
    "eleq2","aceq1","40",1052
    "eleq2","aceq1","41",1053
    "df-ral","aceq1","54",1054
    "eleq1","aceq1","60",1055
    "df-ral","aceq1","68",1056
    "df-ral","aceq2","3",1057
    "n0","aceq2","6",1058
    "eleq2","aceq2","7",1059
    "eleq2","aceq2","8",1060
    "eleq1","aceq2","12",1061
    "eleq1","aceq3lem","17",1062
    "breq1","aceq3lem","18",1063
    "eqeq1","aceq3lem","23",1064
    "opelopab","aceq3lem","25",1065
    "breq1","aceq3lem","52",1066
    "fvopab4","aceq3lem","56",1067
    "breq2","aceq3lem","60",1068
    "sseq1","aceq3lem","98",1069
    "fneq1","aceq3lem","99",1070
    "sseq2","aceq3","1",1071
    "dmeq","aceq3","2",1072
    "elunii","aceq3","13",1073
    "df-xp","aceq3","17",1074
    "eleq1","aceq3","33",1075
    "eleq2","aceq3","34",1076
    "elab","aceq3","37",1077
    "n0","aceq3","38",1078
    "biabrdv","aceq3","52",1079
    "eleq1","aceq3","58",1080
    "eleq2","aceq3","59",1081
    "eleq1","aceq3","61",1082
    "brab","aceq3","64",1083
    "r19.21aiv","aceq3","72",1084
    "fveq1","aceq4","2",1085
    "fveq2","aceq4","7",1086
    "fvopab4","aceq4","10",1087
    "birala","aceq4","13",1088
    "fnopab2","aceq4","17",1089
    "funopabex2","aceq4","20",1090
    "elin","aceq5lem1","1",1091
    "elxp","aceq5lem1","2",1092
    "eleq1","aceq5lem1","8",1093
    "elsn","aceq5lem1","10",1094
    "opeq1","aceq5lem1","22",1095
    "opeq1","aceq5lem1","24",1096
    "ceqsexv","aceq5lem1","28",1097
    "df-rex","aceq5lem2","10",1098
    "opelxp","aceq5lem2","27",1099
    "elsn","aceq5lem2","28",1100
    "eqcom","aceq5lem2","29",1101
    "eleq1","aceq5lem2","38",1102
    "eleq2","aceq5lem2","39",1103
    "ceqsexv","aceq5lem2","41",1104
    "3eqtr3g","aceq5lem3","33",1105
    "sneq","aceq5lem3","34",1106
    "xpeq2","aceq5lem3","37",1107
    "eqcom","aceq5lem3","40",1108
    "eleq1","aceq5lem3","47",1109
    "ceqsexv","aceq5lem3","48",1110
    "df-rex","aceq5lem3","50",1111
    "eqeq1","aceq5lem4","6",1112
    "eqeq1","aceq5lem4","8",1113
    "elab","aceq5lem4","11",1114
    "eleq2","aceq5lem4","15",1115
    "elxp","aceq5lem4","16",1116
    "eleq2","aceq5lem4","20",1117
    "elxp","aceq5lem4","21",1118
    "opeq1","aceq5lem4","28",1119
    "elsn","aceq5lem4","31",1120
    "opeq1","aceq5lem4","35",1121
    "elsn","aceq5lem4","38",1122
    "opth","aceq5lem4","47",1123
    "sneq","aceq5lem4","52",1124
    "xpeq2","aceq5lem4","55",1125
    "eqeq12","aceq5lem4","58",1126
    "r19.23aiv","aceq5lem4","62",1127
    "r19.23adv","aceq5lem4","64",1128
    "eqeq1","aceq5lem4","67",1129
    "eqeq1","aceq5lem4","69",1130
    "elab2","aceq5lem4","72",1131
    "eqeq1","aceq5lem4","75",1132
    "eqeq1","aceq5lem4","77",1133
    "elab2","aceq5lem4","80",1134
    "sneq","aceq5lem4","82",1135
    "xpeq2","aceq5lem4","85",1136
    "disj1","aceq5lem4","95",1137
    "eleq1d","aceq5lem5","42",1138
    "r19.21aiv","aceq5lem5","51",1139
    "fveq2","aceq5","2",1140
    "eleq12d","aceq5","4",1141
    "eqeq2","aceq5","5",1142
    "ineq2","aceq5","7",1143
    "rcla4v","aceq5","11",1144
    "eleq1","aceq5","12",1145
    "disj","aceq5","15",1146
    "eleq1","aceq5","22",1147
    "fveq2","aceq5","28",1148
    "r19.23adv","aceq5","35",1149
    "elin","aceq5","42",1150
    "fveq2","aceq5","49",1151
    "eleq12d","aceq5","51",1152
    "rcla4v","aceq5","52",1153
    "fnfvrn","aceq5","53",1154
    "eqeq2","aceq5","68",1155
    "r19.20dva","aceq5","75",1156
    "eqeq1","aceq5","77",1157
    "raleq","aceq5","108",1158
    "eleq2","aceq6a","1",1159
    "eleq1","aceq6a","2",1160
    "df-rab","aceq6a","7",1161
    "df-rab","aceq6a","8",1162
    "fvopab4","aceq6a","15",1163
    "r19.20i","aceq6a","20",1164
    "funopabex2","aceq6a","22",1165
    "ra4","aceq6b","3",1166
    "eleq1","aceq6b","5",1167
    "eleq1","aceq6b","6",1168
    "eqid","aceq6b","11",1169
    "eqeq1","aceq6b","12",1170
    "eqeq1","aceq6b","14",1171
    "rcla4ev","aceq6b","16",1172
    "fveq2","aceq6b","18",1173
    "preq2","aceq6b","21",1174
    "eleq2","aceq6b","38",1175
    "eqeq1","aceq6b","49",1176
    "elab","aceq6b","52",1177
    "eqeq1","aceq6b","53",1178
    "fveq2","aceq6b","55",1179
    "eleq2","aceq6b","57",1180
    "rcla4v","aceq6b","60",1181
    "prel12","aceq6b","66",1182
    "eleq2","aceq6b","67",1183
    "eleq2","aceq6b","68",1184
    "eleq2","aceq6b","74",1185
    "preleq","aceq6b","85",1186
    "fveq2","aceq6b","87",1187
    "r19.23aiv","aceq6b","98",1188
    "df-reu","aceq6b","112",1189
    "r19.21ai","aceq6b","117",1190
    "hbco","ac6lem","135",1191
    "eqeq1","ac6","5",1192
    "sseli","kmlem1","13",1193
    "sseli","kmlem1","15",1194
    "r19.20i2","kmlem1","17",1195
    "r19.20i2","kmlem1","19",1196
    "eqeq1","kmlem1","20",1197
    "elrab","kmlem1","22",1198
    "eqeq1","kmlem1","26",1199
    "elrab","kmlem1","28",1200
    "r19.20i2","kmlem1","32",1201
    "raleq","kmlem1","37",1202
    "raleqd","kmlem1","38",1203
    "raleq","kmlem1","39",1204
    "ineq2","kmlem2","1",1205
    "eleq2","kmlem2","9",1206
    "elssuni","kmlem2","17",1207
    "sseld","kmlem2","18",1208
    "disjsn","kmlem2","20",1209
    "biraldva","kmlem2","31",1210
    "elun","kmlem2","36",1211
    "eleq1","kmlem2","47",1212
    "dfnul3","kmlem3","2",1213
    "df-rex","kmlem3","9",1214
    "eldif","kmlem3","10",1215
    "elsn","kmlem3","11",1216
    "eqcom","kmlem3","12",1217
    "elin","kmlem3","25",1218
    "eluni","kmlem3","34",1219
    "birabi","kmlem3","41",1220
    "eleq1","kmlem4","2",1221
    "eqeq2","kmlem4","3",1222
    "eleq2","kmlem4","6",1223
    "cla4v","kmlem4","9",1224
    "eldif","kmlem4","11",1225
    "eluni","kmlem4","13",1226
    "eldif","kmlem4","17",1227
    "elsn","kmlem4","18",1228
    "eqcom","kmlem4","19",1229
    "disj","kmlem4","43",1230
    "df-rex","kmlem6","3",1231
    "n0","kmlem6","5",1232
    "eqeq12","kmlem8","8",1233
    "difeq1","kmlem8","9",1234
    "sneq","kmlem8","10",1235
    "r19.23aivv","kmlem8","20",1236
    "eqeq1","kmlem8","23",1237
    "elab2","kmlem8","25",1238
    "eqeq1","kmlem8","27",1239
    "elab2","kmlem8","29",1240
    "difeq1","kmlem8","30",1241
    "sneq","kmlem8","31",1242
    "snssi","kmlem10","2",1243
    "elsn","kmlem10","14",1244
    "difeq1","kmlem10","26",1245
    "sneq","kmlem10","27",1246
    "iunxsn","kmlem10","33",1247
    "difeq1","kmlem11","2",1248
    "sneq","kmlem11","3",1249
    "difeq1","kmlem11","11",1250
    "sneq","kmlem11","12",1251
    "r19.20i","kmlem11","32",1252
    "eqeq1","kmlem11","40",1253
    "elab","kmlem11","42",1254
    "raleq","kmlem12","4",1255
    "raleqd","kmlem12","5",1256
    "raleq","kmlem12","6",1257
    "ineq2","kmlem12","11",1258
    "df-rex","kmlem13","2",1259
    "n0","kmlem13","7",1260
    "eqeq1","kmlem14","4",1261
    "ineq1","kmlem14","6",1262
    "raleqd","kmlem14","10",1263
    "df-rex","kmlem14","12",1264
    "eleq1","kmlem14","13",1265
    "df-ral","kmlem14","17",1266
    "eqeq2","kmlem14","21",1267
    "ineq2","kmlem14","23",1268
    "df-rex","kmlem14","27",1269
    "elin","kmlem14","34",1270
    "elin","kmlem15","6",1271
    "eleq1","kmlem15","8",1272
    "elin","kmlem15","10",1273
    "eqcom","kmlem15","12",1274
    "df-ral","kmlem15","21",1275
    "rneq","numth","5",1276
    "eqeqan12rd","numth","9",1277
    "funfvima2","zornlem2","13",1278
    "r2al","zornlem4","43",1279
    "onelon","zornlem5","19",1280
    "df-ral","zornlem5","27",1281
    "r19.23ad","zornlem5","30",1282
    "onelon","zornlem6","12",1283
    "onelon","zornlem6","13",1284
    "eqeq12","zornlem6","26",1285
    "fveq2","zornlem6","27",1286
    "ordtri3or","zornlem6","41",1287
    "imaeq2","zornlem6","57",1288
    "rcla4v","zornlem6","63",1289
    "imaeq2","zornlem6","65",1290
    "rcla4v","zornlem6","71",1291
    "df-rex","zornlem6","82",1292
    "df-rex","zornlem6","86",1293
    "imaeq2","zornlem7","10",1294
    "breq1","zornlem7","44",1295
    "breq2","zornlem7","61",1296
    "elrab","zornlem7","63",1297
    "breq1","zornlem7","68",1298
    "psseq1","zorn2lem","3",1299
    "psseq2","zorn2lem","4",1300
    "brab","zorn2lem","qed",1301
    "breq2","zorn","4",1302
    "breq1","zorn","6",1303
    "rneq","zorn","12",1304
    "rneq","zorn","17",1305
    "breq1","zorn","22",1306
    "eleq1","zorn","29",1307
    "breq2","zorn","30",1308
    "eqeqan12rd","zorn","40",1309
    "sspsstri","zorn2","8",1310
    "sspss","zorn2","19",1311
    "breq2","hta","36",1312
    "breq1","hta","47",1313
    "hbel","hta","70",1314
    "hbel","hta","79",1315
    "breq2","hta","82",1316
    "eqeq1","unxpdomlem","3",1317
    "ifeq2","unxpdomlem","5",1318
    "eqeq1","unxpdomlem","10",1319
    "ifeq2","unxpdomlem","12",1320
    "eqeq1","unxpdomlem","14",1321
    "rcla42ev","unxpdomlem","18",1322
    "eqid","unxpdomlem","20",1323
    "eqtr4d","unxpdomlem","25",1324
    "eqeq1","unxpdomlem","30",1325
    "ifeq2","unxpdomlem","32",1326
    "eqeq1","unxpdomlem","37",1327
    "ifeq2","unxpdomlem","39",1328
    "eqeq1","unxpdomlem","41",1329
    "rcla42ev","unxpdomlem","45",1330
    "eqeq1","unxpdomlem","56",1331
    "ifeq2","unxpdomlem","58",1332
    "eqeq1","unxpdomlem","63",1333
    "ifeq2","unxpdomlem","65",1334
    "eqeq1","unxpdomlem","67",1335
    "rcla42ev","unxpdomlem","71",1336
    "eqtrd","unxpdomlem","75",1337
    "eqeq1","unxpdomlem","82",1338
    "ifeq2","unxpdomlem","84",1339
    "eqeq1","unxpdomlem","89",1340
    "ifeq2","unxpdomlem","91",1341
    "eqeq1","unxpdomlem","93",1342
    "rcla42ev","unxpdomlem","97",1343
    "eqid","unxpdomlem","99",1344
    "breq1","iscard2","15",1345
    "elrab","iscard2","16",1346
    "onelon","ondomon","4",1347
    "onelsst","ondomon","5",1348
    "breq1","ondomon","16",1349
    "elrab","ondomon","17",1350
    "breq1","ondomon","18",1351
    "elrab","ondomon","19",1352
    "breq1","ondomcard","4",1353
    "elrab","ondomcard","5",1354
    "fveq2","carduni","2",1355
    "eqeq12d","carduni","4",1356
    "rcla4v","carduni","5",1357
    "fveq2","carduni","18",1358
    "eqeq12d","carduni","20",1359
    "rcla4v","carduni","21",1360
    "fveq2","carduni","50",1361
    "eqeq12d","carduni","52",1362
    "rcla4v","carduni","53",1363
    "eqeq1","cardiun","3",1364
    "elab","cardiun","5",1365
    "breq2","cardmin","10",1366
    "elrab","cardmin","11",1367
    "fveq2","alephon","3",1368
    "rdgsucopab","alephon","19",1369
    "rdgsucopabn","alephon","33",1370
    "fveq2","alephcard","5",1371
    "fveq2","alephcard","7",1372
    "eleq2","alephordi","5",1373
    "fveq2","alephordi","6",1374
    "fveq2","alephle","2",1375
    "sseq12d","alephle","3",1376
    "alephord2i","alephle","7",1377
    "onelon","alephle","9",1378
    "r19.20dva","alephle","15",1379
    "fveq2","cardaleph","47",1380
    "onnminsb","cardaleph","49",1381
    "fveq2","cardaleph","97",1382
    "onnminsb","cardaleph","99",1383
    "aleph11","alephiso","12",1384
    "alephord2","alephiso","23",1385
    "hbfv","alephfplem2","16",1386
    "frsucopab","alephfplem2","19",1387
    "fveq2","alephfplem3","5",1388
    "eluni","alephfp","10",1389
    "eleq2","alephfp","28",1390
    "fveq2","alephval2","26",1391
    "rcla4v","alephval2","28",1392
    "breq2","alephval2","92",1393
    "elrab","alephval2","94",1394
    "fveq2","alephval3","59",1395
    "eqeq12d","alephval3","61",1396
    "sseq2","alephval3","62",1397
    "eqeq1","alephval3","63",1398
    "elab","alephval3","67",1399
    "sseq2","cflem","3",1400
    "rcla4ev","cflem","4",1401
    "ssel","cfub","2",1402
    "onelsst","cfub","6",1403
    "eluni","cfub","11",1404
    "df-rex","cfub","12",1405
    "sucssel","cflim","7",1406
    "eluni2","cflim","10",1407
    "eqeq1","cardcf","10",1408
    "elab","cardcf","13",1409
    "eqeq1","cardcf","33",1410
    "elab","cardcf","36",1411
    "sseq2","cflecard","4",1412
    "rcla4ev","cflecard","5",1413
    "eqeq1","cfeq0","5",1414
    "elab","cfeq0","8",1415
    "en2lp","axunndlem1","2",1416
    "eleq2","axpowndlem3","19",1417
    "n0","axpowndlem3","28",1418
    "en2lp","axacndlem5","164",1419
    "vtoclf","zfcndrep","31",1420
    "eleq1","ltpiord","2",1421
    "ordtri2","ltsopi","1",1422
    "ltpiord","ltsopi","5",1423
    "ltpiord","ltsopi","6",1424
    "ontr1","ltsopi","14",1425
    "ltpiord","ltsopi","16",1426
    "ltpiord","ltsopi","18",1427
    "ltpiord","ltsopi","21",1428
    "eleq1","indpi","28",1429
    "breq2","indpi","29",1430
    "eqvinc","indpi","113",1431
    "gencl","indpi","115",1432
    "mulcanpi","enqer","10",1433
    "opreq12","addpipq","8",1434
    "opreq12","addpipq","9",1435
    "opreq12","addpipq","12",1436
    "opreq12","addpipq","13",1437
    "opreq12","addpipq","18",1438
    "opreq12","addpipq","19",1439
    "opreq12","addpipq","22",1440
    "opreq12","addpipq","27",1441
    "opreq12","addpipq","28",1442
    "opreq12","addpipq","31",1443
    "opreq12","mulpipq","8",1444
    "opreq12","mulpipq","9",1445
    "opreq12","mulpipq","12",1446
    "opreq12","mulpipq","13",1447
    "opreq12","mulpipq","18",1448
    "opreq12","mulpipq","19",1449
    "opreq12","mulpipq","23",1450
    "opreq12","mulpipq","24",1451
    "eqeq2","ltsopq","14",1452
    "eleq2","elnp","10",1453
    "rexeq","genpv","14",1454
    "rexeq","genpv","16",1455
    "oprabval2","genpv","19",1456
    "eqeq1","genpv","21",1457
    "eleq1","genpv","25",1458
    "eleq1","genpv","26",1459
    "opreq12","genpv","28",1460
    "sotrieq","distrlem4pr","73",1461
    "opreq1","distrlem4pr","78",1462
    "psslinpr","ltsopr","15",1463
    "opeq1","prlem934a","9",1464
    "eleq1","prlem934a","30",1465
    "opreq1","prlem934a","31",1466
    "opreq2","ltexprlem3","21",1467
    "elab2","ltexprlem3","25",1468
    "opreq2","ltexprlem4","68",1469
    "elab2","ltexprlem4","72",1470
    "opreq2","ltexpri","8",1471
    "opreq2","ltexpri","15",1472
    "opreq2","ltexpri","21",1473
    "eleq1","prlem936","84",1474
    "opreq1","prlem936","85",1475
    "cla4ev","prlem936","89",1476
    "breq1","reclem2pr","66",1477
    "elab2","reclem2pr","69",1478
    "breq1","reclem2pr","87",1479
    "elab2","reclem2pr","90",1480
    "breq1","recexpr","4",1481
    "breq1","recexpr","9",1482
    "n0","suplem1pr","3",1483
    "eluni","suplem1pr","14",1484
    "prcdpq","suplem1pr","45",1485
    "elunii","suplem1pr","51",1486
    "eluni","suplem1pr","56",1487
    "prnmax","suplem1pr","62",1488
    "elunii","suplem1pr","69",1489
    "eluni","suplem1pr","78",1490
    "sotric","suplem2pr","10",1491
    "sspss","suplem2pr","16",1492
    "eqcom","suplem2pr","17",1493
    "addcanpr","enrer","11",1494
    "opreq12","addsrpr","8",1495
    "opreq12","addsrpr","9",1496
    "opreq12","addsrpr","12",1497
    "opreq12","addsrpr","13",1498
    "opreq12","addsrpr","18",1499
    "opreq12","addsrpr","19",1500
    "opreq12","addsrpr","23",1501
    "opreq12","addsrpr","24",1502
    "opreq12","mulsrpr","8",1503
    "opreq12","mulsrpr","9",1504
    "opreq12","mulsrpr","12",1505
    "opreq12","mulsrpr","13",1506
    "opreq12","mulsrpr","18",1507
    "opreq12","mulsrpr","19",1508
    "opreq12","mulsrpr","22",1509
    "opreq12","mulsrpr","23",1510
    "opreq12","mulsrpr","28",1511
    "opreq12","mulsrpr","29",1512
    "opreq12","mulsrpr","32",1513
    "opreq12","mulsrpr","33",1514
    "eqeq2","ltsosr","14",1515
    "opreq1","suppsr","19",1516
    "elab2","suppsr","24",1517
    "opreq1","suppsr","47",1518
    "elab2","suppsr","52",1519
    "opreq1","suppsr","98",1520
    "elab2","suppsr","103",1521
    "eleq1","suppsr2","4",1522
    "breq2","suppsr2","5",1523
    "eleq1","suppsr2","8",1524
    "eleq1","suppsr2","9",1525
    "breq1","suppsr2","10",1526
    "opreq1","suppsr2","48",1527
    "eleq1","suppsr2","64",1528
    "breq2","suppsr2","65",1529
    "eleq1","suppsr2","75",1530
    "breq2","suppsr2","76",1531
    "eleq1","suppsr3","3",1532
    "breq2","suppsr3","4",1533
    "elab2","suppsr3","6",1534
    "sotric","suppsr3","45",1535
    "breq2","suppsr3","53",1536
    "eleq1","suppsr3","104",1537
    "breq2","suppsr3","105",1538
    "elab2","suppsr3","107",1539
    "opreq1","supsrlem4","7",1540
    "eleq1","supsrlem6","3",1541
    "breq2","supsrlem6","4",1542
    "opreq1","supsr","6",1543
    "opeq1","supre","15",1544
    "elab2","supre","17",1545
    "opeq1","supre","38",1546
    "elab2","supre","40",1547
    "opeq1","supre","76",1548
    "elab2","supre","78",1549
    "eqeq2","ltsor","16",1550
    "sotric","ltsor","32",1551
    "eqresr","ltsor","38",1552
    "opeq1","axsup","29",1553
    "opreq2","negeu","3",1554
    "addcant","negeu","32",1555
    "opreq2","receu","4",1556
    "mulcant2","receu","33",1557
    "axlttri","ltso","1",1558
    "eleq2","peano5nn","3",1559
    "eleq1","peano2nn","3",1560
    "opreq1","peano2nn","4",1561
    "elintab","peano2nn","12",1562
    "eleq1","nnind","23",1563
    "elab","nnind","25",1564
    "dfsbcq","nn1suc","6",1565
    "dfsbcq","nn1suc","8",1566
    "dfsbcq","nn1suc","9",1567
    "opreq2","nnaddclt","4",1568
    "opreq2","nnmulclt","4",1569
    "breq2","nnge1t","2",1570
    "eqeq2","nnleltp1t","37",1571
    "opreq1","nnleltp1t","41",1572
    "breq2","nnleltp1t","43",1573
    "eqeq2","nnleltp1t","44",1574
    "eqeq2","nnleltp1t","51",1575
    "eqeq2","nnleltp1t","58",1576
    "breq1","nnleltp1t","72",1577
    "breq1","nnleltp1t","73",1578
    "eqeq1","nnleltp1t","74",1579
    "nn1suc","nnleltp1t","97",1580
    "breq1","nnleltp1t","111",1581
    "breq1","nnleltp1t","112",1582
    "eqeq1","nnleltp1t","113",1583
    "breq1","nnleltp1t","134",1584
    "breq1","nnleltp1t","135",1585
    "eqeq1","nnleltp1t","136",1586
    "rcla4v","nnleltp1t","139",1587
    "addcant","nnleltp1t","168",1588
    "nn1suc","nnleltp1t","180",1589
    "breq1","nnleltp1t","184",1590
    "breq1","nnleltp1t","185",1591
    "eqeq1","nnleltp1t","186",1592
    "breq2","nnsub","7",1593
    "opreq1","nnsub","8",1594
    "breq1","sup2","21",1595
    "eleq1","sup2","46",1596
    "breq2","sup2","47",1597
    "leloet","sup3","5",1598
    "axlttri","arch","6",1599
    "eqcom","arch","9",1600
    "eleq1","uzind","60",1601
    "eqeq12","uzind","78",1602
    "opreq1","uzind","79",1603
    "breq2","uzind3","7",1604
    "elrab","uzind3","8",1605
    "breq1","uzwo","4",1606
    "breq1","uzwo","10",1607
    "breq2","uzwo","14",1608
    "elrab","uzwo","15",1609
    "breq1","uzwo","22",1610
    "rcla4ev","uzwo","24",1611
    "letri3t","uzwo","28",1612
    "eleq1a","uzwo","48",1613
    "uzind3","uzwo","71",1614
    "breq1","uzwo","72",1615
    "rcla4ev","uzwo","74",1616
    "breq2","uzwo2","7",1617
    "rcla4v","uzwo2","8",1618
    "breq2","uzwo2","9",1619
    "rcla4v","uzwo2","10",1620
    "letri3t","uzwo2","17",1621
    "breq1","uzwo2","28",1622
    "breq1","nnwoOLD","4",1623
    "breq1","nnwoOLD","10",1624
    "breq1","nnwoOLD","18",1625
    "rcla4ev","nnwoOLD","20",1626
    "letri3t","nnwoOLD","24",1627
    "eleq1a","nnwoOLD","44",1628
    "nnind","nnwoOLD","61",1629
    "breq1","nnwoOLD","62",1630
    "rcla4ev","nnwoOLD","64",1631
    "hbel","nnwof","5",1632
    "eleq1","nnwof","9",1633
    "breq2","nnwof","10",1634
    "hbel","nnwof","16",1635
    "hbel","nnwof","18",1636
    "eleq1","nnwof","24",1637
    "breq1","nnwof","25",1638
    "elrab","nnwos","13",1639
    "dfsbcq","nn0indALT","8",1640
    "vsbcint","nn0indALT","9",1641
    "eqeq2","nn0indALT","25",1642
    "breq2","uzwo3lem2","4",1643
    "rcla4v","uzwo3lem2","5",1644
    "breq1","uzwo3lem2","7",1645
    "breq2","uzwo3lem2","9",1646
    "breq2","uzwo3lem2","21",1647
    "elrab","uzwo3lem2","22",1648
    "breq2","uzwo3lem2","29",1649
    "breq2","uzwo3lem2","39",1650
    "breq2","uzwo3","4",1651
    "breq1","uzwo3","7",1652
    "breq2","zmin","3",1653
    "elrab","zmin","4",1654
    "breq2","zmin","5",1655
    "elrab","zmin","6",1656
    "breq2","uzinfm","10",1657
    "elrab","uzinfm","11",1658
    "breq2","uzinfm","44",1659
    "elrab","uzinfm","45",1660
    "breq1","flleltt","2",1661
    "opreq1","flleltt","3",1662
    "breq1","flval3t","24",1663
    "elrab","flval3t","25",1664
    "breq1","flval3t","60",1665
    "elrab","flval3t","61",1666
    "breq1","flval3t","81",1667
    "elrab","flval3t","82",1668
    "breq1","flval3t","115",1669
    "elrab","flval3t","116",1670
    "opreq2","qnegclt","17",1671
    "rcla42ev","qnegclt","19",1672
    "breq2","monoord","8",1673
    "fveq2","monoord","9",1674
    "fveq2","monoord","54",1675
    "opreq1","monoord","55",1676
    "vtoclga","monoord","58",1677
    "hbfv","om2uzsuc","17",1678
    "frsucopab","om2uzsuc","30",1679
    "fveq2","om2uzuz","5",1680
    "eleq2","om2uzlt","8",1681
    "fveq2","om2uzlt","9",1682
    "breq2","om2uzran","15",1683
    "elrab","om2uzran","16",1684
    "eleq1","om2uzran","18",1685
    "eleq1","om2uzran","20",1686
    "uzind","om2uzran","53",1687
    "ordtri3","om2uzf1o","28",1688
    "om2uzlt","om2uzf1o","33",1689
    "om2uzlt","om2uzf1o","34",1690
    "fveq2","seqlem1","6",1691
    "eqeq12d","seqlem1","9",1692
    "fveq2","seqlem1","39",1693
    "dfsbcq","seqlem1","53",1694
    "fveq2","seqsuclem","11",1695
    "fveq2","seqsuclem","13",1696
    "fveq2","seqsuclem","14",1697
    "eqeq1","seqsuclem","20",1698
    "fveq2","seqrn","6",1699
    "fveq2","seqrn","12",1700
    "nnind","seqrn","49",1701
    "fveq2","serrecl","4",1702
    "fveq2","sermono","13",1703
    "vtoclga","sermono","15",1704
    "fveq2","sermconst","9",1705
    "fveq2","sermconst","10",1706
    "opreq2","1expt","3",1707
    "opreq2","expcllem","6",1708
    "opreq2","expeq0t","5",1709
    "opreq2","expgt0t","4",1710
    "opreq2","expgt1t","4",1711
    "opreq2","mulexpt","7",1712
    "opreq2","mulexpt","8",1713
    "opreq2","mulexpt","9",1714
    "opreq2","recexpt","6",1715
    "opreq2","recexpt","7",1716
    "opreq2","expaddt","7",1717
    "opreq2","expaddt","9",1718
    "opreq2","bernneq","6",1719
    "opreq2","bernneq","8",1720
    "opreq1","nneo","101",1721
    "opreq1","nneo","104",1722
    "breq2","sqrval","9",1723
    "elrab","sqrval","10",1724
    "breq2","sqrlem24","3",1725
    "opreq12","sqrlem24","4",1726
    "breq2","sqrgt0i","3",1727
    "opreq12","sqrgt0i","4",1728
    "breq2","sqrlem26","3",1729
    "opreq12","sqrlem26","4",1730
    "opreq1","sqr2irrlem3","1",1731
    "opreq1","sqr2irrlem3","5",1732
    "breq1","sqr2irrlem3","11",1733
    "opreq1","sqr2irrlem3","12",1734
    "rcla4v","sqr2irrlem3","17",1735
    "crut","creur","2",1736
    "opreq1","creur","21",1737
    "opreq1","creur","24",1738
    "crut","creui","4",1739
    "opreq1","creui","23",1740
    "opreq1","creui","27",1741
    "opreq2","absexpt","6",1742
    "opreq2","absexpt","8",1743
    "breq2","seqbnd","6",1744
    "breq2","seqbnd","151",1745
    "breq1","sequblem","28",1746
    "fveq2","sequblem","29",1747
    "rcla4v","sequblem","33",1748
    "breq1","sequblem","54",1749
    "elrab","sequblem","55",1750
    "breq1","sequblem","67",1751
    "elrab","sequblem","68",1752
    "breq1","sequb","5",1753
    "breq1","sequb","13",1754
    "fveq2","cau2","4",1755
    "leloet","cau2","22",1756
    "breq1","cvg1","13",1757
    "fveq2","caure","5",1758
    "fveq2","caure","6",1759
    "vtoclga","caure","9",1760
    "fveq2","caure","10",1761
    "fveq2","caure","11",1762
    "vtoclga","caure","14",1763
    "fveq2","cauim","5",1764
    "fveq2","cauim","6",1765
    "vtoclga","cauim","9",1766
    "fveq2","cauim","10",1767
    "fveq2","cauim","11",1768
    "vtoclga","cauim","14",1769
    "opreq2","serabsdiflem","13",1770
    "opreq2","serabsdiflem","17",1771
    "fveq2","sercj","8",1772
    "fveq2","sercj","9",1773
    "fveq2","facclt","3",1774
    "opreq2","faclbnd","5",1775
    "fveq2","faclbnd","7",1776
    "breq2","facdivt","7",1777
    "fveq2","facdivt","8",1778
    "climuni","climmo","3",1779
    "breq2","climmo","5",1780
    "breq2","climshift","96",1781
    "fveq2","climshift","97",1782
    "opreq1","climshift","98",1783
    "rcla4v","climshift","102",1784
    "fveq2","climre","8",1785
    "fveq2","climre","9",1786
    "vtoclga","climre","12",1787
    "fveq2","climre","35",1788
    "fveq2","climre","36",1789
    "vtoclga","climre","39",1790
    "fveq2","climre","55",1791
    "fveq2","climre","56",1792
    "vtoclga","climre","59",1793
    "breq2","climrecl","76",1794
    "fveq2","climrecl","77",1795
    "rcla4ev","climrecl","83",1796
    "breq2","climadd","100",1797
    "fveq2","climadd","101",1798
    "rcla4v","climadd","107",1799
    "fveq2","climadd","173",1800
    "fveq2","climadd","174",1801
    "fveq2","climadd","175",1802
    "vtoclga","climadd","178",1803
    "fveq2","climadd","214",1804
    "fveq2","climadd","215",1805
    "fveq2","climadd","216",1806
    "vtoclga","climadd","219",1807
    "eleq1","climaconstOLD","8",1808
    "fveq2","climaconstOLD","9",1809
    "fveq2","climaconstOLD","10",1810
    "eleq1","climmconst","6",1811
    "fveq2","climmconst","7",1812
    "fveq2","climmconst","8",1813
    "eleq1","climmconst","29",1814
    "fveq2","climmconst","30",1815
    "fveq2","climmconst","31",1816
    "eleq1","climmconst","100",1817
    "fveq2","climmconst","101",1818
    "fveq2","climmconst","102",1819
    "eleq1","climmconst","153",1820
    "fveq2","climmconst","154",1821
    "fveq2","climmconst","155",1822
    "breq2","climcau","27",1823
    "fveq2","climcau","28",1824
    "rcla4v","climcau","33",1825
    "breq2","climcau","49",1826
    "fveq2","climcau","50",1827
    "rcla4v","climcau","55",1828
    "breq2","caucvglem2","42",1829
    "fveq2","caucvglem2","43",1830
    "rcla4v","caucvglem2","46",1831
    "fveq2","caucvglem2","49",1832
    "rcla4v","caucvglem2","52",1833
    "breq2","caucvg","170",1834
    "fveq2","caucvg","171",1835
    "rcla4v","caucvg","176",1836
    "fveq2","ser0","3",1837
    "fveq2","sertrunclem","11",1838
    "breq1","sertrunclem","12",1839
    "opreq1","sertrunclem","14",1840
    "breq1","sertrunc2","18",1841
    "fvopab4","sertrunc2","25",1842
    "fveq2","sercmp","7",1843
    "fveq2","sercmp","8",1844
    "fveq2","sercmp2","11",1845
    "fveq2","sercmp2","12",1846
    "fveq2","cvgcmp2lem","73",1847
    "fveq2","cvgcmp2lem","74",1848
    "vtoclga","cvgcmp2lem","77",1849
    "fveq2","cvgcmp2","13",1850
    "fvopab4","cvgcmp2","17",1851
    "fveq2","cvgcmp2c","14",1852
    "fvopab4","cvgcmp2c","18",1853
    "fveq2","cvgcmp3ce","13",1854
    "fvopab4","cvgcmp3ce","17",1855
    "fveq2","cvgcmp3ce","21",1856
    "fvopab4","cvgcmp3ce","25",1857
    "fveq2","cvgcmp3ce","30",1858
    "fvopab4","cvgcmp3ce","34",1859
    "fveq2","cvgcmp3ce","39",1860
    "fvopab4","cvgcmp3ce","43",1861
    "fveq2","cvgcmp3cetlem1","10",1862
    "vtoclga","cvgcmp3cetlem1","12",1863
    "breq2","cvgcmp3cetlem1","21",1864
    "fveq2","cvgcmp3cetlem1","22",1865
    "fveq2","cvgcmp3cetlem1","24",1866
    "breq2","cvgcmp3cetlem1","100",1867
    "fveq2","cvgcmp3cetlem1","101",1868
    "fveq2","cvgcmp3cetlem1","103",1869
    "breq2","cvgcmp3cetlem1","179",1870
    "fveq2","cvgcmp3cetlem1","180",1871
    "fveq2","cvgcmp3cetlem1","182",1872
    "breq2","cvgcmp3cetlem1","258",1873
    "fveq2","cvgcmp3cetlem1","259",1874
    "fveq2","cvgcmp3cetlem1","261",1875
    "fveq2","cvgcmp3cetlem2","23",1876
    "fveq2","cvgcmp3cetlem2","72",1877
    "fveq2","cvgcmp3cetlem2","122",1878
    "breq2","cvgcmp3cetlem2","165",1879
    "fveq2","cvgcmp3cetlem2","166",1880
    "fveq2","cvgcmp3cetlem2","168",1881
    "opreq2","expcnv","10",1882
    "fvopab4","expcnv","12",1883
    "opreq2","expcnv","31",1884
    "fvopab4","expcnv","33",1885
    "fveq2","geoser","44",1886
    "opreq1","geoser","46",1887
    "opreq2","geolimilem","264",1888
    "fvopab4","geolimilem","266",1889
    "opreq2","geolimi","7",1890
    "fvopab4","geolimi","11",1891
    "opreq2","geolimi","12",1892
    "fvopab4","geolimi","14",1893
    "opreq2","cvgratlem1","8",1894
    "opreq2","cvgratlem1","10",1895
    "fveq2","cvgratlem3","32",1896
    "fvopab4","cvgratlem3","35",1897
    "opreq2","cvgratlem5","23",1898
    "fvopab4","cvgratlem5","25",1899
    "opreq2","cvgratlem5","81",1900
    "fvopab4","cvgratlem5","83",1901
    "climuni","sumclt","9",1902
    "eleq1","sumclt","15",1903
    "breq2","sumclt","16",1904
    "opreq2","efcltlem1","346",1905
    "fveq2","efcltlem1","347",1906
    "fvopab4","efcltlem1","350",1907
    "opreq2","erelem2","89",1908
    "fvopab4","erelem2","92",1909
    "opreq2","erelem2","93",1910
    "fvopab4","erelem2","96",1911
    "fveq2","erelem3","31",1912
    "fvopab4","erelem3","34",1913
    "fveq2","erelem3","127",1914
    "fvopab4","erelem3","130",1915
    "opreq2","erelem3","131",1916
    "fvopab4","erelem3","134",1917
    "eleq1","ruclem12","2",1918
    "eleq1","ruclem12","4",1919
    "ruclem4","ruclem12","7",1920
    "eqeq1","ruclem12","11",1921
    "eqid","ruclem15","23",1922
    "ruclem4","ruclem15","24",1923
    "fveq2","ruclem25","10",1924
    "fveq2","ruclem25","11",1925
    "opreq2","ruclem32","11",1926
    "opreq1","ruclem32","50",1927
    "nn0opth2t","xpnnen","60",1928
    "eqeq12","xpnnen","69",1929
    "opth","xpnnen","73",1930
    "ltnet","znnenlem","14",1931
    "mulcant2","znnen","66",1932
    "mulcant2","znnen","114",1933
    "om2uzlt2","unbenlem","34",1934
    "breq2","infpnlem2","46",1935
    "opreq2","infpnlem2","47",1936
    "infpnlem1","infpnlem2","52",1937
    "breq2","infpn","22",1938
    "opreq1","infpn","23",1939
    "eqeq2","infpn","25",1940
    "elrab","infpn","30",1941
    "breq2","infxpidmlem2","9",1942
    "sseq1","infxpidmlem2","10",1943
    "xpeq1","infxpidmlem2","12",1944
    "xpeq2","infxpidmlem2","13",1945
    "f1oeq3","infxpidmlem2","17",1946
    "sseq1","infxpidmlem7","55",1947
    "sseq2","infxpidmlem7","56",1948
    "sseq2","infxpidmlem7","58",1949
    "sseq1","infxpidmlem7","59",1950
    "rcla42v","infxpidmlem7","61",1951
    "psseq2","infxpidmlem10","7",1952
    "rcla4v","infxpidmlem10","9",1953
    "sseq1","infmap2lem1","8",1954
    "breq1","infmap2lem1","9",1955
    "foeq3","infmap2lem1","11",1956
    "opelopab","infmap2lem1","15",1957
    "sseq1","infmap2lem1","41",1958
    "breq1","infmap2lem1","42",1959
    "eqeqan12d","infmap2lem2","55",1960
    "fveq2","infmap2lem2","58",1961
    "eleq2","closedsub","7",1962
    "breq2","hlimcaui","72",1963
    "fveq2","hlimcaui","73",1964
    "hlimuni","hlimreu","4",1965
    "breq2","hlimreu","8",1966
    "hlimuni","hlimeu","4",1967
    "breq2","hlimeu","7",1968
    "df-rex","chsscm","13",1969
    "closedsub","chsscm","23",1970
    "df-rex","chcmh","19",1971
    "closedsub","chcmh","35",1972
    "eleq1","ch2","10",1973
    "feq3","ch2","11",1974
    "rexeq","ch2","12",1975
    "opreq2","ocin","2",1976
    "rcla4v","ocin","4",1977
    "fveq2","occllem5","2",1978
    "rcla4v","occllem5","5",1979
    "eqeq1","projlem8","28",1980
    "elrab","projlem8","30",1981
    "opreq1","projlem10","16",1982
    "rcla4ev","projlem10","20",1983
    "eqeq1","projlem13","14",1984
    "elrab","projlem13","16",1985
    "eqeq1","projlem15","55",1986
    "opreq1","projlem15","57",1987
    "elrab","projlem15","63",1988
    "opreq2","projlem26","99",1989
    "fveq2","projlem26","101",1990
    "fveq2","projlem26","105",1991
    "opreq2","projlem26","108",1992
    "rcla4v","projlem26","112",1993
    "opreq2","projlem26","153",1994
    "fveq2","projlem26","155",1995
    "fveq2","projlem26","159",1996
    "opreq2","projlem26","162",1997
    "rcla4v","projlem26","166",1998
    "chocuni","pjthu","4",1999
    "opreq2","pjthu","12",2000
    "opreq1","pjthu","25",2001
    "chocuni","pjthu2","6",2002
    "opreq1","pjthu2","14",2003
    "opreq2","pjthu2","27",2004
    "eleq2","pjmvalt","1",2005
    "df-rab","pjmvalt","7",2006
    "elinti","shintcl","23",2007
    "elinti","shintcl","25",2008
    "shaddclt","shintcl","30",2009
    "elinti","shintcl","39",2010
    "shmulclt","shintcl","44",2011
    "chlim","chintcl","12",2012
    "elint2","chintcl","21",2013
    "opreq1","shunss","3",2014
    "rcla42ev","shunss","7",2015
    "opreq2","shunss","18",2016
    "rcla42ev","shunss","20",2017
    "elspan","spanun","40",2018
    "elspan","spanun","43",2019
    "shaddclt","spanun","52",2020
    "eleq1","spanun","54",2021
    "elspan","spanun","62",2022
    "eleq1a","spansn","8",2023
    "elspan","spansn","24",2024
    "feq1","hosmvalt","19",2025
    "elab","hosmvalt","20",2026
    "feq1","hosmvalt","22",2027
    "elab","hosmvalt","23",2028
    "feq1","hodmvalt","19",2029
    "elab","hodmvalt","20",2030
    "feq1","hodmvalt","22",2031
    "elab","hodmvalt","23",2032
    "eqeq2d","spansncv","53",2033
    "eleq1a","spansncv","54",2034
    "fveq2","pjjs","3",2035
    "rcla4v","pjjs","5",2036
    "eleq1","pjrn","8",2037
    "fveq2","pjrn","9",2038
    "cla4ev","pjrn","12",2039
    "fveq2","hun","3",2040
    "opreq1","hun","5",2041
    "fveq2","hun","7",2042
    "opreq2","hun","9",2043
    "hvsubeq0t","hun1o","48",2044
    "sseq1","mdbr3","26",2045
    "opreq1","mdbr3","27",2046
    "opreq1","mdbr3","29",2047
    "sseq1","mdbr4","26",2048
    "opreq1","mdbr4","27",2049
    "opreq1","mdbr4","29",2050
    "sseq2","dmdbr3","29",2051
    "ineq1","dmdbr3","30",2052
    "ineq1","dmdbr3","32",2053
    "sseq2","dmdbr4","29",2054
    "ineq1","dmdbr4","30",2055
    "ineq1","dmdbr4","31",2056
    "breq2","mddmd","20",2057
    "sseq1","hatomistic","10",2058
    "elrab","hatomistic","11",2059
    "sseq1","hatomistic","12",2060
    "elrab","hatomistic","13",2061
    "sseq1","hatomistic","26",2062
    "elrab","hatomistic","27",2063
    "opreq1","mdsymlem2","4",2064
    "sseq1","mdsymlem2","6",2065
    "rcla4ev","mdsymlem2","9",2066
    "atnem0","mdsymlem3","33",2067
    "sseq1","mdsymlem3","35",2068
    "atnem0","mdsymlem5","4",2069
    "sseq1","mdsymlem6","5",2070
    "shsubclt","sumdmdi","6",2071
    "ssel2","sumdmdi","9",2072
    "chelt","sumdmdi","24",2073
    "eleq1","sumdmdi","30",2074
    "elin","sumdmdi","41",2075
    "elin","sumdmdi","64",2076
    "eqeq2d","sumdmdlem","41",2077
    "eleq1","sumdmdlem","47",2078