OAI/Computability/StarHeight/StreamSplicing.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.piece_left_any line 21
2. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.product_left_any line 27
3. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.observedSuffix line 31
4. def OAI.GeneralizedStarHeight.OuterStream.originBound line 65
5. lemma OAI.GeneralizedStarHeight.OuterStream.origin_bound line 68
6. lemma OAI.GeneralizedStarHeight.OuterStream.main_origin line 75
7. lemma OAI.GeneralizedStarHeight.OuterStream.suffix_splice line 81
8. lemma OAI.GeneralizedStarHeight.InnerStream.hypothetical_splice line 145
9. def OAI.GeneralizedStarHeight.InnerStream.inspectionBound line 167
10. lemma OAI.GeneralizedStarHeight.InnerStream.origin_bound line 171
11. lemma OAI.GeneralizedStarHeight.InnerStream.boundary_bound line 181
12. lemma OAI.GeneralizedStarHeight.InnerStream.suffix_splice line 189
13. lemma OAI.GeneralizedStarHeight.StreamSplice.wordTest_finite line 222
14. def OAI.GeneralizedStarHeight.OuterStream.prefixLanguage line 240
15. def OAI.GeneralizedStarHeight.OuterStream.suffixLanguage line 244
16. lemma OAI.GeneralizedStarHeight.OuterStream.prefix_finite line 248
17. lemma OAI.GeneralizedStarHeight.OuterStream.prefix_height line 265
18. lemma OAI.GeneralizedStarHeight.OuterStream.suffix_regular line 269
19. lemma OAI.GeneralizedStarHeight.OuterStream.suffix_height line 277
20. def OAI.GeneralizedStarHeight.InnerStream.prefixLanguage line 301
21. def OAI.GeneralizedStarHeight.InnerStream.suffixLanguage line 305
22. lemma OAI.GeneralizedStarHeight.InnerStream.prefix_finite line 309
23. lemma OAI.GeneralizedStarHeight.InnerStream.prefix_height line 318
24. lemma OAI.GeneralizedStarHeight.InnerStream.suffix_regular line 322
25. lemma OAI.GeneralizedStarHeight.InnerStream.suffix_height line 331