OAI/Combinatorics/SnakyCertificate/Heights.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SnakyCertificate.Check.cache_height_block_0 line 8
  2. theorem OAI.SnakyCertificate.Check.cache_height_range_0 line 11
  3. theorem OAI.SnakyCertificate.Check.cache_height_block_16 line 14
  4. theorem OAI.SnakyCertificate.Check.cache_height_range_16 line 17
  5. theorem OAI.SnakyCertificate.Check.cache_height_block_32 line 20
  6. theorem OAI.SnakyCertificate.Check.cache_height_range_32 line 23
  7. theorem OAI.SnakyCertificate.Check.cache_height_block_48 line 26
  8. theorem OAI.SnakyCertificate.Check.cache_height_range_48 line 29
  9. theorem OAI.SnakyCertificate.Check.cache_height_block_64 line 32
  10. theorem OAI.SnakyCertificate.Check.cache_height_range_64 line 35
  11. theorem OAI.SnakyCertificate.Check.cache_height_block_80 line 38
  12. theorem OAI.SnakyCertificate.Check.cache_height_range_80 line 41
  13. theorem OAI.SnakyCertificate.Check.cache_height_block_96 line 44
  14. theorem OAI.SnakyCertificate.Check.cache_height_range_96 line 47
  15. theorem OAI.SnakyCertificate.Check.cache_height_block_112 line 50
  16. theorem OAI.SnakyCertificate.Check.cache_height_range_112 line 53
  17. theorem OAI.SnakyCertificate.Check.cache_height_block_128 line 56
  18. theorem OAI.SnakyCertificate.Check.cache_height_range_128 line 59
  19. theorem OAI.SnakyCertificate.Check.cache_height_block_144 line 62
  20. theorem OAI.SnakyCertificate.Check.cache_height_range_144 line 65
  21. theorem OAI.SnakyCertificate.Check.cache_height_block_160 line 68
  22. theorem OAI.SnakyCertificate.Check.cache_height_range_160 line 71
  23. theorem OAI.SnakyCertificate.Check.cache_height_block_176 line 74
  24. theorem OAI.SnakyCertificate.Check.cache_height_range_176 line 77
  25. theorem OAI.SnakyCertificate.Check.cache_height_block_192 line 80
  26. theorem OAI.SnakyCertificate.Check.cache_height_range_192 line 83
  27. theorem OAI.SnakyCertificate.Check.cache_height_block_208 line 86
  28. theorem OAI.SnakyCertificate.Check.cache_height_range_208 line 89
  29. theorem OAI.SnakyCertificate.Check.cache_height_block_224 line 92
  30. theorem OAI.SnakyCertificate.Check.cache_height_range_224 line 95
  31. theorem OAI.SnakyCertificate.Check.cache_height_block_240 line 98
  32. theorem OAI.SnakyCertificate.Check.cache_height_range_240 line 101
  33. theorem OAI.SnakyCertificate.Check.cache_height_block_256 line 104
  34. theorem OAI.SnakyCertificate.Check.cache_height_range_256 line 107
  35. theorem OAI.SnakyCertificate.Check.cache_height_block_272 line 110
  36. theorem OAI.SnakyCertificate.Check.cache_height_range_272 line 113
  37. theorem OAI.SnakyCertificate.Check.cache_height_block_288 line 116
  38. theorem OAI.SnakyCertificate.Check.cache_height_range_288 line 119
  39. theorem OAI.SnakyCertificate.Check.cache_height_block_304 line 122
  40. theorem OAI.SnakyCertificate.Check.cache_height_range_304 line 125
  41. theorem OAI.SnakyCertificate.Check.cache_height_block_320 line 128
  42. theorem OAI.SnakyCertificate.Check.cache_height_range_320 line 131
  43. theorem OAI.SnakyCertificate.Check.cache_height_block_336 line 134
  44. theorem OAI.SnakyCertificate.Check.cache_height_range_336 line 137
  45. theorem OAI.SnakyCertificate.Check.cache_height_block_352 line 140
  46. theorem OAI.SnakyCertificate.Check.cache_height_range_352 line 143
  47. theorem OAI.SnakyCertificate.Check.cache_height_block_368 line 146
  48. theorem OAI.SnakyCertificate.Check.cache_height_range_368 line 149
  49. theorem OAI.SnakyCertificate.Check.cache_height_block_384 line 152
  50. theorem OAI.SnakyCertificate.Check.cache_height_range_384 line 155
  51. theorem OAI.SnakyCertificate.Check.cache_height_block_400 line 158
  52. theorem OAI.SnakyCertificate.Check.cache_height_range_400 line 161
  53. theorem OAI.SnakyCertificate.Check.cache_height_block_416 line 164
  54. theorem OAI.SnakyCertificate.Check.cache_height_range_416 line 167
  55. theorem OAI.SnakyCertificate.Check.cache_height_block_432 line 170
  56. theorem OAI.SnakyCertificate.Check.cache_height_range_432 line 173
  57. theorem OAI.SnakyCertificate.Check.cache_height_block_448 line 176
  58. theorem OAI.SnakyCertificate.Check.cache_height_range_448 line 179
  59. theorem OAI.SnakyCertificate.Check.cache_height_block_464 line 182
  60. theorem OAI.SnakyCertificate.Check.cache_height_range_464 line 185
  61. theorem OAI.SnakyCertificate.Check.cache_height_block_480 line 188
  62. theorem OAI.SnakyCertificate.Check.cache_height_range_480 line 191
  63. theorem OAI.SnakyCertificate.Check.cache_height_block_496 line 194
  64. theorem OAI.SnakyCertificate.Check.cache_height_range_496 line 197
  65. theorem OAI.SnakyCertificate.Check.cache_height_block_512 line 200
  66. theorem OAI.SnakyCertificate.Check.cache_height_range_512 line 203
  67. theorem OAI.SnakyCertificate.Check.cache_height_block_528 line 206
  68. theorem OAI.SnakyCertificate.Check.cache_height_range_528 line 209
  69. theorem OAI.SnakyCertificate.Check.cache_height_block_544 line 212
  70. theorem OAI.SnakyCertificate.Check.cache_height_range_544 line 215
  71. theorem OAI.SnakyCertificate.Check.cache_height_block_560 line 218
  72. theorem OAI.SnakyCertificate.Check.cache_height_range_560 line 221
  73. theorem OAI.SnakyCertificate.Check.cache_height_block_576 line 224
  74. theorem OAI.SnakyCertificate.Check.cache_height_range_576 line 227
  75. theorem OAI.SnakyCertificate.Check.cache_height_block_592 line 230
  76. theorem OAI.SnakyCertificate.Check.cache_height_range_592 line 233
  77. theorem OAI.SnakyCertificate.Check.cache_height_block_608 line 236
  78. theorem OAI.SnakyCertificate.Check.cache_height_range_608 line 239
  79. theorem OAI.SnakyCertificate.Check.cache_height_range_0_32 line 242
  80. theorem OAI.SnakyCertificate.Check.cache_height_range_32_64 line 245
  81. theorem OAI.SnakyCertificate.Check.cache_height_range_0_64 line 248
  82. theorem OAI.SnakyCertificate.Check.cache_height_range_64_96 line 251
  83. theorem OAI.SnakyCertificate.Check.cache_height_range_112_144 line 254
  84. theorem OAI.SnakyCertificate.Check.cache_height_range_96_144 line 257
  85. theorem OAI.SnakyCertificate.Check.cache_height_range_64_144 line 260
  86. theorem OAI.SnakyCertificate.Check.cache_height_range_0_144 line 263
  87. theorem OAI.SnakyCertificate.Check.cache_height_range_144_176 line 266
  88. theorem OAI.SnakyCertificate.Check.cache_height_range_192_224 line 269
  89. theorem OAI.SnakyCertificate.Check.cache_height_range_176_224 line 272
  90. theorem OAI.SnakyCertificate.Check.cache_height_range_144_224 line 275
  91. theorem OAI.SnakyCertificate.Check.cache_height_range_224_256 line 278
  92. theorem OAI.SnakyCertificate.Check.cache_height_range_272_304 line 281
  93. theorem OAI.SnakyCertificate.Check.cache_height_range_256_304 line 284
  94. theorem OAI.SnakyCertificate.Check.cache_height_range_224_304 line 287
  95. theorem OAI.SnakyCertificate.Check.cache_height_range_144_304 line 290
  96. theorem OAI.SnakyCertificate.Check.cache_height_range_0_304 line 293
  97. theorem OAI.SnakyCertificate.Check.cache_height_range_304_336 line 296
  98. theorem OAI.SnakyCertificate.Check.cache_height_range_352_384 line 299
  99. theorem OAI.SnakyCertificate.Check.cache_height_range_336_384 line 302
  100. theorem OAI.SnakyCertificate.Check.cache_height_range_304_384 line 305
  101. theorem OAI.SnakyCertificate.Check.cache_height_range_384_416 line 308
  102. theorem OAI.SnakyCertificate.Check.cache_height_range_432_464 line 311
  103. theorem OAI.SnakyCertificate.Check.cache_height_range_416_464 line 314
  104. theorem OAI.SnakyCertificate.Check.cache_height_range_384_464 line 317
  105. theorem OAI.SnakyCertificate.Check.cache_height_range_304_464 line 320
  106. theorem OAI.SnakyCertificate.Check.cache_height_range_464_496 line 323
  107. theorem OAI.SnakyCertificate.Check.cache_height_range_512_544 line 326
  108. theorem OAI.SnakyCertificate.Check.cache_height_range_496_544 line 329
  109. theorem OAI.SnakyCertificate.Check.cache_height_range_464_544 line 332
  110. theorem OAI.SnakyCertificate.Check.cache_height_range_544_576 line 335
  111. theorem OAI.SnakyCertificate.Check.cache_height_range_592_616 line 338
  112. theorem OAI.SnakyCertificate.Check.cache_height_range_576_616 line 341
  113. theorem OAI.SnakyCertificate.Check.cache_height_range_544_616 line 344
  114. theorem OAI.SnakyCertificate.Check.cache_height_range_464_616 line 347
  115. theorem OAI.SnakyCertificate.Check.cache_height_range_304_616 line 350
  116. theorem OAI.SnakyCertificate.Check.cache_height_range_0_616 line 353
  117. theorem OAI.SnakyCertificate.Check.cache_heights line 356