OAI/Combinatorics/KMedianRecovery/Encoding/UnaryParser.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.step line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.step_computes line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.next line 19
  4. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.next_computes line 20
  5. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.mass_next line 28
  6. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.length_next line 39
  7. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.iterate_bounds line 45
  8. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.loop line 54
  9. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.loop_computes line 55
  10. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.next_stop line 69
  11. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.next_false line 71
  12. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.next_true line 74
  13. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.exact_prefix line 77
  14. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.run line 87
  15. def OAI.MetricKMedianRecovery.BitMachine.UnaryParser.run_computes line 90
  16. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryParser.run_code line 93
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.nat line 107
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.nat_computes line 109
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.nat_code line 111
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.numerator line 117
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.numerator_computes line 119
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.denominator line 121
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.denominator_computes line 122
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.rational line 125
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.rational_computes line 127
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInputParser.rational_code line 130