OAI/Computability/Superstring/WalkCode.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Superstring.WalkCode.Walk line 9
  2. def OAI.Superstring.WalkCode.Edge line 11
  3. def OAI.Superstring.WalkCode.Valid line 14
  4. def OAI.Superstring.WalkCode.cost line 17
  5. def OAI.Superstring.WalkCode.join line 20
  6. def OAI.Superstring.WalkCode.Visits line 22
  7. def OAI.Superstring.WalkCode.Path.points line 26
  8. theorem OAI.Superstring.WalkCode.join_cons line 34
  9. theorem OAI.Superstring.WalkCode.cost_nil line 37
  10. theorem OAI.Superstring.WalkCode.cost_singleton line 38
  11. theorem OAI.Superstring.WalkCode.cost_cons_cons line 39
  12. theorem OAI.Superstring.WalkCode.cost_join line 44
  13. theorem OAI.Superstring.WalkCode.cost_eq_edges line 69
  14. theorem OAI.Superstring.WalkCode.valid_nil line 72
  15. theorem OAI.Superstring.WalkCode.valid_step line 75
  16. theorem OAI.Superstring.WalkCode.edge_path line 80
  17. theorem OAI.Superstring.WalkCode.realize line 89
  18. theorem OAI.Superstring.WalkCode.mem_join line 118
  19. theorem OAI.Superstring.WalkCode.valid_join line 137
  20. theorem OAI.Superstring.WalkCode.head_join line 160
  21. theorem OAI.Superstring.WalkCode.last_join line 166
  22. theorem OAI.Superstring.WalkCode.points_spec line 182
  23. theorem OAI.Superstring.WalkCode.length_cost line 207
  24. theorem OAI.Superstring.WalkCode.poly_join line 229
  25. theorem OAI.Superstring.WalkCode.poly_zip line 233
  26. theorem OAI.Superstring.WalkCode.poly_cost line 254
  27. def OAI.Superstring.WalkCode.delete line 271
  28. def OAI.Superstring.WalkCode.append line 274
  29. def OAI.Superstring.WalkCode.gap line 277
  30. theorem OAI.Superstring.WalkCode.delete_nil line 279
  31. theorem OAI.Superstring.WalkCode.delete_cons line 280
  32. theorem OAI.Superstring.WalkCode.append_nil line 285
  33. theorem OAI.Superstring.WalkCode.append_cons line 286
  34. theorem OAI.Superstring.WalkCode.gap_nil line 292
  35. theorem OAI.Superstring.WalkCode.gap_cons line 293
  36. theorem OAI.Superstring.WalkCode.points_copy line 296
  37. theorem OAI.Superstring.WalkCode.points_delete line 300
  38. theorem OAI.Superstring.WalkCode.points_append line 317
  39. theorem OAI.Superstring.WalkCode.points_gap line 334
  40. theorem OAI.Superstring.WalkCode.delete_spec line 341
  41. theorem OAI.Superstring.WalkCode.append_spec line 349
  42. theorem OAI.Superstring.WalkCode.gap_spec line 357
  43. theorem OAI.Superstring.WalkCode.mem_delete line 365
  44. theorem OAI.Superstring.WalkCode.mem_append line 369
  45. theorem OAI.Superstring.WalkCode.poly_delete line 375
  46. theorem OAI.Superstring.WalkCode.poly_append line 381
  47. theorem OAI.Superstring.WalkCode.poly_gap line 387
  48. def OAI.Superstring.WalkCode.Runs line 402
  49. theorem OAI.Superstring.WalkCode.runs_join line 405
  50. theorem OAI.Superstring.WalkCode.runs_points line 410
  51. theorem OAI.Superstring.WalkCode.take_drop_join line 415
  52. theorem OAI.Superstring.WalkCode.split_runs line 420
  53. def OAI.Superstring.WalkCode.rotate line 436
  54. theorem OAI.Superstring.WalkCode.rotate_spec line 438
  55. def OAI.Superstring.WalkCode.insertAt line 456
  56. theorem OAI.Superstring.WalkCode.insertAt_spec line 459
  57. theorem OAI.Superstring.WalkCode.poly_rotate line 480
  58. theorem OAI.Superstring.WalkCode.poly_insertAt line 483
  59. def OAI.Superstring.WalkCode.locate line 495
  60. def OAI.Superstring.WalkCode.meeting line 498
  61. def OAI.Superstring.WalkCode.splice line 501
  62. theorem OAI.Superstring.WalkCode.locate_spec line 506
  63. theorem OAI.Superstring.WalkCode.meeting_spec line 514
  64. theorem OAI.Superstring.WalkCode.splice_spec line 523
  65. theorem OAI.Superstring.WalkCode.poly_locate line 538
  66. theorem OAI.Superstring.WalkCode.poly_meeting line 544
  67. theorem OAI.Superstring.WalkCode.poly_splice line 550
  68. theorem OAI.Superstring.WalkCode.size_join line 558
  69. theorem OAI.Superstring.WalkCode.size_rotate line 565
  70. theorem OAI.Superstring.WalkCode.size_insertAt line 573
  71. theorem OAI.Superstring.WalkCode.size_splice line 584
  72. def OAI.Superstring.WalkCode.fill line 587
  73. theorem OAI.Superstring.WalkCode.poly_fill line 588
  74. theorem OAI.Superstring.WalkCode.fill_spec line 597