OAI/Computability/StarHeight/UsableCopies.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.outer_available line 26
2. lemma OAI.GeneralizedStarHeight.InnerStream.available line 128
3. lemma OAI.GeneralizedStarHeight.SourceSchedule.Late.count_margins line 160
4. lemma OAI.GeneralizedStarHeight.SourceSchedule.Late.decoder_margins line 173
5. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.full_bad_card line 200
6. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.roster_visible line 259
7. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.inner_available line 270
8. def OAI.GeneralizedStarHeight.SlotResidues.slotIndex line 295
9. def OAI.GeneralizedStarHeight.SlotResidues.reserved line 296
10. def OAI.GeneralizedStarHeight.SlotResidues.slotModulus line 297
11. lemma OAI.GeneralizedStarHeight.SlotResidues.slotIndex_bounds line 299
12. lemma OAI.GeneralizedStarHeight.SlotResidues.slotIndex_injective line 304
13. lemma OAI.GeneralizedStarHeight.SlotResidues.reserved_distinct line 311
14. lemma OAI.GeneralizedStarHeight.SlotResidues.slotModulus_pos line 328