OAI/Combinatorics/KMedian/Binary/BinaryLists.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.encodeList line 15
  2. theorem OAI.MetricKMedian.Binary.EncodedList.nil line 21
  3. theorem OAI.MetricKMedian.Binary.EncodedList.cons line 22
  4. theorem OAI.MetricKMedian.Binary.EncodedList.cons_length line 23
  5. theorem OAI.MetricKMedian.Binary.EncodedList.length_le line 25
  6. theorem OAI.MetricKMedian.Binary.EncodedList.isEmpty line 29
  7. theorem OAI.MetricKMedian.Binary.EncodedList.append line 38
  8. theorem OAI.MetricKMedian.Binary.EncodedList.reverse_length line 42
  9. theorem OAI.MetricKMedian.Binary.EncodedList.member_length line 48
  10. theorem OAI.MetricKMedian.Binary.EncodedList.length_bound line 57
  11. def OAI.MetricKMedian.Binary.PolyProgram.listIsEmpty line 70
  12. def OAI.MetricKMedian.Binary.PolyProgram.listUncons line 73
  13. def OAI.MetricKMedian.Binary.PolyProgram.listHead line 82
  14. def OAI.MetricKMedian.Binary.PolyProgram.listTail line 84
  15. def OAI.MetricKMedian.Binary.PolyProgram.listCons line 86
  16. abbrev OAI.MetricKMedian.Binary.ListReverse.enc line 92
  17. def OAI.MetricKMedian.Binary.ListReverse.body line 93
  18. def OAI.MetricKMedian.Binary.ListReverse.result line 95
  19. def OAI.MetricKMedian.Binary.ListReverse.program line 97
  20. theorem OAI.MetricKMedian.Binary.ListReverse.run line 107
  21. def OAI.MetricKMedian.Binary.ListReverse.loop line 123
  22. def OAI.MetricKMedian.Binary.PolyProgram.listReverse line 134
  23. def OAI.MetricKMedian.Binary.PolyProgram.listAppend line 137