OAI/Combinatorics/KMedianRecovery/Machines/LengthQuery.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.ctxBits line 14
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.cf line 18
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.cf_computes line 19
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.newLeaf line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.newLeaf_computes line 22
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.newLeaf_pack line 26
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.opened line 34
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.opened_computes line 36
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.opened_pack line 39
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.base line 50
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.base_computes line 51
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.interior line 52
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.interior_computes line 54
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.interior_pack line 56
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.isZero line 64
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.isZero_computes line 65
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.isUpper line 66
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.isUpper_computes line 67
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.chosen line 68
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.chosen_computes line 69
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.chosen_pack line 71
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.finalOpened line 83
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.finalOpened_computes line 84
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.count line 86
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.count_computes line 87
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLengthQuery.count_pack line 89
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.resultBits line 105
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.lower line 108
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.upper line 109
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.lower_computes line 110
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.upper_computes line 111
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.context line 112
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.context_computes line 113
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.boundK line 114
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.boundK_computes line 115
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftInput line 116
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightInput line 117
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftInput_computes line 118
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightInput_computes line 119
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftHistory line 120
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightHistory line 121
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftHistory_computes line 122
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightHistory_computes line 123
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftSuccess line 124
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightSuccess line 125
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.bracket line 126
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftSuccess_computes line 127
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightSuccess_computes line 137
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.bracket_computes line 147
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftEqual line 157
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightEqual line 158
  52. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.leftEqual_computes line 159
  53. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.rightEqual_computes line 161
  54. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.finish line 163
  55. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.finish_computes line 165
  56. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.finish_pack line 167
  57. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.input line 178
  58. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.input_computes line 179
  59. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.run line 180
  60. def OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.run_computes line 181
  61. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLengthSearch.run_pack line 182