OAI/Computability/StarHeight/MarkerSearch.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.LocalMarkers.AgreesOn line 14
  2. def OAI.GeneralizedStarHeight.LocalMarkers.ShortContinuation line 17
  3. lemma OAI.GeneralizedStarHeight.LocalMarkers.short_continuation_exists line 21
  4. lemma OAI.GeneralizedStarHeight.LocalMarkers.short_continuations_equal line 33
  5. lemma OAI.GeneralizedStarHeight.LocalMarkers.common_continuation line 63
  6. lemma OAI.GeneralizedStarHeight.LocalMarkers.periodic_run line 75
  7. def OAI.GeneralizedStarHeight.MarkerSearch.Separated line 130
  8. def OAI.GeneralizedStarHeight.MarkerSearch.FirstAfter line 133
  9. lemma OAI.GeneralizedStarHeight.MarkerSearch.firstAfter_unique line 136
  10. def OAI.GeneralizedStarHeight.MarkerSearch.search line 140
  11. lemma OAI.GeneralizedStarHeight.MarkerSearch.search_none line 145
  12. lemma OAI.GeneralizedStarHeight.MarkerSearch.search_some line 159
  13. lemma OAI.GeneralizedStarHeight.MarkerSearch.search_some_or_none line 190
  14. lemma OAI.GeneralizedStarHeight.MarkerSearch.search_ext line 197
  15. lemma OAI.GeneralizedStarHeight.MarkerSearch.firstAfter_shift line 212
  16. lemma OAI.GeneralizedStarHeight.MarkerSearch.instability_charge line 242
  17. lemma OAI.GeneralizedStarHeight.MarkerSearch.extension_charge line 283
  18. lemma OAI.GeneralizedStarHeight.MarkerSearch.close_unique line 305
  19. lemma OAI.GeneralizedStarHeight.MarkerSearch.separated_interval_unique line 311
  20. lemma OAI.GeneralizedStarHeight.MarkerSearch.firstAfter_same_side line 320
  21. lemma OAI.GeneralizedStarHeight.MarkerSearch.left_charge_card line 332
  22. lemma OAI.GeneralizedStarHeight.MarkerSearch.right_charge_card line 364
  23. def OAI.GeneralizedStarHeight.MarkerSearch.InnerFailure line 398
  24. lemma OAI.GeneralizedStarHeight.MarkerSearch.innerFailure_charge line 402
  25. lemma OAI.GeneralizedStarHeight.MarkerSearch.innerFailure_card line 413