OAI/Combinatorics/KMedian/Binary/BooleanThread.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.Thread.Key line 14
  2. abbrev OAI.MetricKMedian.Binary.Thread.Label line 15
  3. abbrev OAI.MetricKMedian.Binary.Thread.State line 16
  4. abbrev OAI.MetricKMedian.Binary.Thread.source line 17
  5. abbrev OAI.MetricKMedian.Binary.Thread.buffer line 18
  6. abbrev OAI.MetricKMedian.Binary.Thread.reading line 19
  7. abbrev OAI.MetricKMedian.Binary.Thread.loading line 20
  8. abbrev OAI.MetricKMedian.Binary.Thread.emitting line 21
  9. abbrev OAI.MetricKMedian.Binary.Thread.draining line 22
  10. def OAI.MetricKMedian.Binary.Thread.store line 24
  11. theorem OAI.MetricKMedian.Binary.Thread.store_local line 30
  12. theorem OAI.MetricKMedian.Binary.Thread.store_source line 32
  13. theorem OAI.MetricKMedian.Binary.Thread.store_buffer line 34
  14. def OAI.MetricKMedian.Binary.Thread.slot line 37
  15. theorem OAI.MetricKMedian.Binary.Thread.slot_nil line 39
  16. theorem OAI.MetricKMedian.Binary.Thread.slot_self line 40
  17. theorem OAI.MetricKMedian.Binary.Thread.slot_update line 41
  18. theorem OAI.MetricKMedian.Binary.Thread.store_update_local line 45
  19. theorem OAI.MetricKMedian.Binary.Thread.store_update_source line 51
  20. theorem OAI.MetricKMedian.Binary.Thread.store_update_buffer line 56
  21. def OAI.MetricKMedian.Binary.Thread.body line 62
  22. theorem OAI.MetricKMedian.Binary.Thread.body_stmt line 77
  23. def OAI.MetricKMedian.Binary.Thread.clean line 81
  24. def OAI.MetricKMedian.Binary.Thread.readCode line 83
  25. def OAI.MetricKMedian.Binary.Thread.loadCode line 91
  26. def OAI.MetricKMedian.Binary.Thread.emitCode line 98
  27. def OAI.MetricKMedian.Binary.Thread.drainCode line 106
  28. def OAI.MetricKMedian.Binary.Thread.code line 113
  29. abbrev OAI.MetricKMedian.Binary.Thread.machine line 117
  30. theorem OAI.MetricKMedian.Binary.Thread.code_body line 127
  31. def OAI.MetricKMedian.Binary.Thread.readCfg line 130
  32. def OAI.MetricKMedian.Binary.Thread.loadCfg line 133
  33. def OAI.MetricKMedian.Binary.Thread.emitCfg line 136
  34. def OAI.MetricKMedian.Binary.Thread.drainCfg line 139
  35. theorem OAI.MetricKMedian.Binary.Thread.read_cons line 142
  36. theorem OAI.MetricKMedian.Binary.Thread.read_nil line 147
  37. theorem OAI.MetricKMedian.Binary.Thread.read_run line 152
  38. theorem OAI.MetricKMedian.Binary.Thread.load_cons line 160
  39. theorem OAI.MetricKMedian.Binary.Thread.load_nil line 165
  40. theorem OAI.MetricKMedian.Binary.Thread.load_run line 171
  41. theorem OAI.MetricKMedian.Binary.Thread.emit_cons line 180
  42. theorem OAI.MetricKMedian.Binary.Thread.emit_nil line 185
  43. theorem OAI.MetricKMedian.Binary.Thread.emit_run line 190
  44. theorem OAI.MetricKMedian.Binary.Thread.drain_cons line 199
  45. theorem OAI.MetricKMedian.Binary.Thread.drain_nil line 204
  46. theorem OAI.MetricKMedian.Binary.Thread.drain_run line 214
  47. theorem OAI.MetricKMedian.Binary.Thread.body_final line 222
  48. theorem OAI.MetricKMedian.Binary.Thread.run line 224
  49. def OAI.MetricKMedian.Binary.PolyProgram.thread line 253