OAI/Combinatorics/KMedianRecovery/Branching/CategoricalRawPrep.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.pack line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.qword line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.aword line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.dimensions line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.qword_computes line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.aword_computes line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.dimensions_computes line 20
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.tword line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.lword line 22
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.bword line 23
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.tword_computes line 25
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.lword_computes line 26
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.bword_computes line 27
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.leftShape line 28
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.rightShape line 29
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.leftShape_computes line 30
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.rightShape_computes line 32
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.cut line 33
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.cut_computes line 35
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.left line 36
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.right line 37
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.left_computes line 39
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.right_computes line 41
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.runInput line 43
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.runInput_computes line 44
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.run line 46
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.run_computes line 47
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.qword_pack line 52
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.aword_pack line 55
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.dimensions_pack line 57
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.tword_pack line 58
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.leftShape_pack line 59
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.rightShape_pack line 61
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.cut_pack line 63
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.left_pack line 69
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.right_pack line 77
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Prepare.run_pack line 82
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.elemBits line 92
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.pack line 93
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.test line 95
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.test_computes line 97
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.options line 100
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.options_computes line 102
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.pick line 105
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.pick_computes line 108
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.options_pack line 114
  47. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.pick_pack line 119
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.run line 133
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.run_computes line 134
  50. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionFill.run_pack line 138