generated from pitmonticone/LeanProject
-
Notifications
You must be signed in to change notification settings - Fork 66
/
unknowns_10_06.txt
440 lines (440 loc) · 12.4 KB
/
unknowns_10_06.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
Equation63 => Equation1692
Equation65 => Equation359
Equation65 => Equation614
Equation65 => Equation817
Equation65 => Equation1426
Equation65 => Equation1491
Equation65 => Equation3862
Equation65 => Equation4065
Equation73 => Equation99
Equation73 => Equation125
Equation73 => Equation203
Equation73 => Equation229
Equation73 => Equation255
Equation73 => Equation4380
Equation73 => Equation4435
Equation115 => Equation4273
Equation118 => Equation222
Equation118 => Equation274
Equation118 => Equation4435
Equation124 => Equation1924
Equation229 => Equation4435
Equation274 => Equation4380
Equation274 => Equation4435
Equation467 => Equation2847
Equation476 => Equation359
Equation476 => Equation3862
Equation476 => Equation4065
Equation477 => Equation1426
Equation477 => Equation1519 (*)
Equation477 => Equation2035
Equation477 => Equation2128 (*)
Equation477 => Equation3050
Equation477 => Equation3150 (*)
Equation481 => Equation1488 (*)
Equation481 => Equation1492
Equation481 => Equation2035
Equation481 => Equation2038
Equation481 => Equation2041
Equation481 => Equation2124 (*)
Equation481 => Equation2128
Equation481 => Equation2132 (*)
Equation481 => Equation2135
Equation481 => Equation3050
Equation481 => Equation3056
Equation481 => Equation3139 (*)
Equation481 => Equation3150
Equation481 => Equation3161 (*)
Equation503 => Equation359
Equation503 => Equation3862
Equation503 => Equation4065
Equation504 => Equation817
Equation504 => Equation1629
Equation504 => Equation1832
Equation504 => Equation1925 (*)
Equation511 => Equation614
Equation511 => Equation714
Equation511 => Equation1020
Equation511 => Equation1120
Equation511 => Equation1223
Equation511 => Equation2238
Equation511 => Equation2338
Equation511 => Equation2441
Equation511 => Equation2847
Equation511 => Equation3050
Equation511 => Equation4380
Equation511 => Equation4435
Equation677 => Equation255
Equation680 => Equation1629
Equation680 => Equation1832
Equation680 => Equation2847
Equation680 => Equation2947 (*)
Equation707 => Equation1223
Equation707 => Equation1316
Equation707 => Equation2238
Equation707 => Equation2331
Equation707 => Equation2847
Equation707 => Equation2940
Equation713 => Equation359
Equation713 => Equation817
Equation713 => Equation1426
Equation713 => Equation3862
Equation713 => Equation4065
Equation854 => Equation104
Equation854 => Equation107
Equation854 => Equation413
Equation854 => Equation429
Equation854 => Equation1038
Equation854 => Equation1041
Equation854 => Equation1045
Equation854 => Equation1055
Equation854 => Equation1238
Equation854 => Equation1248
Equation854 => Equation1251
Equation854 => Equation1850
Equation854 => Equation3316
Equation854 => Equation3925
Equation879 => Equation4065
Equation883 => Equation2035
Equation883 => Equation2101
Equation883 => Equation2238
Equation883 => Equation2304
Equation906 => Equation3862
Equation917 => Equation1629
Equation917 => Equation1729
Equation917 => Equation2441
Equation917 => Equation2541
Equation1076 => Equation3
Equation1076 => Equation8
Equation1076 => Equation23
Equation1076 => Equation47
Equation1076 => Equation99
Equation1076 => Equation151
Equation1076 => Equation203
Equation1076 => Equation255
Equation1076 => Equation307
Equation1076 => Equation326
Equation1076 => Equation359
Equation1076 => Equation375
Equation1076 => Equation411
Equation1076 => Equation614
Equation1076 => Equation817
Equation1076 => Equation1223
Equation1076 => Equation1426
Equation1076 => Equation1629
Equation1076 => Equation1832
Equation1076 => Equation2035
Equation1076 => Equation2238
Equation1076 => Equation2294
Equation1076 => Equation2441
Equation1076 => Equation2644
Equation1076 => Equation2847
Equation1076 => Equation3050
Equation1076 => Equation3253
Equation1076 => Equation3319
Equation1076 => Equation3456
Equation1076 => Equation3522
Equation1076 => Equation3659
Equation1076 => Equation3715
Equation1076 => Equation3722
Equation1076 => Equation3862
Equation1076 => Equation3915
Equation1076 => Equation4065
Equation1076 => Equation4118
Equation1076 => Equation4380
Equation1076 => Equation4435
Equation1076 => Equation4470
Equation1086 => Equation1832
Equation1086 => Equation2644
Equation1086 => Equation2710 (*)
Equation1110 => Equation8
Equation1110 => Equation411
Equation1110 => Equation1629
Equation1110 => Equation1832
Equation1110 => Equation3253
Equation1110 => Equation3319
Equation1110 => Equation3862
Equation1110 => Equation3915
Equation1112 => Equation8
Equation1112 => Equation411
Equation1112 => Equation1629
Equation1112 => Equation1832
Equation1112 => Equation3253
Equation1112 => Equation3319
Equation1112 => Equation3862
Equation1112 => Equation3915
Equation1113 => Equation2441
Equation1113 => Equation2534
Equation1117 => Equation2441
Equation1117 => Equation2444
Equation1117 => Equation2530
Equation1117 => Equation2534
Equation1117 => Equation2538
Equation1133 => Equation1035
Equation1133 => Equation1055
Equation1133 => Equation1085
Equation1133 => Equation1096
Equation1133 => Equation1167
Equation1133 => Equation1634
Equation1133 => Equation1657
Equation1133 => Equation1668
Equation1133 => Equation1681
Equation1133 => Equation1701
Equation1133 => Equation1721
Equation1133 => Equation1860
Equation1133 => Equation1884
Equation1133 => Equation1958
Equation1133 => Equation3877
Equation1133 => Equation3897
Equation1133 => Equation3952
Equation1133 => Equation3972
Equation1133 => Equation3989
Equation1133 => Equation4006
Equation1133 => Equation4040
Equation1133 => Equation4587
Equation1133 => Equation4606
Equation1133 => Equation4615
Equation1167 => Equation1025
Equation1167 => Equation1055
Equation1167 => Equation1096
Equation1167 => Equation1112
Equation1167 => Equation1133
Equation1167 => Equation1634
Equation1167 => Equation1657
Equation1167 => Equation1668
Equation1167 => Equation1681
Equation1167 => Equation1701
Equation1167 => Equation1721
Equation1167 => Equation1847
Equation1167 => Equation1897
Equation1167 => Equation1958
Equation1167 => Equation3867
Equation1167 => Equation3897
Equation1167 => Equation3925
Equation1167 => Equation3935
Equation1167 => Equation3972
Equation1167 => Equation4006
Equation1167 => Equation4040
Equation1167 => Equation4587
Equation1167 => Equation4606
Equation1167 => Equation4615
Equation1276 => Equation4273
Equation1289 => Equation2507
Equation1289 => Equation2913
Equation1289 => Equation3116
Equation1289 => Equation4435
Equation1323 => Equation2744
Equation1431 => Equation1428
Equation1431 => Equation4269
Equation1437 => Equation4269
Equation1441 => Equation4065
Equation1441 => Equation4067
Equation1443 => Equation23
Equation1443 => Equation1629
Equation1443 => Equation1630
Equation1443 => Equation2441
Equation1443 => Equation3050
Equation1443 => Equation3055 (*)
Equation1443 => Equation3522
Equation1443 => Equation4065
Equation1443 => Equation4067
Equation1443 => Equation4118
Equation1443 => Equation4268
Equation1447 => Equation1431
Equation1447 => Equation4269
Equation1485 => Equation151
Equation1485 => Equation152
Equation1485 => Equation166
Equation1485 => Equation1427
Equation1485 => Equation1429
Equation1485 => Equation1481
Equation1485 => Equation1483
Equation1485 => Equation2051
Equation1485 => Equation2087
Equation1485 => Equation2124
Equation1485 => Equation3456
Equation1485 => Equation3457
Equation1485 => Equation3511
Equation1485 => Equation3862
Equation1485 => Equation3877
Equation1485 => Equation3955
Equation1486 => Equation151
Equation1486 => Equation152
Equation1486 => Equation166
Equation1486 => Equation1427
Equation1486 => Equation1428
Equation1486 => Equation1479
Equation1486 => Equation1481
Equation1486 => Equation1483
Equation1486 => Equation1484
Equation1486 => Equation1485
Equation1486 => Equation2035
Equation1486 => Equation2036
Equation1486 => Equation2050
Equation1486 => Equation2051
Equation1486 => Equation2052
Equation1486 => Equation2087
Equation1486 => Equation2088
Equation1486 => Equation2089 (*)
Equation1486 => Equation2124
Equation1486 => Equation2125
Equation1486 => Equation2126 (*)
Equation1486 => Equation2162
Equation1486 => Equation2163
Equation1486 => Equation3456
Equation1486 => Equation3457
Equation1486 => Equation3511
Equation1486 => Equation3512
Equation1486 => Equation3513
Equation1486 => Equation3862
Equation1486 => Equation3877
Equation1486 => Equation3918
Equation1486 => Equation3955
Equation1486 => Equation3993
Equation1491 => Equation65
Equation1515 => Equation4590
Equation1516 => Equation255
Equation1516 => Equation1489
Equation1518 => Equation47
Equation1518 => Equation614
Equation1518 => Equation817
Equation1518 => Equation3862
Equation1519 => Equation2035
Equation1519 => Equation2128 (*)
Equation1523 => Equation2035
Equation1523 => Equation2038
Equation1523 => Equation2124 (*)
Equation1523 => Equation2128
Equation1523 => Equation2132 (*)
Equation1526 => Equation1223
Equation1526 => Equation1323
Equation1526 => Equation2744
Equation1630 => Equation4268
Equation1633 => Equation4268
Equation1648 => Equation23
Equation1648 => Equation151
Equation1648 => Equation203
Equation1648 => Equation206
Equation1648 => Equation307
Equation1648 => Equation1426
Equation1648 => Equation1832
Equation1648 => Equation2238
Equation1648 => Equation2441
Equation1648 => Equation3050
Equation1648 => Equation3253
Equation1648 => Equation3456
Equation1648 => Equation3522
Equation1648 => Equation4065
Equation1648 => Equation4118
Equation1659 => Equation1631
Equation1659 => Equation1633
Equation1659 => Equation1655
Equation1659 => Equation1656
Equation1659 => Equation1660
Equation1659 => Equation1661
Equation1659 => Equation1833
Equation1659 => Equation1837
Equation1659 => Equation1839
Equation1659 => Equation1851
Equation1659 => Equation1860
Equation1659 => Equation2446
Equation1659 => Equation2452
Equation1659 => Equation2460
Equation1659 => Equation3458
Equation1659 => Equation3460
Equation1659 => Equation3519
Equation1659 => Equation3520
Equation1659 => Equation3524
Equation1659 => Equation3525
Equation1659 => Equation3527
Equation1659 => Equation4268
Equation1659 => Equation4314
Equation1659 => Equation4315
Equation1661 => Equation1630
Equation1661 => Equation1633
Equation1661 => Equation1656
Equation1661 => Equation1657
Equation1661 => Equation1659
Equation1661 => Equation1660
Equation1661 => Equation1833
Equation1661 => Equation1837
Equation1661 => Equation1839
Equation1661 => Equation1851
Equation1661 => Equation1860
Equation1661 => Equation2443
Equation1661 => Equation2452
Equation1661 => Equation2467
Equation1661 => Equation3457
Equation1661 => Equation3460
Equation1661 => Equation3520
Equation1661 => Equation3521
Equation1661 => Equation3523
Equation1661 => Equation3524
Equation1661 => Equation3527
Equation1661 => Equation4268
Equation1661 => Equation4314
Equation1661 => Equation4315
Equation1681 => Equation3862
Equation1681 => Equation3877
Equation1692 => Equation23
Equation1692 => Equation47
Equation1692 => Equation63
Equation1692 => Equation1832
Equation1692 => Equation1922
Equation1692 => Equation2441
Equation1692 => Equation3050
Equation1692 => Equation3456
Equation1692 => Equation3522
Equation1692 => Equation4065
Equation1692 => Equation4118
Equation1701 => Equation8
Equation1701 => Equation411
Equation1701 => Equation1020
Equation1701 => Equation1035
Equation1701 => Equation1832
Equation1701 => Equation1884
Equation1701 => Equation3253
Equation1701 => Equation3319
Equation1701 => Equation3862
Equation1701 => Equation3877
Equation1701 => Equation3915
Equation1701 => Equation4587
Equation1722 => Equation1832
Equation1722 => Equation2644
Equation1722 => Equation2737
Equation1722 => Equation3050
Equation1722 => Equation3143
Equation1728 => Equation99
Equation1729 => Equation817
Equation1729 => Equation917
Equation1924 => Equation151
Equation2126 => Equation151
Equation2338 => Equation4435
Equation2531 => Equation3
Equation2531 => Equation151
Equation2531 => Equation3659
Equation2531 => Equation3715
Equation2531 => Equation3722
Equation2531 => Equation4380
Equation2531 => Equation4435
Equation2531 => Equation4470
Equation3116 => Equation4380
Equation3116 => Equation4435
Equation3308 => Equation3456
Equation3308 => Equation3511
Equation3342 => Equation3456
Equation3342 => Equation3522
Equation3342 => Equation4065
Equation3342 => Equation4118
Equation3352 => Equation4065
Equation3475 => Equation3659
Equation3545 => Equation3862
Equation3549 => Equation3862
Equation3549 => Equation3955
Equation3555 => Equation3862
Equation3588 => Equation3862
Equation3588 => Equation3878
Equation3588 => Equation3917
Equation3588 => Equation3955
Equation3588 => Equation3994 (*)
Equation3888 => Equation3659