OAI/Combinatorics/KMedian/Binary/BooleanEncoding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.quote line 12
  2. theorem OAI.MetricKMedian.Binary.quote_length line 16
  3. def OAI.MetricKMedian.Binary.encodePair line 21
  4. theorem OAI.MetricKMedian.Binary.encodePair_length line 24
  5. def OAI.MetricKMedian.Binary.WordTransducer.quoting line 30
  6. theorem OAI.MetricKMedian.Binary.WordTransducer.quoting_run line 36
  7. def OAI.MetricKMedian.Binary.WordTransducer.projecting line 41
  8. theorem OAI.MetricKMedian.Binary.WordTransducer.projecting_done line 50
  9. theorem OAI.MetricKMedian.Binary.WordTransducer.projecting_pair line 59
  10. def OAI.MetricKMedian.Binary.PolyProgram.of_word line 72
  11. def OAI.MetricKMedian.Binary.PolyProgram.quote line 79
  12. def OAI.MetricKMedian.Binary.PolyProgram.fst line 82
  13. def OAI.MetricKMedian.Binary.PolyProgram.snd line 87