OAI/Combinatorics/KMedianRecovery/Recovery/PlanResult.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.sf line 14
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.sf_computes line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.rf line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.rf_computes line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.success line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.success_computes line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.rightHeight line 21
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.rightHeight_computes line 22
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.price line 23
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.price_computes line 24
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.root line 25
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.root_computes line 26
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.common line 27
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.common_computes line 28
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.leafInput line 29
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.leafInput_computes line 30
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.finishInput line 45
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.finishInput_computes line 47
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.run line 56
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.run_computes line 58
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.pack line 63
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.leafInput_pack line 65
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPlanResult.run_pack line 85
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.original_order line 123
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.originalSort line 126
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.copiedSet line 131
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.copiedSet_computes line 132
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.copiedSet_pack line 133
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.pool line 142
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.pool_computes line 143
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.pool_pack line 145
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.threeQ line 148
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.threeQ_computes line 149
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.threeQOne line 152
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.threeQOne_computes line 153
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.bankFirst line 156
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.bankFirst_computes line 157
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.banks line 159
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.banks_computes line 160
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.banks_pack line 162