OAI/Combinatorics/KMedianRecovery/Branching/CompletionRealize.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.pack line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.fillInput line 20
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.fillInput_computes line 21
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.filled line 23
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.filled_computes line 26
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.redValues line 28
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.redValues_computes line 29
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.redIndices line 34
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.redIndices_computes line 37
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.red line 39
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.red_computes line 41
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.blue line 42
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.blue_computes line 43
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.dest line 44
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.dest_computes line 45
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.removed line 46
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.removed_computes line 49
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.remain line 51
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.remain_computes line 53
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.added line 54
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.added_computes line 56
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.core line 57
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.core_computes line 59
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.runInput line 60
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.runInput_computes line 62
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.run line 65
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.run_computes line 66
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.fillInput_pack line 74
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.filled_pack line 77
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.redValues_pack line 81
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.redIndices_pack line 83
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.red_pack line 87
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.blue_pack line 90
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.dest_pack line 92
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.removed_pack line 94
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.remain_pack line 97
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.added_pack line 100
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionRealize.run_pack line 102