OAI/Combinatorics/KMedian/Hardness/Threads.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.Key line 14
  2. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.Label line 15
  3. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.State line 16
  4. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.Alphabet line 18
  5. instance OAI.MetricKMedian.Complexity.FiniteComposition.Thread.alphabetFinite line 22
  6. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.source line 26
  7. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.buffer line 27
  8. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.reading line 28
  9. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.loading line 29
  10. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.emitting line 30
  11. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.draining line 31
  12. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.store line 33
  13. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.store_local line 39
  14. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.store_source line 41
  15. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.store_buffer line 43
  16. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.slot line 46
  17. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.slot_nil line 48
  18. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.slot_self line 53
  19. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.slot_update line 54
  20. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.store_update_local line 60
  21. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.store_update_source line 68
  22. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.store_update_buffer line 73
  23. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.body line 79
  24. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.body_stmt line 98
  25. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.clean line 102
  26. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.readCode line 104
  27. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.loadCode line 112
  28. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.emitCode line 119
  29. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.drainCode line 127
  30. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.code line 134
  31. abbrev OAI.MetricKMedian.Complexity.FiniteComposition.Thread.machine line 138
  32. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.code_body line 151
  33. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.readCfg line 154
  34. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.loadCfg line 157
  35. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.emitCfg line 160
  36. def OAI.MetricKMedian.Complexity.FiniteComposition.Thread.drainCfg line 163
  37. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.read_cons line 166
  38. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.read_nil line 171
  39. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.read_run line 176
  40. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.load_cons line 184
  41. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.load_nil line 189
  42. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.load_run line 194
  43. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.emit_cons line 203
  44. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.emit_nil line 208
  45. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.emit_run line 213
  46. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.drain_cons line 222
  47. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.drain_nil line 227
  48. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.drain_run line 238
  49. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.body_final line 246
  50. theorem OAI.MetricKMedian.Complexity.FiniteComposition.Thread.run line 248
  51. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.thread line 276
  52. def OAI.MetricKMedian.Complexity.FiniteComposition.PolyProgram.withInput line 291
  53. theorem OAI.MetricKMedian.Complexity.FinitePolyTime.withInput line 301