OAI/Combinatorics/KMedian/Hardness/Composition.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Complexity.FiniteComposition.Machine line 13
  2. theorem OAI.MetricKMedian.Complexity.FiniteComposition.cfg_ext line 33
  3. def OAI.MetricKMedian.Complexity.FiniteComposition.Machine.tm line 44
  4. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Machine.Cfg line 55
  5. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Machine.step line 56
  6. def OAI.MetricKMedian.Complexity.FiniteComposition.Machine.single line 58
  7. def OAI.MetricKMedian.Complexity.FiniteComposition.Machine.initialCfg line 61
  8. def OAI.MetricKMedian.Complexity.FiniteComposition.Machine.finalCfg line 64
  9. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.init_eq line 67
  10. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.halt_eq line 77
  11. structure OAI.MetricKMedian.Complexity.FiniteComposition.Embedding line 89
  12. def OAI.MetricKMedian.Complexity.FiniteComposition.Embedding.stmt line 112
  13. def OAI.MetricKMedian.Complexity.FiniteComposition.Embedding.cfg line 123
  14. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Embedding.head_map_inverse line 126
  15. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Embedding.stepAux_stmt line 129
  16. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Embedding.step_cfg line 154
  17. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Embedding.trace line 167
  18. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Compose.Key line 176
  19. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Compose.Label line 177
  20. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Compose.State line 178
  21. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.Alphabet line 180
  22. instance OAI.MetricKMedian.Complexity.FiniteComposition.Compose.alphabetFinite line 185
  23. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Compose.phaseLabel line 191
  24. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Compose.auxiliary line 192
  25. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.left line 194
  26. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.right line 221
  27. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.source line 251
  28. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.target line 252
  29. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.source_ne_target line 254
  30. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.sourceAlphabet line 257
  31. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.targetAlphabet line 261
  32. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.following line 265
  33. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.clean line 268
  34. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.transfer line 270
  35. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.code line 277
  36. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Compose.machine line 282
  37. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.code_left line 295
  38. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.code_right line 298
  39. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.initial_left line 301
  40. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.final_right line 312
  41. def OAI.MetricKMedian.Complexity.FiniteComposition.twoStacks line 327
  42. theorem OAI.MetricKMedian.Complexity.FiniteComposition.twoStacks_source line 331
  43. theorem OAI.MetricKMedian.Complexity.FiniteComposition.twoStacks_target line 336
  44. theorem OAI.MetricKMedian.Complexity.FiniteComposition.twoStacks_move line 340
  45. theorem OAI.MetricKMedian.Complexity.FiniteComposition.twoStacks_pop_empty line 351
  46. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.transferCfg line 362
  47. def OAI.MetricKMedian.Complexity.FiniteComposition.Compose.boundaryCfg line 367
  48. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.transfer_cons line 371
  49. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.transfer_run line 386
  50. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.transfer_empty line 396
  51. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.left_final line 408
  52. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.boundary_false line 425
  53. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.boundary_true line 448
  54. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.transfer_all line 466
  55. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Compose.run line 480
  56. def OAI.MetricKMedian.Complexity.FiniteComposition.Machine.pushes line 496
  57. def OAI.MetricKMedian.Complexity.FiniteComposition.Machine.volume line 505
  58. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.volume_update line 509
  59. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.stepAux_volume line 523
  60. def OAI.MetricKMedian.Complexity.FiniteComposition.Machine.growth line 550
  61. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.step_volume line 552
  62. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.trace_volume line 564
  63. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.volume_single line 574
  64. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.initial_volume line 579
  65. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.final_volume line 583
  66. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Machine.output_length line 587
  67. structure OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram line 594
  68. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.stock line 604
  69. theorem OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.finite_work line 620
  70. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.stockMachine line 623
  71. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.ofStock line 642
  72. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.sizeBound line 652
  73. theorem OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.length_bound line 655
  74. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.compTime line 663
  75. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.comp line 666
  76. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.congr line 680
  77. theorem OAI.MetricKMedian.Complexity.FinitePolyTime.comp line 692