OAI/Combinatorics/KMedianRecovery/Recovery/RegularChain.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.regularInput line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.regularInput_computes line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.context line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.context_computes line 19
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.vertices line 28
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.vertices_computes line 29
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.run line 31
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.run_computes line 32
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.pack line 33
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.regularInput_pack line 35
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.context_pack line 38
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRegularChain.run_pack line 43
  13. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.walk line 69
  14. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.slots line 73
  15. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.firstPresent line 77
  16. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.finalNode line 82
  17. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.walk_slots line 86
  18. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.cuts_slots line 94
  19. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.firstPresent_append_none line 104
  20. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.finalNode_reverse line 108
  21. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.transition line 119
  22. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.scan_walk line 124