OAI/Combinatorics/KMedianRecovery/Machines/InitialLoop.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.initial_prices_length line 11
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.run_initial line 20
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.pack line 47
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.output line 52
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.unaryRat line 55
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.high line 58
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.high_computes line 60
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.far line 63
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.far_computes line 65
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.ctx line 67
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.ctx_computes line 68
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loInput line 70
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loInput_computes line 71
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loCount line 73
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loCount_computes line 74
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loHistory line 76
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loHistory_computes line 77
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loFinish line 79
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loFinish_computes line 80
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.bracketInput line 88
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.bracketInput_computes line 89
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.bracket line 99
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.bracket_computes line 100
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lower line 102
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lower_computes line 103
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerInput line 105
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerInput_computes line 106
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerCount line 108
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerCount_computes line 109
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerHistory line 111
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerHistory_computes line 112
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerFinish line 114
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.lowerFinish_computes line 115
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upper line 123
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upper_computes line 124
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperInput line 126
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperInput_computes line 127
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperCount line 129
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperCount_computes line 130
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperHistory line 132
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperHistory_computes line 133
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperFinish line 135
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.upperFinish_computes line 136
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.initialState line 144
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.initialState_computes line 145
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.initialOutcome line 157
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.initialOutcome_computes line 158
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loopInput line 160
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loopInput_computes line 161
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.normal line 173
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.normal_computes line 175
  52. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.run line 182
  53. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.run_computes line 183