OAI/Computability/Superstring/CollectionCode.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Superstring.CollectionCode.Env line 8
  2. def OAI.Superstring.CollectionCode.data line 9
  3. def OAI.Superstring.CollectionCode.gs line 10
  4. def OAI.Superstring.CollectionCode.stride line 11
  5. def OAI.Superstring.CollectionCode.owner line 12
  6. def OAI.Superstring.CollectionCode.idx line 13
  7. def OAI.Superstring.CollectionCode.layer line 14
  8. def OAI.Superstring.CollectionCode.book line 16
  9. def OAI.Superstring.CollectionCode.ids line 17
  10. def OAI.Superstring.CollectionCode.per line 19
  11. def OAI.Superstring.CollectionCode.phase line 20
  12. def OAI.Superstring.CollectionCode.contents line 21
  13. def OAI.Superstring.CollectionCode.ls line 22
  14. theorem OAI.Superstring.CollectionCode.owner_encode line 25
  15. theorem OAI.Superstring.CollectionCode.idx_encode line 30
  16. theorem OAI.Superstring.CollectionCode.lookup_encode line 35
  17. theorem OAI.Superstring.CollectionCode.ls_encode line 42
  18. theorem OAI.Superstring.CollectionCode.encode_injective line 49
  19. theorem OAI.Superstring.CollectionCode.poly_data line 56
  20. theorem OAI.Superstring.CollectionCode.poly_owner line 60
  21. theorem OAI.Superstring.CollectionCode.poly_idx line 62
  22. theorem OAI.Superstring.CollectionCode.poly_layer line 64
  23. theorem OAI.Superstring.CollectionCode.poly_book line 66
  24. theorem OAI.Superstring.CollectionCode.poly_ids line 70
  25. theorem OAI.Superstring.CollectionCode.poly_per line 77
  26. theorem OAI.Superstring.CollectionCode.poly_contents line 79
  27. theorem OAI.Superstring.CollectionCode.poly_phase line 84
  28. def OAI.Superstring.CollectionCode.rank line 95
  29. structure OAI.Superstring.CollectionCode.Model line 99
  30. def OAI.Superstring.CollectionCode.Model.encode line 113
  31. theorem OAI.Superstring.CollectionCode.Model.local_lt line 116
  32. theorem OAI.Superstring.CollectionCode.Model.owner_eq line 117
  33. theorem OAI.Superstring.CollectionCode.Model.idx_eq line 119
  34. theorem OAI.Superstring.CollectionCode.Model.encode_inj line 121
  35. theorem OAI.Superstring.CollectionCode.Model.id_mem line 130
  36. theorem OAI.Superstring.CollectionCode.Model.mem_ids line 136
  37. theorem OAI.Superstring.CollectionCode.Model.book_rep line 147
  38. theorem OAI.Superstring.CollectionCode.Model.content_iff line 152
  39. theorem OAI.Superstring.CollectionCode.Model.per_eq line 156
  40. theorem OAI.Superstring.CollectionCode.Model.text_eq line 158
  41. theorem OAI.Superstring.CollectionCode.Model.rank_eq line 160
  42. def OAI.Superstring.CollectionCode.Model.natIndex line 163
  43. def OAI.Superstring.CollectionCode.Model.natLayer line 165
  44. theorem OAI.Superstring.CollectionCode.Model.natIndex_val line 166
  45. theorem OAI.Superstring.CollectionCode.Model.natLayer_fin line 168
  46. theorem OAI.Superstring.CollectionCode.Model.nat_rep line 172
  47. theorem OAI.Superstring.CollectionCode.Model.nat_order line 175
  48. theorem OAI.Superstring.CollectionCode.Model.rank_shift line 181
  49. def OAI.Superstring.CollectionCode.hard line 196
  50. theorem OAI.Superstring.CollectionCode.Model.hard_spec line 204
  51. theorem OAI.Superstring.BitCode.Poly.zip line 299
  52. abbrev OAI.Superstring.WindowCode.Window line 323
  53. def OAI.Superstring.WindowCode.ordered line 324
  54. def OAI.Superstring.WindowCode.routeList line 325
  55. theorem OAI.Superstring.WindowCode.routeList_nil line 329
  56. theorem OAI.Superstring.WindowCode.routeList_cons line 331
  57. theorem OAI.Superstring.WindowCode.routeList_realizes line 342
  58. theorem OAI.Superstring.WindowCode.poly_routeList line 384