OAI/Combinatorics/KMedianRecovery/Machines/ScanMachine.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.cf line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.cf_computes line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.opened line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.opened_computes line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.base line 19
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.base_computes line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.contInput line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.contInput_computes line 23
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.node line 24
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.node_computes line 25
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.contCtx line 26
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryScan.node_pack line 27
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.mapCtx line 42
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.mapCtx_computes line 43
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.nodes line 47
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.nodes_computes line 49
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.scanInput line 57
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.scanInput_computes line 58
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.run line 65
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.run_computes line 66
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryScan.pack line 67
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryScan.nodes_pack line 70
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryScan.run_pack line 81
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.chainInput line 98
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.chainInput_computes line 100
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.crossCtx line 111
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.crossCtx_computes line 112
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.nextQ line 120
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.nextQ_computes line 121
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.firstNode line 122
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.firstNode_computes line 123
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.scanInput line 124
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.scanInput_computes line 126
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.run line 138
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.run_computes line 139
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.pack line 140
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.chainInput_pack line 143
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.crossCtx_pack line 150
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteCross.run_pack line 156