OAI/Computability/StarHeight/SuffixDecoder.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GeneralizedStarHeight.SuffixDecoder.origin line 17
2. structure OAI.GeneralizedStarHeight.SuffixDecoder.Test line 19
3. lemma OAI.GeneralizedStarHeight.SuffixDecoder.searches_agree line 31
4. lemma OAI.GeneralizedStarHeight.SuffixDecoder.reference_forces_end line 43
5. lemma OAI.GeneralizedStarHeight.SuffixDecoder.true_anchor line 64
6. lemma OAI.GeneralizedStarHeight.SuffixDecoder.sound line 80
7. lemma OAI.GeneralizedStarHeight.SuffixDecoder.all_small_absent line 112
8. lemma OAI.GeneralizedStarHeight.SuffixDecoder.available_at line 123
9. lemma OAI.GeneralizedStarHeight.PeriodicCuts.markerless_run line 158
10. lemma OAI.GeneralizedStarHeight.PeriodicCuts.segment_shift_period line 170
11. lemma OAI.GeneralizedStarHeight.PeriodicCuts.product_periods line 178
12. lemma OAI.GeneralizedStarHeight.PeriodicCuts.fixed_prefix line 192
13. lemma OAI.GeneralizedStarHeight.PeriodicCuts.progression line 223
14. lemma OAI.GeneralizedStarHeight.PeriodicClock.map_modEq line 271
15. lemma OAI.GeneralizedStarHeight.PeriodicClock.sweep line 279
16. lemma OAI.GeneralizedStarHeight.PeriodicClock.progression_coprime line 294
17. lemma OAI.GeneralizedStarHeight.SuffixDecoder.available_copy line 312
18. lemma OAI.GeneralizedStarHeight.SpacedStencil.exists_points_fintype line 362
19. lemma OAI.GeneralizedStarHeight.SpacedStencil.exists_boundaries line 375