OAI/Computability/StarHeight/PeriodicSplicing.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GeneralizedStarHeight.StreamSplice.periodic_of_dvd line 17
  2. lemma OAI.GeneralizedStarHeight.StreamSplice.periodic_pattern line 22
  3. lemma OAI.GeneralizedStarHeight.StreamSplice.fits_realizes line 30
  4. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.symm line 50
  5. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.agrees_periodic line 59
  6. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.mismatch_periodic line 84
  7. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.short_period_factorial line 100
  8. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.endAt_none line 108
  9. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.endAt line 125
  10. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.exists_horizon line 155
  11. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.visible_long line 164
  12. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.complete_regular line 168
  13. def OAI.GeneralizedStarHeight.EpisodeAlgebra.remainder line 203
  14. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.remainder_eq line 206
  15. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.factor_remainder line 215
  16. lemma OAI.GeneralizedStarHeight.EpisodeEnd.firstMismatch_of_disagrees line 243
  17. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.complete_prefix line 263
  18. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.remainder_middle line 276
  19. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.remainder_regular line 319
  20. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.remainder_height line 331
  21. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.residue_eq_of_dvd line 346
  22. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.exists_horizon line 351
  23. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Failed_phase_congr line 381