OAI/Combinatorics/KMedianRecovery/Machines/SliceFold.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.CanonicalSlices.Acc line 10
  2. def OAI.MetricKMedianRecovery.CanonicalSlices.addFront line 15
  3. def OAI.MetricKMedianRecovery.CanonicalSlices.step line 16
  4. lemma OAI.MetricKMedianRecovery.CanonicalSlices.fold_result line 18
  5. lemma OAI.MetricKMedianRecovery.CanonicalSlices.addFront_nil line 31
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.itemsBits line 40
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.cutBits line 41
  8. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.outBits line 43
  9. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.accBits line 44
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.itemsBits_append line 46
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.itemsBits_cons line 48
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.itemsBits_nil line 50
  13. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.itemsBits_tail line 51
  14. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.itemsBits_tail_le line 56
  15. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.outBits_append line 61
  16. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.outBits_singleton line 64
  17. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.sf line 67
  18. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.item line 68
  19. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.sf_computes line 69
  20. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.item_computes line 71
  21. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.front line 72
  22. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.front_computes line 73
  23. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.rest line 74
  24. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.rest_computes line 75
  25. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.cut line 76
  26. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.cut_computes line 77
  27. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.output line 84
  28. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.output_computes line 85
  29. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.step line 86
  30. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.step_computes line 87
  31. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.step_pack line 94
  32. structure OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.Bounds line 100
  33. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.Bounds.step line 105
  34. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.Bounds.fold line 123
  35. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.capacityPoly line 131
  36. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.capacity line 134
  37. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.accBits_bound line 135
  38. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.initial line 150
  39. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.initial_computes line 151
  40. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.result line 159
  41. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.result_computes line 160
  42. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.run line 162
  43. def OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.run_computes line 163
  44. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.result_items line 164
  45. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Slices.run_items line 184