OAI/Combinatorics/KMedianRecovery/Recovery/CrossEdge.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.boolCond line 7
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.resultBits line 21
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.pack line 25
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftNode line 28
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightNode line 29
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftNode_computes line 30
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightNode_computes line 31
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftData line 32
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightData line 33
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftData_computes line 34
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightData_computes line 35
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftPaid line 36
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightPaid line 37
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftPaid_computes line 38
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightPaid_computes line 39
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftLength line 40
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightLength line 41
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.leftLength_computes line 42
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.rightLength_computes line 43
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.forward line 44
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.forward_computes line 47
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.forward_pack line 50
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.mixed line 59
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.mixed_computes line 60
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.mixedCount line 62
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.mixedCount_computes line 63
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.successNode line 65
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.successNode_computes line 66
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.taggedPair line 74
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.taggedPair_computes line 75
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.mixedCommon line 83
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.mixedCommon_computes line 84
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.directed line 86
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.directed_computes line 90
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.mixed_pack line 94
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.directed_pack line 98
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.flipped line 111
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.flipped_computes line 112
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.edge line 113
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryCross.edge_computes line 114
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCross.edge_pack line 115