OAI/Combinatorics/KMedian/Binary/BinaryDivision.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.DivisionLoop.qstep line 14
  2. def OAI.MetricKMedian.Binary.DivisionLoop.rstep line 15
  3. theorem OAI.MetricKMedian.Binary.DivisionLoop.step_total line 17
  4. theorem OAI.MetricKMedian.Binary.DivisionLoop.step_remainder line 29
  5. def OAI.MetricKMedian.Binary.DivisionLoop.eval line 37
  6. theorem OAI.MetricKMedian.Binary.DivisionLoop.eval_spec line 41
  7. abbrev OAI.MetricKMedian.Binary.DivisionLoop.S line 56
  8. abbrev OAI.MetricKMedian.Binary.DivisionLoop.eqr line 57
  9. abbrev OAI.MetricKMedian.Binary.DivisionLoop.edqr line 58
  10. abbrev OAI.MetricKMedian.Binary.DivisionLoop.enc line 59
  11. def OAI.MetricKMedian.Binary.DivisionLoop.next line 60
  12. def OAI.MetricKMedian.Binary.DivisionLoop.body line 63
  13. def OAI.MetricKMedian.Binary.DivisionLoop.result line 64
  14. def OAI.MetricKMedian.Binary.DivisionLoop.potential line 65
  15. theorem OAI.MetricKMedian.Binary.DivisionLoop.enc_length line 67
  16. theorem OAI.MetricKMedian.Binary.DivisionLoop.total_le_length line 72
  17. theorem OAI.MetricKMedian.Binary.DivisionLoop.length_le_total line 76
  18. theorem OAI.MetricKMedian.Binary.DivisionLoop.next_potential line 80
  19. theorem OAI.MetricKMedian.Binary.DivisionLoop.next_result line 94
  20. def OAI.MetricKMedian.Binary.DivisionLoop.program line 100
  21. theorem OAI.MetricKMedian.Binary.DivisionLoop.run line 118
  22. def OAI.MetricKMedian.Binary.DivisionLoop.loop line 133
  23. def OAI.MetricKMedian.Binary.PolyProgram.natDivMod line 145
  24. def OAI.MetricKMedian.Binary.PolyProgram.natDiv line 168
  25. def OAI.MetricKMedian.Binary.PolyProgram.natMod line 170