OAI/Combinatorics/KMedianRecovery/Branching/BlueProgram.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.pack line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.states line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.states_computes line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.prepare line 18
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.prepare_computes line 19
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.prepare_pack line 22
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.run line 34
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.run_computes line 35
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.run_pack line 36
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueProgram.source_run line 43
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.matching line 62
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.matching_computes line 64
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.pick line 66
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.pick_computes line 67
  15. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.atomEnc line 68
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.pick_pack line 69
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.query line 88
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.query_computes line 89
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.source line 90
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.source_computes line 91
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.destination line 93
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.destination_computes line 94
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.prepared line 96
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.prepared_computes line 97
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.run line 99
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.run_computes line 100
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.run_some line 105
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueOutput.run_best line 116