OAI/Combinatorics/KMedian/Binary/BinaryListFold.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.ListFold.enc line 15
  2. def OAI.MetricKMedian.Binary.ListFold.body line 16
  3. def OAI.MetricKMedian.Binary.ListFold.result line 18
  4. def OAI.MetricKMedian.Binary.ListFold.program line 20
  5. theorem OAI.MetricKMedian.Binary.ListFold.run line 31
  6. def OAI.MetricKMedian.Binary.ListFold.loop line 46
  7. theorem OAI.MetricKMedian.Binary.ListFold.linear_height line 64
  8. def OAI.MetricKMedian.Binary.ListFold.linearLoop line 76
  9. def OAI.MetricKMedian.Binary.PolyProgram.listFold line 89
  10. def OAI.MetricKMedian.Binary.PolyProgram.listFoldLinear line 94