OAI/Combinatorics/SnakyCertificate/TableList.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyCertificate.tableListChunk_0 line 7
  2. def OAI.SnakyCertificate.tableListChunk_1 line 9
  3. def OAI.SnakyCertificate.tableListChunk_2 line 11
  4. def OAI.SnakyCertificate.tableListChunk_3 line 13
  5. def OAI.SnakyCertificate.tableListChunk_4 line 15
  6. def OAI.SnakyCertificate.tableListChunk_5 line 17
  7. def OAI.SnakyCertificate.tableListChunk_6 line 19
  8. def OAI.SnakyCertificate.tableListChunk_7 line 21
  9. def OAI.SnakyCertificate.tableListChunk_8 line 23
  10. def OAI.SnakyCertificate.tableListChunk_9 line 25
  11. def OAI.SnakyCertificate.tableListChunk_10 line 27
  12. def OAI.SnakyCertificate.tableListChunk_11 line 29
  13. def OAI.SnakyCertificate.tableListChunk_12 line 31
  14. def OAI.SnakyCertificate.tableListChunk_13 line 33
  15. def OAI.SnakyCertificate.tableListChunk_14 line 35
  16. def OAI.SnakyCertificate.tableListChunk_15 line 37
  17. def OAI.SnakyCertificate.tableListChunk_16 line 39
  18. def OAI.SnakyCertificate.tableListChunk_17 line 41
  19. def OAI.SnakyCertificate.tableListChunk_18 line 43
  20. def OAI.SnakyCertificate.tableListChunk_19 line 45
  21. def OAI.SnakyCertificate.tableListChunk_20 line 47
  22. def OAI.SnakyCertificate.tableListChunk_21 line 49
  23. def OAI.SnakyCertificate.tableListChunk_22 line 51
  24. def OAI.SnakyCertificate.tableListChunk_23 line 53
  25. def OAI.SnakyCertificate.tableListChunk_24 line 55
  26. def OAI.SnakyCertificate.tableListChunk_25 line 57
  27. def OAI.SnakyCertificate.tableListChunk_26 line 59
  28. def OAI.SnakyCertificate.tableListChunk_27 line 61
  29. def OAI.SnakyCertificate.tableListChunk_28 line 63
  30. def OAI.SnakyCertificate.tableListChunk_29 line 65
  31. def OAI.SnakyCertificate.tableListChunk_30 line 67
  32. def OAI.SnakyCertificate.tableList line 69
  33. theorem OAI.SnakyCertificate.table_toList line 71
  34. theorem OAI.SnakyCertificate.table_getElem?_eq line 75
  35. theorem OAI.SnakyCertificate.merge_ranges line 78
  36. theorem OAI.SnakyCertificate.fin_block_range line 87