OAI/Combinatorics/SnakyCertificate/Reconstruction.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SnakyCertificate.Check.cache_equations_range_0 line 22
  2. theorem OAI.SnakyCertificate.Check.cache_equations_range_16 line 42
  3. theorem OAI.SnakyCertificate.Check.cache_equations_range_32 line 62
  4. theorem OAI.SnakyCertificate.Check.cache_equations_range_48 line 82
  5. theorem OAI.SnakyCertificate.Check.cache_equations_range_64 line 102
  6. theorem OAI.SnakyCertificate.Check.cache_equations_range_80 line 122
  7. theorem OAI.SnakyCertificate.Check.cache_equations_range_96 line 142
  8. theorem OAI.SnakyCertificate.Check.cache_equations_range_112 line 162
  9. theorem OAI.SnakyCertificate.Check.cache_equations_range_128 line 182
  10. theorem OAI.SnakyCertificate.Check.cache_equations_range_144 line 202
  11. theorem OAI.SnakyCertificate.Check.cache_equations_range_160 line 222
  12. theorem OAI.SnakyCertificate.Check.cache_equations_range_176 line 242
  13. theorem OAI.SnakyCertificate.Check.cache_equations_range_192 line 262
  14. theorem OAI.SnakyCertificate.Check.cache_equations_range_208 line 282
  15. theorem OAI.SnakyCertificate.Check.cache_equations_range_224 line 302
  16. theorem OAI.SnakyCertificate.Check.cache_equations_range_240 line 322
  17. theorem OAI.SnakyCertificate.Check.cache_equations_range_256 line 342
  18. theorem OAI.SnakyCertificate.Check.cache_equations_range_272 line 362
  19. theorem OAI.SnakyCertificate.Check.cache_equations_range_288 line 382
  20. theorem OAI.SnakyCertificate.Check.cache_equations_range_304 line 402
  21. theorem OAI.SnakyCertificate.Check.cache_equations_range_320 line 422
  22. theorem OAI.SnakyCertificate.Check.cache_equations_range_336 line 442
  23. theorem OAI.SnakyCertificate.Check.cache_equations_range_352 line 462
  24. theorem OAI.SnakyCertificate.Check.cache_equations_range_368 line 482
  25. theorem OAI.SnakyCertificate.Check.cache_equations_range_384 line 502
  26. theorem OAI.SnakyCertificate.Check.cache_equations_range_400 line 522
  27. theorem OAI.SnakyCertificate.Check.cache_equations_range_416 line 542
  28. theorem OAI.SnakyCertificate.Check.cache_equations_range_432 line 562
  29. theorem OAI.SnakyCertificate.Check.cache_equations_range_448 line 582
  30. theorem OAI.SnakyCertificate.Check.cache_equations_range_464 line 602
  31. theorem OAI.SnakyCertificate.Check.cache_equations_range_480 line 622
  32. theorem OAI.SnakyCertificate.Check.cache_equations_range_496 line 642
  33. theorem OAI.SnakyCertificate.Check.cache_equations_range_512 line 662
  34. theorem OAI.SnakyCertificate.Check.cache_equations_range_528 line 682
  35. theorem OAI.SnakyCertificate.Check.cache_equations_range_544 line 702
  36. theorem OAI.SnakyCertificate.Check.cache_equations_range_560 line 722
  37. theorem OAI.SnakyCertificate.Check.cache_equations_range_576 line 742
  38. theorem OAI.SnakyCertificate.Check.cache_equations_range_592 line 762
  39. theorem OAI.SnakyCertificate.Check.cache_equations_range_608 line 782
  40. theorem OAI.SnakyCertificate.Check.cache_equations_range_0_32 line 794
  41. theorem OAI.SnakyCertificate.Check.cache_equations_range_32_64 line 797
  42. theorem OAI.SnakyCertificate.Check.cache_equations_range_0_64 line 800
  43. theorem OAI.SnakyCertificate.Check.cache_equations_range_64_96 line 803
  44. theorem OAI.SnakyCertificate.Check.cache_equations_range_112_144 line 806
  45. theorem OAI.SnakyCertificate.Check.cache_equations_range_96_144 line 809
  46. theorem OAI.SnakyCertificate.Check.cache_equations_range_64_144 line 812
  47. theorem OAI.SnakyCertificate.Check.cache_equations_range_0_144 line 815
  48. theorem OAI.SnakyCertificate.Check.cache_equations_range_144_176 line 818
  49. theorem OAI.SnakyCertificate.Check.cache_equations_range_192_224 line 821
  50. theorem OAI.SnakyCertificate.Check.cache_equations_range_176_224 line 824
  51. theorem OAI.SnakyCertificate.Check.cache_equations_range_144_224 line 827
  52. theorem OAI.SnakyCertificate.Check.cache_equations_range_224_256 line 830
  53. theorem OAI.SnakyCertificate.Check.cache_equations_range_272_304 line 833
  54. theorem OAI.SnakyCertificate.Check.cache_equations_range_256_304 line 836
  55. theorem OAI.SnakyCertificate.Check.cache_equations_range_224_304 line 839
  56. theorem OAI.SnakyCertificate.Check.cache_equations_range_144_304 line 842
  57. theorem OAI.SnakyCertificate.Check.cache_equations_range_0_304 line 845
  58. theorem OAI.SnakyCertificate.Check.cache_equations_range_304_336 line 848
  59. theorem OAI.SnakyCertificate.Check.cache_equations_range_352_384 line 851
  60. theorem OAI.SnakyCertificate.Check.cache_equations_range_336_384 line 854
  61. theorem OAI.SnakyCertificate.Check.cache_equations_range_304_384 line 857
  62. theorem OAI.SnakyCertificate.Check.cache_equations_range_384_416 line 860
  63. theorem OAI.SnakyCertificate.Check.cache_equations_range_432_464 line 863
  64. theorem OAI.SnakyCertificate.Check.cache_equations_range_416_464 line 866
  65. theorem OAI.SnakyCertificate.Check.cache_equations_range_384_464 line 869
  66. theorem OAI.SnakyCertificate.Check.cache_equations_range_304_464 line 872
  67. theorem OAI.SnakyCertificate.Check.cache_equations_range_464_496 line 875
  68. theorem OAI.SnakyCertificate.Check.cache_equations_range_512_544 line 878
  69. theorem OAI.SnakyCertificate.Check.cache_equations_range_496_544 line 881
  70. theorem OAI.SnakyCertificate.Check.cache_equations_range_464_544 line 884
  71. theorem OAI.SnakyCertificate.Check.cache_equations_range_544_576 line 887
  72. theorem OAI.SnakyCertificate.Check.cache_equations_range_592_616 line 890
  73. theorem OAI.SnakyCertificate.Check.cache_equations_range_576_616 line 893
  74. theorem OAI.SnakyCertificate.Check.cache_equations_range_544_616 line 896
  75. theorem OAI.SnakyCertificate.Check.cache_equations_range_464_616 line 899
  76. theorem OAI.SnakyCertificate.Check.cache_equations_range_304_616 line 902
  77. theorem OAI.SnakyCertificate.Check.cache_equations_range_0_616 line 905
  78. theorem OAI.SnakyCertificate.Check.cache_equations line 908