Block1Row20.lean`

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MUB6.Certificate.GramEntries.Block1.rows20_0 line 20
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_0 line 22
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_0 line 26
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_0 line 49
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_1 line 56
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_1 line 58
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_1 line 62
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_1 line 85
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_2 line 92
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_2 line 94
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_2 line 98
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_2 line 121
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_3 line 128
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_3 line 130
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_3 line 134
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_3 line 157
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_4 line 164
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_4 line 166
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_4 line 170
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_4 line 193
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_5 line 200
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_5 line 202
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_5 line 206
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_5 line 229
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_6 line 236
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_6 line 238
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_6 line 242
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_6 line 265
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_7 line 272
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_7 line 274
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_7 line 278
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_7 line 301
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_8 line 308
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_8 line 310
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_8 line 314
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_8 line 337
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_9 line 344
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_9 line 346
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_9 line 350
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_9 line 373
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_10 line 380
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_10 line 382
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_10 line 386
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_10 line 409
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_11 line 416
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_11 line 418
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_11 line 422
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_11 line 445
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_12 line 452
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_12 line 454
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_12 line 458
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_12 line 481
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_13 line 488
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_13 line 490
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_13 line 494
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_13 line 517
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_14 line 524
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_14 line 526
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_14 line 530
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_14 line 553
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_15 line 560
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_15 line 562
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_15 line 566
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_15 line 589
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_16 line 596
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_16 line 598
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_16 line 602
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_16 line 625
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_17 line 632
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_17 line 634
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_17 line 638
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_17 line 661
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_18 line 668
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_18 line 670
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_18 line 674
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_18 line 697
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_19 line 704
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_19 line 706
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_19 line 710
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_19 line 733
def OAI.MUB6.Certificate.GramEntries.Block1.rows20_20 line 740
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck20_20 line 742
theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound20_20 line 746
theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval20_20 line 769