OAI/Combinatorics/KMedianRecovery/Branching/CompletionFair.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.context line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.context_computes line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.prepared line 19
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.prepared_computes line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.run line 23
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.run_computes line 24
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.context_pack line 33
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.result line 37
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.run_pack line 43
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFair.run_flat line 53
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.table_id line 63
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.blueInput line 71
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.blueInput_computes line 72
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.records line 75
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.records_computes line 76
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.bluePack line 81
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.bluePack_computes line 82
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.best line 85
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.best_computes line 86
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.plan line 91
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.plan_computes line 92
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.rowInput line 95
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.rowInput_computes line 96
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.rows line 99
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.rows_computes line 100
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.completion line 103
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.completion_computes line 104
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.run line 107
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.run_computes line 108
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.blueInput_pack line 119
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.records_pack line 124
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.bluePack_pack line 126
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.rowInput_pack line 137
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.rows_pack line 143