OAI/Combinatorics/KMedianRecovery/Recovery/FirstPresent.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.present line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.present_computes line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.found line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.found_computes line 14
  5. def OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.run line 16
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.run_computes line 17
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.marker line 22
  8. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.find_markers line 23
  9. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.FirstPresent.run_pack line 32
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftCount line 48
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightCount line 49
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftCount_computes line 50
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightCount_computes line 51
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftCount_pack line 52
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightCount_pack line 57
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.key_pack line 62
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.sandwiched line 66
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.sandwiched_computes line 69
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.sandwiched_pack line 72
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.transition line 80
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.transition_computes line 83
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.transition_pack line 87
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.suffix line 104
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.suffix_computes line 105
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.current line 106
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.current_computes line 107
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.transitionInput line 108
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.transitionInput_computes line 110
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.cutOp line 112
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.cutOp_computes line 114
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.cutOp_pack line 119
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.scanInput line 136
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.scanInput_computes line 137
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.markers line 139
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.markers_computes line 140
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.lastNode line 141
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.lastNode_computes line 142
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.fallback line 144
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.fallback_computes line 145
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.run line 152
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.run_computes line 153
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.head_encode_of_head line 154
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.pack line 162
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.markers_pack line 165
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.fallback_pack line 181
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNodeScan.run_pack line 189