OAI/Computability/Superstring/BlockClose.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Superstring.BlockClose.Block line 8
  2. instance OAI.Superstring.BlockClose.(instance at line 9) line 9
  3. instance OAI.Superstring.BlockClose.(instance at line 13) line 13
  4. abbrev OAI.Superstring.BlockClose.Block.source line 18
  5. abbrev OAI.Superstring.BlockClose.Block.target line 19
  6. abbrev OAI.Superstring.BlockClose.Block.members line 20
  7. abbrev OAI.Superstring.BlockClose.Block.word line 21
  8. abbrev OAI.Superstring.BlockClose.Block.period line 22
  9. abbrev OAI.Superstring.BlockClose.Block.reserve line 23
  10. abbrev OAI.Superstring.BlockClose.Block.internal line 24
  11. abbrev OAI.Superstring.BlockClose.Block.links line 25
  12. abbrev OAI.Superstring.BlockClose.Action line 27
  13. def OAI.Superstring.BlockClose.Covers line 29
  14. def OAI.Superstring.BlockClose.Good line 32
  15. structure OAI.Superstring.BlockClose.ValidBlock line 36
  16. def OAI.Superstring.BlockClose.singles line 50
  17. def OAI.Superstring.BlockClose.doubles line 52
  18. def OAI.Superstring.BlockClose.pool line 54
  19. theorem OAI.Superstring.BlockClose.covers_mono line 58
  20. theorem OAI.Superstring.BlockClose.pool_single line 61
  21. theorem OAI.Superstring.BlockClose.pool_link line 64
  22. theorem OAI.Superstring.BlockClose.pool_double line 67
  23. theorem OAI.Superstring.BlockClose.pool_sane line 74
  24. theorem OAI.Superstring.BlockClose.pool_complete line 92
  25. def OAI.Superstring.BlockClose.rootedCheck line 152
  26. theorem OAI.Superstring.BlockClose.rootedCheck_eq line 155
  27. def OAI.Superstring.BlockClose.lookup line 161
  28. def OAI.Superstring.BlockClose.coversCheck line 162
  29. theorem OAI.Superstring.BlockClose.coversCheck_eq line 165
  30. def OAI.Superstring.BlockClose.goodCheck line 169
  31. theorem OAI.Superstring.BlockClose.goodCheck_eq line 172
  32. def OAI.Superstring.BlockClose.select line 178
  33. def OAI.Superstring.BlockClose.remaining line 180
  34. theorem OAI.Superstring.BlockClose.select_spec line 183
  35. theorem OAI.Superstring.BlockClose.mem_remaining line 200
  36. theorem OAI.Superstring.BlockClose.remaining_budget line 205
  37. theorem OAI.Superstring.BlockClose.remaining_length line 218
  38. abbrev OAI.Superstring.BlockClose.State line 227
  39. def OAI.Superstring.BlockClose.step line 228
  40. theorem OAI.Superstring.BlockClose.step_spec line 233
  41. theorem OAI.Superstring.BitCode.Poly.flatMapFn line 259
  42. instance OAI.Superstring.BlockClose.codedState line 267
  43. instance OAI.Superstring.BlockClose.codedAction line 268
  44. instance OAI.Superstring.BlockClose.codedContextState line 269
  45. instance OAI.Superstring.BlockClose.codedContextAction line 270
  46. theorem OAI.Superstring.BlockClose.poly_singles line 272
  47. theorem OAI.Superstring.BlockClose.poly_doubles line 280
  48. theorem OAI.Superstring.BlockClose.poly_pool line 287
  49. theorem OAI.Superstring.BlockClose.poly_rootedCheck line 301
  50. theorem OAI.Superstring.BlockClose.poly_lookup line 305
  51. theorem OAI.Superstring.BlockClose.poly_coversCheck line 308
  52. theorem OAI.Superstring.BlockClose.poly_reserves line 317
  53. theorem OAI.Superstring.BlockClose.poly_goodCheck line 320
  54. theorem OAI.Superstring.BlockClose.poly_shuffle line 338
  55. theorem OAI.Superstring.BlockClose.poly_goodCheck_context line 342
  56. theorem OAI.Superstring.BlockClose.poly_filteredPool line 348
  57. theorem OAI.Superstring.BlockClose.poly_select line 351
  58. theorem OAI.Superstring.BlockClose.poly_remaining line 355
  59. theorem OAI.Superstring.BlockClose.poly_step line 360
  60. def OAI.Superstring.BlockFactory.pack line 371
  61. def OAI.Superstring.BlockFactory.individual line 375
  62. def OAI.Superstring.BlockFactory.collective line 377
  63. theorem OAI.Superstring.BlockFactory.pack_cover line 382
  64. theorem OAI.Superstring.BlockFactory.individual_valid line 393
  65. theorem OAI.Superstring.BlockFactory.collective_valid line 445