OAI/Combinatorics/KMedianRecovery/Machines/RefineMachine.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.flatMapWith_typed line 8
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.ctxBits line 23
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.cutTail line 25
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.cutTail_computes line 26
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.source line 27
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.source_computes line 28
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.target line 29
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.target_computes line 30
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.cf line 31
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.cf_computes line 32
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.jumpContext line 33
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.jumpContext_computes line 34
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.edgeInput line 43
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.edgeInput_computes line 44
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.cutOp line 50
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.cutOp_computes line 51
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.cutOp_pack line 55
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.runInput line 71
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.runInput_computes line 72
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.run line 73
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.run_computes line 74
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRefine.run_pack line 75