OAI/Computability/StarHeight/ScheduleClock.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GeneralizedStarHeight.PeriodicClock.prime_mesh line 16
2. lemma OAI.GeneralizedStarHeight.PeriodicClock.prime_pairwise line 30
3. lemma OAI.GeneralizedStarHeight.PeriodicClock.small_coprime line 38
4. lemma OAI.GeneralizedStarHeight.PeriodicClock.unbounded_residue line 45
5. theorem OAI.GeneralizedStarHeight.ScheduleClock.exists_stencil_clock line 100
6. def OAI.GeneralizedStarHeight.EpisodeEnd.FirstMismatch line 159
7. lemma OAI.GeneralizedStarHeight.EpisodeEnd.firstMismatch_unique line 162
8. lemma OAI.GeneralizedStarHeight.EpisodeEnd.shortCont_congr line 178
9. def OAI.GeneralizedStarHeight.EpisodeEnd.EndAt line 187
10. def OAI.GeneralizedStarHeight.EpisodeEnd.clockAnchor line 193
11. lemma OAI.GeneralizedStarHeight.EpisodeEnd.EndAt.unique line 195
12. lemma OAI.GeneralizedStarHeight.EpisodeEnd.shared_end line 208
13. lemma OAI.GeneralizedStarHeight.EpisodeEnd.transfer_end line 246
14. structure OAI.GeneralizedStarHeight.LocalMarkers.Rule line 279
15. lemma OAI.GeneralizedStarHeight.LocalMarkers.nonempty_rule line 291
16. lemma OAI.GeneralizedStarHeight.EndSearch.search_congr line 302
17. lemma OAI.GeneralizedStarHeight.EndSearch.search_local line 315
18. lemma OAI.GeneralizedStarHeight.EndSearch.absent_continuation line 326