OAI/Combinatorics/KMedian/Binary/BooleanParallelTransducer.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Binary.ParallelTransducer line 12
  2. def OAI.MetricKMedian.Binary.ParallelTransducer.run line 23
  3. def OAI.MetricKMedian.Binary.ParallelTransducer.width line 30
  4. theorem OAI.MetricKMedian.Binary.ParallelTransducer.finish_length line 33
  5. theorem OAI.MetricKMedian.Binary.ParallelTransducer.next_length line 36
  6. theorem OAI.MetricKMedian.Binary.ParallelTransducer.run_length line 41
  7. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.Key line 52
  8. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.input line 53
  9. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.left line 54
  10. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.right line 55
  11. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.output line 56
  12. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.Label line 57
  13. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.State line 58
  14. def OAI.MetricKMedian.Binary.ParallelTransducer.store line 60
  15. theorem OAI.MetricKMedian.Binary.ParallelTransducer.store_update_input line 63
  16. theorem OAI.MetricKMedian.Binary.ParallelTransducer.store_update_left line 67
  17. theorem OAI.MetricKMedian.Binary.ParallelTransducer.store_update_right line 71
  18. theorem OAI.MetricKMedian.Binary.ParallelTransducer.store_update_output line 75
  19. def OAI.MetricKMedian.Binary.ParallelTransducer.emit line 80
  20. theorem OAI.MetricKMedian.Binary.ParallelTransducer.emit_step line 85
  21. def OAI.MetricKMedian.Binary.ParallelTransducer.emitPair line 94
  22. theorem OAI.MetricKMedian.Binary.ParallelTransducer.emitPair_step line 97
  23. def OAI.MetricKMedian.Binary.ParallelTransducer.transfer line 103
  24. def OAI.MetricKMedian.Binary.ParallelTransducer.code line 109
  25. abbrev OAI.MetricKMedian.Binary.ParallelTransducer.machine line 118
  26. def OAI.MetricKMedian.Binary.ParallelTransducer.readCfg line 128
  27. def OAI.MetricKMedian.Binary.ParallelTransducer.rightCfg line 130
  28. def OAI.MetricKMedian.Binary.ParallelTransducer.leftCfg line 132
  29. theorem OAI.MetricKMedian.Binary.ParallelTransducer.read_cons line 135
  30. theorem OAI.MetricKMedian.Binary.ParallelTransducer.read_nil line 140
  31. theorem OAI.MetricKMedian.Binary.ParallelTransducer.read_run line 145
  32. theorem OAI.MetricKMedian.Binary.ParallelTransducer.right_cons line 155
  33. theorem OAI.MetricKMedian.Binary.ParallelTransducer.right_nil line 159
  34. theorem OAI.MetricKMedian.Binary.ParallelTransducer.right_run line 163
  35. theorem OAI.MetricKMedian.Binary.ParallelTransducer.left_cons line 171
  36. theorem OAI.MetricKMedian.Binary.ParallelTransducer.left_nil line 175
  37. theorem OAI.MetricKMedian.Binary.ParallelTransducer.left_run line 184
  38. theorem OAI.MetricKMedian.Binary.ParallelTransducer.run_trace line 192
  39. def OAI.MetricKMedian.Binary.ParallelTransducer.program line 211