OAI/Combinatorics/KMedianRecovery/Recovery/MergePath.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RationalPhase.completion line 9
2. lemma OAI.MetricKMedianRecovery.RationalPhase.completion_spec line 13
3. def OAI.MetricKMedianRecovery.CanonicalMergePath.CorrectCompletion line 38
4. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.rational_correct line 43
5. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.CorrectCompletion.retaining line 52
6. inductive OAI.MetricKMedianRecovery.CanonicalMergePath.Path line 66
7. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.Path.toWalk line 74
8. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.Path.append line 81
9. def OAI.MetricKMedianRecovery.CanonicalMergePath.deleteSuffix line 89
10. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.deleteSuffix_length line 98
11. theorem OAI.MetricKMedianRecovery.CanonicalMergePath.deleteSuffix_spec line 105
12. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.Path.last_good line 169
13. def OAI.MetricKMedianRecovery.CanonicalMergePath.advancePrefix line 173
14. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.advancePrefix_length line 179
15. theorem OAI.MetricKMedianRecovery.CanonicalMergePath.advancePrefix_spec line 185
16. def OAI.MetricKMedianRecovery.CanonicalMergePath.matchPrefix line 239
17. theorem OAI.MetricKMedianRecovery.CanonicalMergePath.matchPrefix_spec line 247
18. def OAI.MetricKMedianRecovery.CanonicalMergePath.pruneSuffix line 306
19. lemma OAI.MetricKMedianRecovery.CanonicalMergePath.pruneSuffix_length line 311
20. theorem OAI.MetricKMedianRecovery.CanonicalMergePath.pruneSuffix_spec line 316
21. def OAI.MetricKMedianRecovery.CanonicalMergePath.regularPath line 352
22. theorem OAI.MetricKMedianRecovery.CanonicalMergePath.regularPath_spec line 357