OAI/Combinatorics/KMedian/Binary/BinaryGCD.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Binary.NatBinary.mod_length_lt line 13
  2. abbrev OAI.MetricKMedian.Binary.GCDLoop.S line 37
  3. abbrev OAI.MetricKMedian.Binary.GCDLoop.enc line 38
  4. def OAI.MetricKMedian.Binary.GCDLoop.next line 39
  5. def OAI.MetricKMedian.Binary.GCDLoop.body line 40
  6. def OAI.MetricKMedian.Binary.GCDLoop.result line 41
  7. def OAI.MetricKMedian.Binary.GCDLoop.potential line 42
  8. theorem OAI.MetricKMedian.Binary.GCDLoop.enc_length line 44
  9. theorem OAI.MetricKMedian.Binary.GCDLoop.length_le_potential line 46
  10. theorem OAI.MetricKMedian.Binary.GCDLoop.potential_le_length line 48
  11. theorem OAI.MetricKMedian.Binary.GCDLoop.next_result line 51
  12. theorem OAI.MetricKMedian.Binary.GCDLoop.next_potential line 57
  13. theorem OAI.MetricKMedian.Binary.GCDLoop.next_potential_lt line 62
  14. def OAI.MetricKMedian.Binary.GCDLoop.program line 67
  15. theorem OAI.MetricKMedian.Binary.GCDLoop.run_ordered line 76
  16. theorem OAI.MetricKMedian.Binary.GCDLoop.run line 92
  17. def OAI.MetricKMedian.Binary.GCDLoop.loop line 106
  18. def OAI.MetricKMedian.Binary.PolyProgram.natGcd line 116