OAI/Combinatorics/KMedian/Binary/BinaryMultiplication.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.MultiplicationLoop.S line 14
  2. abbrev OAI.MetricKMedian.Binary.MultiplicationLoop.ey line 15
  3. abbrev OAI.MetricKMedian.Binary.MultiplicationLoop.enc line 16
  4. def OAI.MetricKMedian.Binary.MultiplicationLoop.next line 17
  5. def OAI.MetricKMedian.Binary.MultiplicationLoop.body line 18
  6. def OAI.MetricKMedian.Binary.MultiplicationLoop.result line 19
  7. def OAI.MetricKMedian.Binary.MultiplicationLoop.potential line 20
  8. theorem OAI.MetricKMedian.Binary.MultiplicationLoop.enc_length line 22
  9. theorem OAI.MetricKMedian.Binary.MultiplicationLoop.potential_le_length line 26
  10. theorem OAI.MetricKMedian.Binary.MultiplicationLoop.length_le_potential line 30
  11. theorem OAI.MetricKMedian.Binary.MultiplicationLoop.next_potential line 34
  12. theorem OAI.MetricKMedian.Binary.MultiplicationLoop.next_result line 41
  13. def OAI.MetricKMedian.Binary.MultiplicationLoop.program line 52
  14. theorem OAI.MetricKMedian.Binary.MultiplicationLoop.run line 67
  15. def OAI.MetricKMedian.Binary.MultiplicationLoop.loop line 83
  16. def OAI.MetricKMedian.Binary.PolyProgram.natMul line 93