OAI/Combinatorics/SnakyCertificate/TableValidity.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SnakyCertificate.table_size line 7
2. abbrev OAI.SnakyCertificate.TableEntryOk line 11
3. theorem OAI.SnakyCertificate.table_entries_block_0 line 15
4. theorem OAI.SnakyCertificate.table_entries_range_0 line 20
5. theorem OAI.SnakyCertificate.table_entries_block_10 line 23
6. theorem OAI.SnakyCertificate.table_entries_range_10 line 28
7. theorem OAI.SnakyCertificate.table_entries_block_20 line 31
8. theorem OAI.SnakyCertificate.table_entries_range_20 line 36
9. theorem OAI.SnakyCertificate.table_entries_block_30 line 39
10. theorem OAI.SnakyCertificate.table_entries_range_30 line 44
11. theorem OAI.SnakyCertificate.table_entries_block_40 line 47
12. theorem OAI.SnakyCertificate.table_entries_range_40 line 52
13. theorem OAI.SnakyCertificate.table_entries_block_50 line 55
14. theorem OAI.SnakyCertificate.table_entries_range_50 line 60
15. theorem OAI.SnakyCertificate.table_entries_block_60 line 63
16. theorem OAI.SnakyCertificate.table_entries_range_60 line 68
17. theorem OAI.SnakyCertificate.table_entries_block_70 line 71
18. theorem OAI.SnakyCertificate.table_entries_range_70 line 76
19. theorem OAI.SnakyCertificate.table_entries_block_80 line 79
20. theorem OAI.SnakyCertificate.table_entries_range_80 line 84
21. theorem OAI.SnakyCertificate.table_entries_block_90 line 87
22. theorem OAI.SnakyCertificate.table_entries_range_90 line 92
23. theorem OAI.SnakyCertificate.table_entries_block_100 line 95
24. theorem OAI.SnakyCertificate.table_entries_range_100 line 100
25. theorem OAI.SnakyCertificate.table_entries_block_110 line 103
26. theorem OAI.SnakyCertificate.table_entries_range_110 line 108
27. theorem OAI.SnakyCertificate.table_entries_block_120 line 111
28. theorem OAI.SnakyCertificate.table_entries_range_120 line 116
29. theorem OAI.SnakyCertificate.table_entries_block_130 line 119
30. theorem OAI.SnakyCertificate.table_entries_range_130 line 124
31. theorem OAI.SnakyCertificate.table_entries_block_140 line 127
32. theorem OAI.SnakyCertificate.table_entries_range_140 line 132
33. theorem OAI.SnakyCertificate.table_entries_block_150 line 135
34. theorem OAI.SnakyCertificate.table_entries_range_150 line 140
35. theorem OAI.SnakyCertificate.table_entries_block_160 line 143
36. theorem OAI.SnakyCertificate.table_entries_range_160 line 148
37. theorem OAI.SnakyCertificate.table_entries_block_170 line 151
38. theorem OAI.SnakyCertificate.table_entries_range_170 line 156
39. theorem OAI.SnakyCertificate.table_entries_block_180 line 159
40. theorem OAI.SnakyCertificate.table_entries_range_180 line 164
41. theorem OAI.SnakyCertificate.table_entries_block_190 line 167
42. theorem OAI.SnakyCertificate.table_entries_range_190 line 172
43. theorem OAI.SnakyCertificate.table_entries_block_200 line 175
44. theorem OAI.SnakyCertificate.table_entries_range_200 line 180
45. theorem OAI.SnakyCertificate.table_entries_block_210 line 183
46. theorem OAI.SnakyCertificate.table_entries_range_210 line 188
47. theorem OAI.SnakyCertificate.table_entries_block_220 line 191
48. theorem OAI.SnakyCertificate.table_entries_range_220 line 196
49. theorem OAI.SnakyCertificate.table_entries_block_230 line 199
50. theorem OAI.SnakyCertificate.table_entries_range_230 line 204
51. theorem OAI.SnakyCertificate.table_entries_block_240 line 207
52. theorem OAI.SnakyCertificate.table_entries_range_240 line 212
53. theorem OAI.SnakyCertificate.table_entries_block_250 line 215
54. theorem OAI.SnakyCertificate.table_entries_range_250 line 220
55. theorem OAI.SnakyCertificate.table_entries_block_260 line 223
56. theorem OAI.SnakyCertificate.table_entries_range_260 line 228
57. theorem OAI.SnakyCertificate.table_entries_block_270 line 231
58. theorem OAI.SnakyCertificate.table_entries_range_270 line 236
59. theorem OAI.SnakyCertificate.table_entries_block_280 line 239
60. theorem OAI.SnakyCertificate.table_entries_range_280 line 244
61. theorem OAI.SnakyCertificate.table_entries_block_290 line 247
62. theorem OAI.SnakyCertificate.table_entries_range_290 line 252
63. theorem OAI.SnakyCertificate.table_entries_block_300 line 255
64. theorem OAI.SnakyCertificate.table_entries_range_300 line 260
65. theorem OAI.SnakyCertificate.table_entries_block_310 line 263
66. theorem OAI.SnakyCertificate.table_entries_range_310 line 268
67. theorem OAI.SnakyCertificate.table_entries_block_320 line 271
68. theorem OAI.SnakyCertificate.table_entries_range_320 line 276
69. theorem OAI.SnakyCertificate.table_entries_block_330 line 279
70. theorem OAI.SnakyCertificate.table_entries_range_330 line 284
71. theorem OAI.SnakyCertificate.table_entries_block_340 line 287
72. theorem OAI.SnakyCertificate.table_entries_range_340 line 292
73. theorem OAI.SnakyCertificate.table_entries_block_350 line 295
74. theorem OAI.SnakyCertificate.table_entries_range_350 line 300
75. theorem OAI.SnakyCertificate.table_entries_block_360 line 303
76. theorem OAI.SnakyCertificate.table_entries_range_360 line 308
77. theorem OAI.SnakyCertificate.table_entries_block_370 line 311
78. theorem OAI.SnakyCertificate.table_entries_range_370 line 316
79. theorem OAI.SnakyCertificate.table_entries_block_380 line 319
80. theorem OAI.SnakyCertificate.table_entries_range_380 line 324
81. theorem OAI.SnakyCertificate.table_entries_block_390 line 327
82. theorem OAI.SnakyCertificate.table_entries_range_390 line 332
83. theorem OAI.SnakyCertificate.table_entries_block_400 line 335
84. theorem OAI.SnakyCertificate.table_entries_range_400 line 340
85. theorem OAI.SnakyCertificate.table_entries_block_410 line 343
86. theorem OAI.SnakyCertificate.table_entries_range_410 line 348
87. theorem OAI.SnakyCertificate.table_entries_block_420 line 351
88. theorem OAI.SnakyCertificate.table_entries_range_420 line 356
89. theorem OAI.SnakyCertificate.table_entries_block_430 line 359
90. theorem OAI.SnakyCertificate.table_entries_range_430 line 364
91. theorem OAI.SnakyCertificate.table_entries_block_440 line 367
92. theorem OAI.SnakyCertificate.table_entries_range_440 line 372
93. theorem OAI.SnakyCertificate.table_entries_block_450 line 375
94. theorem OAI.SnakyCertificate.table_entries_range_450 line 380
95. theorem OAI.SnakyCertificate.table_entries_block_460 line 383
96. theorem OAI.SnakyCertificate.table_entries_range_460 line 388
97. theorem OAI.SnakyCertificate.table_entries_block_470 line 391
98. theorem OAI.SnakyCertificate.table_entries_range_470 line 396
99. theorem OAI.SnakyCertificate.table_entries_block_480 line 399
100. theorem OAI.SnakyCertificate.table_entries_range_480 line 404
101. theorem OAI.SnakyCertificate.table_entries_block_490 line 407
102. theorem OAI.SnakyCertificate.table_entries_range_490 line 412
103. theorem OAI.SnakyCertificate.table_entries_block_500 line 415
104. theorem OAI.SnakyCertificate.table_entries_range_500 line 420
105. theorem OAI.SnakyCertificate.table_entries_block_510 line 423
106. theorem OAI.SnakyCertificate.table_entries_range_510 line 428
107. theorem OAI.SnakyCertificate.table_entries_block_520 line 431
108. theorem OAI.SnakyCertificate.table_entries_range_520 line 436
109. theorem OAI.SnakyCertificate.table_entries_block_530 line 439
110. theorem OAI.SnakyCertificate.table_entries_range_530 line 444
111. theorem OAI.SnakyCertificate.table_entries_block_540 line 447
112. theorem OAI.SnakyCertificate.table_entries_range_540 line 452
113. theorem OAI.SnakyCertificate.table_entries_block_550 line 455
114. theorem OAI.SnakyCertificate.table_entries_range_550 line 460
115. theorem OAI.SnakyCertificate.table_entries_block_560 line 463
116. theorem OAI.SnakyCertificate.table_entries_range_560 line 468
117. theorem OAI.SnakyCertificate.table_entries_block_570 line 471
118. theorem OAI.SnakyCertificate.table_entries_range_570 line 476
119. theorem OAI.SnakyCertificate.table_entries_block_580 line 479
120. theorem OAI.SnakyCertificate.table_entries_range_580 line 484
121. theorem OAI.SnakyCertificate.table_entries_block_590 line 487
122. theorem OAI.SnakyCertificate.table_entries_range_590 line 492
123. theorem OAI.SnakyCertificate.table_entries_block_600 line 495
124. theorem OAI.SnakyCertificate.table_entries_range_600 line 500
125. theorem OAI.SnakyCertificate.table_entries_range_10_30 line 503
126. theorem OAI.SnakyCertificate.table_entries_range_0_30 line 506
127. theorem OAI.SnakyCertificate.table_entries_range_30_50 line 509
128. theorem OAI.SnakyCertificate.table_entries_range_50_70 line 512
129. theorem OAI.SnakyCertificate.table_entries_range_30_70 line 515
130. theorem OAI.SnakyCertificate.table_entries_range_0_70 line 518
131. theorem OAI.SnakyCertificate.table_entries_range_70_90 line 521
132. theorem OAI.SnakyCertificate.table_entries_range_90_110 line 524
133. theorem OAI.SnakyCertificate.table_entries_range_70_110 line 527
134. theorem OAI.SnakyCertificate.table_entries_range_110_130 line 530
135. theorem OAI.SnakyCertificate.table_entries_range_130_150 line 533
136. theorem OAI.SnakyCertificate.table_entries_range_110_150 line 536
137. theorem OAI.SnakyCertificate.table_entries_range_70_150 line 539
138. theorem OAI.SnakyCertificate.table_entries_range_0_150 line 542
139. theorem OAI.SnakyCertificate.table_entries_range_160_180 line 545
140. theorem OAI.SnakyCertificate.table_entries_range_150_180 line 548
141. theorem OAI.SnakyCertificate.table_entries_range_180_200 line 551
142. theorem OAI.SnakyCertificate.table_entries_range_200_220 line 554
143. theorem OAI.SnakyCertificate.table_entries_range_180_220 line 557
144. theorem OAI.SnakyCertificate.table_entries_range_150_220 line 560
145. theorem OAI.SnakyCertificate.table_entries_range_220_240 line 563
146. theorem OAI.SnakyCertificate.table_entries_range_240_260 line 566
147. theorem OAI.SnakyCertificate.table_entries_range_220_260 line 569
148. theorem OAI.SnakyCertificate.table_entries_range_260_280 line 572
149. theorem OAI.SnakyCertificate.table_entries_range_280_300 line 575
150. theorem OAI.SnakyCertificate.table_entries_range_260_300 line 578
151. theorem OAI.SnakyCertificate.table_entries_range_220_300 line 581
152. theorem OAI.SnakyCertificate.table_entries_range_150_300 line 584
153. theorem OAI.SnakyCertificate.table_entries_range_0_300 line 587
154. theorem OAI.SnakyCertificate.table_entries_range_310_330 line 590
155. theorem OAI.SnakyCertificate.table_entries_range_300_330 line 593
156. theorem OAI.SnakyCertificate.table_entries_range_330_350 line 596
157. theorem OAI.SnakyCertificate.table_entries_range_350_370 line 599
158. theorem OAI.SnakyCertificate.table_entries_range_330_370 line 602
159. theorem OAI.SnakyCertificate.table_entries_range_300_370 line 605
160. theorem OAI.SnakyCertificate.table_entries_range_370_390 line 608
161. theorem OAI.SnakyCertificate.table_entries_range_390_410 line 611
162. theorem OAI.SnakyCertificate.table_entries_range_370_410 line 614
163. theorem OAI.SnakyCertificate.table_entries_range_410_430 line 617
164. theorem OAI.SnakyCertificate.table_entries_range_430_450 line 620
165. theorem OAI.SnakyCertificate.table_entries_range_410_450 line 623
166. theorem OAI.SnakyCertificate.table_entries_range_370_450 line 626
167. theorem OAI.SnakyCertificate.table_entries_range_300_450 line 629
168. theorem OAI.SnakyCertificate.table_entries_range_450_470 line 632
169. theorem OAI.SnakyCertificate.table_entries_range_470_490 line 635
170. theorem OAI.SnakyCertificate.table_entries_range_450_490 line 638
171. theorem OAI.SnakyCertificate.table_entries_range_490_510 line 641
172. theorem OAI.SnakyCertificate.table_entries_range_510_530 line 644
173. theorem OAI.SnakyCertificate.table_entries_range_490_530 line 647
174. theorem OAI.SnakyCertificate.table_entries_range_450_530 line 650
175. theorem OAI.SnakyCertificate.table_entries_range_530_550 line 653
176. theorem OAI.SnakyCertificate.table_entries_range_550_570 line 656
177. theorem OAI.SnakyCertificate.table_entries_range_530_570 line 659
178. theorem OAI.SnakyCertificate.table_entries_range_570_590 line 662
179. theorem OAI.SnakyCertificate.table_entries_range_590_610 line 665
180. theorem OAI.SnakyCertificate.table_entries_range_570_610 line 668
181. theorem OAI.SnakyCertificate.table_entries_range_530_610 line 671
182. theorem OAI.SnakyCertificate.table_entries_range_450_610 line 674
183. theorem OAI.SnakyCertificate.table_entries_range_300_610 line 677
184. theorem OAI.SnakyCertificate.table_entries_range_0_610 line 680
185. theorem OAI.SnakyCertificate.table_entries_valid line 683
186. theorem OAI.SnakyCertificate.table_valid line 689
187. theorem OAI.SnakyCertificate.placement_count line 694
188. theorem OAI.SnakyCertificate.entryAt_index line 698
189. theorem OAI.SnakyCertificate.entryAt_nonempty line 703
190. theorem OAI.SnakyCertificate.entryAt_backward line 707