OAI/Combinatorics/SnakyCertificate/Equations02.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SnakyCertificate.Check.verified_row_80 line 8
  2. theorem OAI.SnakyCertificate.Check.load_entry_80 line 11
  3. theorem OAI.SnakyCertificate.Check.cache_equation_80 line 15
  4. theorem OAI.SnakyCertificate.Check.verified_row_81 line 21
  5. theorem OAI.SnakyCertificate.Check.load_entry_81 line 24
  6. theorem OAI.SnakyCertificate.Check.cache_equation_81 line 28
  7. theorem OAI.SnakyCertificate.Check.verified_row_82 line 34
  8. theorem OAI.SnakyCertificate.Check.load_entry_82 line 37
  9. theorem OAI.SnakyCertificate.Check.cache_equation_82 line 41
  10. theorem OAI.SnakyCertificate.Check.verified_row_83 line 47
  11. theorem OAI.SnakyCertificate.Check.load_entry_83 line 50
  12. theorem OAI.SnakyCertificate.Check.cache_equation_83 line 54
  13. theorem OAI.SnakyCertificate.Check.verified_row_84 line 60
  14. theorem OAI.SnakyCertificate.Check.load_entry_84 line 63
  15. theorem OAI.SnakyCertificate.Check.cache_equation_84 line 67
  16. theorem OAI.SnakyCertificate.Check.verified_row_85 line 73
  17. theorem OAI.SnakyCertificate.Check.load_entry_85 line 76
  18. theorem OAI.SnakyCertificate.Check.cache_equation_85 line 80
  19. theorem OAI.SnakyCertificate.Check.verified_row_86 line 86
  20. theorem OAI.SnakyCertificate.Check.load_entry_86 line 89
  21. theorem OAI.SnakyCertificate.Check.cache_equation_86 line 93
  22. theorem OAI.SnakyCertificate.Check.verified_row_87 line 99
  23. theorem OAI.SnakyCertificate.Check.load_entry_87 line 102
  24. theorem OAI.SnakyCertificate.Check.cache_equation_87 line 106
  25. theorem OAI.SnakyCertificate.Check.verified_row_88 line 112
  26. theorem OAI.SnakyCertificate.Check.load_entry_88 line 115
  27. theorem OAI.SnakyCertificate.Check.cache_equation_88 line 119
  28. theorem OAI.SnakyCertificate.Check.verified_row_89 line 125
  29. theorem OAI.SnakyCertificate.Check.load_entry_89 line 128
  30. theorem OAI.SnakyCertificate.Check.cache_equation_89 line 132
  31. theorem OAI.SnakyCertificate.Check.verified_row_90 line 138
  32. theorem OAI.SnakyCertificate.Check.load_entry_90 line 141
  33. theorem OAI.SnakyCertificate.Check.cache_equation_90 line 145
  34. theorem OAI.SnakyCertificate.Check.verified_row_91 line 151
  35. theorem OAI.SnakyCertificate.Check.load_entry_91 line 154
  36. theorem OAI.SnakyCertificate.Check.cache_equation_91 line 158
  37. theorem OAI.SnakyCertificate.Check.verified_row_92 line 164
  38. theorem OAI.SnakyCertificate.Check.load_entry_92 line 167
  39. theorem OAI.SnakyCertificate.Check.cache_equation_92 line 171
  40. theorem OAI.SnakyCertificate.Check.verified_row_93 line 177
  41. theorem OAI.SnakyCertificate.Check.load_entry_93 line 180
  42. theorem OAI.SnakyCertificate.Check.cache_equation_93 line 184
  43. theorem OAI.SnakyCertificate.Check.verified_row_94 line 190
  44. theorem OAI.SnakyCertificate.Check.load_entry_94 line 193
  45. theorem OAI.SnakyCertificate.Check.cache_equation_94 line 197
  46. theorem OAI.SnakyCertificate.Check.verified_row_95 line 203
  47. theorem OAI.SnakyCertificate.Check.load_entry_95 line 206
  48. theorem OAI.SnakyCertificate.Check.cache_equation_95 line 210
  49. theorem OAI.SnakyCertificate.Check.verified_row_96 line 216
  50. theorem OAI.SnakyCertificate.Check.load_entry_96 line 219
  51. theorem OAI.SnakyCertificate.Check.cache_equation_96 line 223
  52. theorem OAI.SnakyCertificate.Check.verified_row_97 line 229
  53. theorem OAI.SnakyCertificate.Check.load_entry_97 line 232
  54. theorem OAI.SnakyCertificate.Check.cache_equation_97 line 236
  55. theorem OAI.SnakyCertificate.Check.verified_row_98 line 242
  56. theorem OAI.SnakyCertificate.Check.load_entry_98 line 245
  57. theorem OAI.SnakyCertificate.Check.cache_equation_98 line 249
  58. theorem OAI.SnakyCertificate.Check.verified_row_99 line 255
  59. theorem OAI.SnakyCertificate.Check.load_entry_99 line 258
  60. theorem OAI.SnakyCertificate.Check.cache_equation_99 line 262
  61. theorem OAI.SnakyCertificate.Check.verified_row_100 line 268
  62. theorem OAI.SnakyCertificate.Check.load_entry_100 line 271
  63. theorem OAI.SnakyCertificate.Check.cache_equation_100 line 275
  64. theorem OAI.SnakyCertificate.Check.verified_row_101 line 281
  65. theorem OAI.SnakyCertificate.Check.load_entry_101 line 284
  66. theorem OAI.SnakyCertificate.Check.cache_equation_101 line 288
  67. theorem OAI.SnakyCertificate.Check.verified_row_102 line 294
  68. theorem OAI.SnakyCertificate.Check.load_entry_102 line 297
  69. theorem OAI.SnakyCertificate.Check.cache_equation_102 line 301
  70. theorem OAI.SnakyCertificate.Check.verified_row_103 line 307
  71. theorem OAI.SnakyCertificate.Check.load_entry_103 line 310
  72. theorem OAI.SnakyCertificate.Check.cache_equation_103 line 314
  73. theorem OAI.SnakyCertificate.Check.verified_row_104 line 320
  74. theorem OAI.SnakyCertificate.Check.load_entry_104 line 323
  75. theorem OAI.SnakyCertificate.Check.cache_equation_104 line 327
  76. theorem OAI.SnakyCertificate.Check.verified_row_105 line 333
  77. theorem OAI.SnakyCertificate.Check.load_entry_105 line 336
  78. theorem OAI.SnakyCertificate.Check.cache_equation_105 line 340
  79. theorem OAI.SnakyCertificate.Check.verified_row_106 line 346
  80. theorem OAI.SnakyCertificate.Check.load_entry_106 line 349
  81. theorem OAI.SnakyCertificate.Check.cache_equation_106 line 353
  82. theorem OAI.SnakyCertificate.Check.verified_row_107 line 359
  83. theorem OAI.SnakyCertificate.Check.load_entry_107 line 362
  84. theorem OAI.SnakyCertificate.Check.cache_equation_107 line 366
  85. theorem OAI.SnakyCertificate.Check.verified_row_108 line 372
  86. theorem OAI.SnakyCertificate.Check.load_entry_108 line 375
  87. theorem OAI.SnakyCertificate.Check.cache_equation_108 line 379
  88. theorem OAI.SnakyCertificate.Check.verified_row_109 line 385
  89. theorem OAI.SnakyCertificate.Check.load_entry_109 line 388
  90. theorem OAI.SnakyCertificate.Check.cache_equation_109 line 392
  91. theorem OAI.SnakyCertificate.Check.verified_row_110 line 398
  92. theorem OAI.SnakyCertificate.Check.load_entry_110 line 401
  93. theorem OAI.SnakyCertificate.Check.cache_equation_110 line 405
  94. theorem OAI.SnakyCertificate.Check.verified_row_111 line 411
  95. theorem OAI.SnakyCertificate.Check.load_entry_111 line 414
  96. theorem OAI.SnakyCertificate.Check.cache_equation_111 line 418
  97. theorem OAI.SnakyCertificate.Check.verified_row_112 line 424
  98. theorem OAI.SnakyCertificate.Check.load_entry_112 line 427
  99. theorem OAI.SnakyCertificate.Check.cache_equation_112 line 431
  100. theorem OAI.SnakyCertificate.Check.verified_row_113 line 437
  101. theorem OAI.SnakyCertificate.Check.load_entry_113 line 440
  102. theorem OAI.SnakyCertificate.Check.cache_equation_113 line 444
  103. theorem OAI.SnakyCertificate.Check.verified_row_114 line 450
  104. theorem OAI.SnakyCertificate.Check.load_entry_114 line 453
  105. theorem OAI.SnakyCertificate.Check.cache_equation_114 line 457
  106. theorem OAI.SnakyCertificate.Check.verified_row_115 line 463
  107. theorem OAI.SnakyCertificate.Check.load_entry_115 line 466
  108. theorem OAI.SnakyCertificate.Check.cache_equation_115 line 470
  109. theorem OAI.SnakyCertificate.Check.verified_row_116 line 476
  110. theorem OAI.SnakyCertificate.Check.load_entry_116 line 479
  111. theorem OAI.SnakyCertificate.Check.cache_equation_116 line 483
  112. theorem OAI.SnakyCertificate.Check.verified_row_117 line 489
  113. theorem OAI.SnakyCertificate.Check.load_entry_117 line 492
  114. theorem OAI.SnakyCertificate.Check.cache_equation_117 line 496
  115. theorem OAI.SnakyCertificate.Check.verified_row_118 line 502
  116. theorem OAI.SnakyCertificate.Check.load_entry_118 line 505
  117. theorem OAI.SnakyCertificate.Check.cache_equation_118 line 509
  118. theorem OAI.SnakyCertificate.Check.verified_row_119 line 515
  119. theorem OAI.SnakyCertificate.Check.load_entry_119 line 518
  120. theorem OAI.SnakyCertificate.Check.cache_equation_119 line 522