OAI/Combinatorics/KMedian/Binary/BinarySubtraction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.Word.borrowBit line 13
  2. theorem OAI.MetricKMedian.Binary.Word.fullSubtract line 14
  3. def OAI.MetricKMedian.Binary.Word.sub line 18
  4. theorem OAI.MetricKMedian.Binary.Word.sub_step line 28
  5. theorem OAI.MetricKMedian.Binary.Word.value_lt line 34
  6. theorem OAI.MetricKMedian.Binary.Word.value_sub line 42
  7. theorem OAI.MetricKMedian.Binary.Word.sub_borrow line 69
  8. theorem OAI.MetricKMedian.Binary.Word.sub_clamp line 80
  9. def OAI.MetricKMedian.Binary.SubtractionLoop.next line 96
  10. def OAI.MetricKMedian.Binary.SubtractionLoop.finish line 99
  11. def OAI.MetricKMedian.Binary.SubtractionLoop.body line 100
  12. def OAI.MetricKMedian.Binary.SubtractionLoop.result line 101
  13. def OAI.MetricKMedian.Binary.SubtractionLoop.program line 105
  14. theorem OAI.MetricKMedian.Binary.SubtractionLoop.next_result line 123
  15. theorem OAI.MetricKMedian.Binary.SubtractionLoop.next_size line 128
  16. theorem OAI.MetricKMedian.Binary.SubtractionLoop.run line 133
  17. def OAI.MetricKMedian.Binary.SubtractionLoop.loop line 152
  18. def OAI.MetricKMedian.Binary.PolyProgram.subWords line 161
  19. def OAI.MetricKMedian.Binary.PolyProgram.natLT line 166
  20. def OAI.MetricKMedian.Binary.PolyProgram.natSub line 170