OAI/Computability/Superstring/Computable.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.Computable.nth line 9
  2. theorem OAI.Superstring.Computable.poly_nth line 11
  3. def OAI.Superstring.Computable.occurs line 16

    Source documentation

    All indices and loop counters below are explicitly represented unary data.

    def occurs (T s : List α) (j : ℕ) : Bool :=
…
  4. def OAI.Superstring.Computable.infixB line 19
  5. def OAI.Superstring.Computable.text line 22
  6. def OAI.Superstring.Computable.matchesB line 25
  7. def OAI.Superstring.Computable.blocks line 28
  8. def OAI.Superstring.Computable.coefficient line 36
  9. theorem OAI.Superstring.Computable.poly_occurs line 40
  10. theorem OAI.Superstring.Computable.poly_infix line 44
  11. theorem OAI.Superstring.Computable.poly_text line 49
  12. theorem OAI.Superstring.Computable.poly_matches line 53
  13. theorem OAI.Superstring.Computable.poly_blocks line 57
  14. theorem OAI.Superstring.Computable.poly_coefficient line 69
  15. theorem OAI.Superstring.Computable.occurs_eq line 77
  16. theorem OAI.Superstring.Computable.infix_eq line 91
  17. theorem OAI.Superstring.Computable.text_eq line 101
  18. theorem OAI.Superstring.Computable.matches_eq line 105
  19. theorem OAI.Superstring.Computable.nth_eq_iff line 124
  20. theorem OAI.Superstring.Computable.blocks_eq line 128
  21. theorem OAI.Superstring.Computable.length_filter_range_card line 166
  22. theorem OAI.Superstring.Computable.coefficient_eq line 183
  23. def OAI.Superstring.Computable.subwords line 188
  24. def OAI.Superstring.Computable.vertices line 192
  25. def OAI.Superstring.Computable.required line 194
  26. def OAI.Superstring.Computable.alphabet line 197
  27. theorem OAI.Superstring.Computable.mem_subwords line 200
  28. theorem OAI.Superstring.Computable.vertices_eq line 213
  29. theorem OAI.Superstring.Computable.required_eq line 226
  30. theorem OAI.Superstring.Computable.alphabet_eq line 245
  31. theorem OAI.Superstring.Computable.poly_subwords line 255
  32. theorem OAI.Superstring.Computable.poly_vertices line 263
  33. theorem OAI.Superstring.Computable.poly_required line 271
  34. theorem OAI.Superstring.Computable.poly_alphabet line 281
  35. abbrev OAI.Superstring.Computable.DataCode line 291
  36. abbrev OAI.Superstring.Computable.Table line 292
  37. def OAI.Superstring.Computable.dataCode line 294
  38. def OAI.Superstring.Computable.decodeData line 296
  39. theorem OAI.Superstring.Computable.decode_dataCode line 299
  40. def OAI.Superstring.Computable.lookup line 303

    Source documentation

    A finite association table; every stage is materialized before the next.

    def lookup (t : Table α) (w : List α) : ℕ :=
…

    Mentions: OAI.Superstring.Computable.Table

  41. theorem OAI.Superstring.Computable.lookup_map line 306
  42. theorem OAI.Superstring.Computable.sum_map_finset line 318
  43. theorem OAI.Superstring.Computable.max_map_finset line 327
  44. def OAI.Superstring.Computable.blocking line 339
  45. def OAI.Superstring.Computable.rule line 342
  46. def OAI.Superstring.Computable.rulesFor line 348
  47. def OAI.Superstring.Computable.rules line 352
  48. def OAI.Superstring.Computable.left line 355
  49. def OAI.Superstring.Computable.right line 358
  50. def OAI.Superstring.Computable.step line 361
  51. def OAI.Superstring.Computable.tableStep line 367
  52. theorem OAI.Superstring.Computable.blocking_eq line 369
  53. theorem OAI.Superstring.Computable.rule_eq line 374
  54. theorem OAI.Superstring.Computable.rules_eq line 383
  55. theorem OAI.Superstring.Computable.step_eq line 388
  56. theorem OAI.Superstring.Computable.poly_dataCode line 407
  57. theorem OAI.Superstring.Computable.poly_lookup line 412
  58. theorem OAI.Superstring.Computable.poly_blocking line 419
  59. theorem OAI.Superstring.Computable.poly_rule line 428
  60. theorem OAI.Superstring.Computable.poly_rulesFor line 434
  61. theorem OAI.Superstring.Computable.poly_rules line 447
  62. theorem OAI.Superstring.Computable.poly_left line 455
  63. theorem OAI.Superstring.Computable.poly_right line 464
  64. theorem OAI.Superstring.Computable.poly_step line 472
  65. theorem OAI.Superstring.Computable.poly_tableStep line 477