OAI/Combinatorics/KMedian/Binary/BinaryAddition.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.Word.sumBit line 16
  2. def OAI.MetricKMedian.Binary.Word.carryBit line 17
  3. theorem OAI.MetricKMedian.Binary.Word.fullAdder line 19
  4. def OAI.MetricKMedian.Binary.Word.add line 23
  5. theorem OAI.MetricKMedian.Binary.Word.add_step line 29
  6. theorem OAI.MetricKMedian.Binary.Word.value_add line 36
  7. abbrev OAI.MetricKMedian.Binary.AdditionLoop.S line 56
  8. abbrev OAI.MetricKMedian.Binary.AdditionLoop.ec line 57
  9. abbrev OAI.MetricKMedian.Binary.AdditionLoop.ey line 58
  10. abbrev OAI.MetricKMedian.Binary.AdditionLoop.enc line 59
  11. def OAI.MetricKMedian.Binary.AdditionLoop.empty line 60
  12. def OAI.MetricKMedian.Binary.AdditionLoop.next line 61
  13. def OAI.MetricKMedian.Binary.AdditionLoop.finish line 64
  14. def OAI.MetricKMedian.Binary.AdditionLoop.body line 65
  15. def OAI.MetricKMedian.Binary.AdditionLoop.result line 66
  16. theorem OAI.MetricKMedian.Binary.AdditionLoop.enc_length line 68
  17. def OAI.MetricKMedian.Binary.AdditionLoop.program line 72
  18. theorem OAI.MetricKMedian.Binary.AdditionLoop.shorten line 90
  19. theorem OAI.MetricKMedian.Binary.AdditionLoop.next_result line 96
  20. theorem OAI.MetricKMedian.Binary.AdditionLoop.next_size line 101
  21. theorem OAI.MetricKMedian.Binary.AdditionLoop.run line 106
  22. def OAI.MetricKMedian.Binary.AdditionLoop.loop line 125
  23. def OAI.MetricKMedian.Binary.PolyProgram.addWords line 135
  24. def OAI.MetricKMedian.Binary.PolyProgram.natAdd line 140