OAI/Combinatorics/KMedian/Binary/BooleanListPrimitives.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.encodeBool line 14
  2. def OAI.MetricKMedian.Binary.WordTransducer.emptyTest line 18
  3. theorem OAI.MetricKMedian.Binary.WordTransducer.emptyTest_run line 24
  4. def OAI.MetricKMedian.Binary.WordTransducer.head line 33
  5. theorem OAI.MetricKMedian.Binary.WordTransducer.head_run line 39
  6. def OAI.MetricKMedian.Binary.WordTransducer.tail line 48
  7. theorem OAI.MetricKMedian.Binary.WordTransducer.tail_run_false line 54
  8. theorem OAI.MetricKMedian.Binary.WordTransducer.tail_run line 59
  9. abbrev OAI.MetricKMedian.Binary.WordTransducer.prepend line 64
  10. theorem OAI.MetricKMedian.Binary.WordTransducer.prepend_done line 70
  11. theorem OAI.MetricKMedian.Binary.WordTransducer.prepend_run line 77
  12. def OAI.MetricKMedian.Binary.WordTransducer.prependWord line 82
  13. theorem OAI.MetricKMedian.Binary.WordTransducer.prefix_done line 88
  14. theorem OAI.MetricKMedian.Binary.WordTransducer.prefix_run line 93
  15. def OAI.MetricKMedian.Binary.WordTransducer.select line 100
  16. theorem OAI.MetricKMedian.Binary.WordTransducer.select_done line 111
  17. theorem OAI.MetricKMedian.Binary.WordTransducer.select_pair line 120
  18. theorem OAI.MetricKMedian.Binary.WordTransducer.select_run line 129
  19. def OAI.MetricKMedian.Binary.PolyProgram.isEmpty line 138
  20. def OAI.MetricKMedian.Binary.PolyProgram.head line 142
  21. def OAI.MetricKMedian.Binary.PolyProgram.tail line 146
  22. def OAI.MetricKMedian.Binary.PolyProgram.cons line 150
  23. def OAI.MetricKMedian.Binary.PolyProgram.prependWord line 154
  24. def OAI.MetricKMedian.Binary.PolyProgram.injectLeft line 158
  25. def OAI.MetricKMedian.Binary.PolyProgram.injectRight line 162
  26. def OAI.MetricKMedian.Binary.PolyProgram.select line 166
  27. def OAI.MetricKMedian.Binary.PolyProgram.ite line 173