OAI/Combinatorics/KMedianRecovery/Machines/BisectionMachine.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.clog_two_eq_size_pred line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.predWords line 16
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.predWords_computes line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.logWord line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.logWord_computes line 21
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.logWord_eq line 22
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.width line 26
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.width_computes line 27
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.widthCeil line 29
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.widthCeil_computes line 30
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.fuel line 31
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.fuel_computes line 32
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.context line 33
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.context_computes line 34
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.input line 38
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.input_computes line 39
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.run line 40
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.run_computes line 41
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.pack line 43
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.fuel_pack line 45
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.context_pack line 49
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBisection.run_pack line 52