OAI/Computability/StarHeight/RegularLanguages.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GeneralizedStarHeight.FiniteRecognition.regular_mul line 15
  2. lemma OAI.GeneralizedStarHeight.FiniteRecognition.regular_finite line 47
  3. lemma OAI.GeneralizedStarHeight.FiniteRecognition.regular_singleton line 57
  4. lemma OAI.GeneralizedStarHeight.FiniteRecognition.regular_finset_iSup line 60
  5. lemma OAI.GeneralizedStarHeight.FiniteRecognition.regular_iSup line 76
  6. lemma OAI.GeneralizedStarHeight.FiniteRecognition.regular_recognized line 83
  7. lemma OAI.GeneralizedStarHeight.FiniteRecognition.regular_sandwich line 103
  8. def OAI.GeneralizedStarHeight.PeriodicSummary.matcher line 167
  9. def OAI.GeneralizedStarHeight.PeriodicSummary.Fits line 171
  10. lemma OAI.GeneralizedStarHeight.PeriodicSummary.eval_none line 175
  11. lemma OAI.GeneralizedStarHeight.PeriodicSummary.eval_isSome line 181
  12. lemma OAI.GeneralizedStarHeight.PeriodicSummary.fits_iff line 195
  13. def OAI.GeneralizedStarHeight.PeriodicSummary.transition line 209
  14. lemma OAI.GeneralizedStarHeight.PeriodicSummary.fits_congr line 213
  15. def OAI.GeneralizedStarHeight.PeriodicSummary.lengthMod line 226
  16. lemma OAI.GeneralizedStarHeight.PeriodicSummary.lengthMod_dvd line 234
  17. def OAI.GeneralizedStarHeight.StreamSplice.splice line 248
  18. lemma OAI.GeneralizedStarHeight.StreamSplice.splice_left line 252
  19. lemma OAI.GeneralizedStarHeight.StreamSplice.splice_right line 255
  20. lemma OAI.GeneralizedStarHeight.StreamSplice.splice_middle line 260
  21. lemma OAI.GeneralizedStarHeight.StreamSplice.splice_realizes line 267
  22. structure OAI.GeneralizedStarHeight.StreamSplice.Frame line 285
  23. lemma OAI.GeneralizedStarHeight.StreamSplice.splice_frame line 291
  24. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.agrees_left line 304
  25. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.piece_left line 308
  26. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.piece_right line 311
  27. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.product line 323