OAI/Computability/StarHeight/WordStreams.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.end_congr line 17
  2. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.complete_realizes line 35
  3. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.anchor_congr line 50
  4. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.failedLanguage_iff line 56
  5. lemma OAI.GeneralizedStarHeight.OuterStream.snapshot_congr line 80
  6. lemma OAI.GeneralizedStarHeight.OuterStream.update_congr line 95
  7. def OAI.GeneralizedStarHeight.OuterStream.wordUpdate line 102
  8. lemma OAI.GeneralizedStarHeight.OuterStream.wordUpdate_eq line 105
  9. lemma OAI.GeneralizedStarHeight.InnerStream.update_congr line 126
  10. def OAI.GeneralizedStarHeight.InnerStream.wordUpdate line 143
  11. lemma OAI.GeneralizedStarHeight.InnerStream.wordUpdate_eq line 146
  12. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.subset_height line 162
  13. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.complete_height line 169
  14. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.failedDomain line 178
  15. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.failedDomain_subset line 180
  16. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.failedDomain_height line 182
  17. lemma OAI.GeneralizedStarHeight.WordIntervals.realizes_cut line 193
  18. lemma OAI.GeneralizedStarHeight.WordIntervals.prefix_eq_of_length line 204