OAI/Computability/StarHeight/StreamRecovery.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.GeneralizedStarHeight.OuterStream.Geometry line 24
2. lemma OAI.GeneralizedStarHeight.OuterStream.Geometry.actual_visibility line 40
3. lemma OAI.GeneralizedStarHeight.OuterStream.Geometry.origin_overlap line 59
4. lemma OAI.GeneralizedStarHeight.OuterStream.Geometry.present line 74
5. lemma OAI.GeneralizedStarHeight.OuterStream.consumes line 96
6. lemma OAI.GeneralizedStarHeight.OuterStream.Geometry.cut_multiple line 109
7. lemma OAI.GeneralizedStarHeight.OuterStream.residue_shift line 117
8. lemma OAI.GeneralizedStarHeight.OuterStream.pair_sound line 127
9. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.factors_congr line 201
10. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.later_ext line 224
11. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.later_congr line 228
12. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Visible.innerVisible line 243
13. def OAI.GeneralizedStarHeight.InnerStream.hypothetical line 264
14. def OAI.GeneralizedStarHeight.InnerStream.update line 270
15. lemma OAI.GeneralizedStarHeight.InnerStream.hypothetical_congr line 275
16. structure OAI.GeneralizedStarHeight.InnerStream.Prefix line 291
17. structure OAI.GeneralizedStarHeight.InnerStream.Suffix line 295
18. lemma OAI.GeneralizedStarHeight.InnerStream.prefix_actual line 302
19. lemma OAI.GeneralizedStarHeight.InnerStream.suffix_actual line 313
20. lemma OAI.GeneralizedStarHeight.InnerStream.same_slot_sound line 346
21. lemma OAI.GeneralizedStarHeight.InnerStream.pair_sound line 364
22. lemma OAI.GeneralizedStarHeight.InnerStream.hypothetical_actual line 393