OAI/Combinatorics/KMedian/Binary/BooleanProducts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.WordTransducer.identity line 16
  2. theorem OAI.MetricKMedian.Binary.WordTransducer.identity_run line 22
  3. def OAI.MetricKMedian.Binary.WordTransducer.constant line 27
  4. theorem OAI.MetricKMedian.Binary.WordTransducer.constant_run line 33
  5. def OAI.MetricKMedian.Binary.WordTransducer.duplicate line 38
  6. theorem OAI.MetricKMedian.Binary.WordTransducer.duplicate_run line 44
  7. def OAI.MetricKMedian.Binary.WordTransducer.exchange line 52
  8. theorem OAI.MetricKMedian.Binary.WordTransducer.exchange_done line 61
  9. theorem OAI.MetricKMedian.Binary.WordTransducer.exchange_run line 69
  10. def OAI.MetricKMedian.Binary.PolyProgram.identity line 83
  11. def OAI.MetricKMedian.Binary.PolyProgram.constant line 87
  12. def OAI.MetricKMedian.Binary.PolyProgram.duplicate line 92
  13. def OAI.MetricKMedian.Binary.PolyProgram.exchange line 97
  14. def OAI.MetricKMedian.Binary.PolyProgram.second line 103
  15. def OAI.MetricKMedian.Binary.PolyProgram.product line 107
  16. def OAI.MetricKMedian.Binary.PolyProgram.fanout line 111