OAI/Combinatorics/KMedianRecovery/Recovery/CrossCount.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.containsItem line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.containsItem_computes line 10
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.inter line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.inter_computes line 14
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.inter_pack line 16
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.lengthBits_setBits line 24
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.countInter line 26
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.countInter_computes line 27
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.countInter_pack line 28
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.ctxBits line 39
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.nodeBits line 40
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.cf line 42
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.cf_computes line 43
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.opened line 44
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.opened_computes line 46
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.opened_pack line 48
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.paid line 53
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.paid_computes line 54
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.paid_pack line 56
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.finalOpened line 62
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.finalOpened_computes line 64
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.finalCount line 66
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.finalCount_computes line 67
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.finalCount_pack line 69
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removedTail line 82
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removedTail_computes line 84
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removedTail_pack line 88
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.addOp line 93
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.addOp_computes line 94
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removeOp line 103
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removeOp_computes line 105
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.replaceOp line 115
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.replaceOp_computes line 116
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.adds line 125
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.adds_computes line 126
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removes line 130
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removes_computes line 131
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.replaces line 136
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.replaces_computes line 137
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.candidates line 142
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.candidates_computes line 143
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.adds_pack line 144
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removes_pack line 148
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.replaces_pack line 156
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.candidates_pack line 164
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.view line 168
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.view_computes line 169
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.view_pack line 170