OAI/Computability/StarHeight/CanonicalEpisodes.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.WordIntervals.segment line 16
  2. lemma OAI.GeneralizedStarHeight.WordIntervals.length_segment line 19
  3. lemma OAI.GeneralizedStarHeight.WordIntervals.segment_add line 22
  4. lemma OAI.GeneralizedStarHeight.WordIntervals.segment_congr line 32
  5. lemma OAI.GeneralizedStarHeight.WordIntervals.segment_translate line 38
  6. def OAI.GeneralizedStarHeight.WordIntervals.Realizes line 46
  7. lemma OAI.GeneralizedStarHeight.WordIntervals.realizes_iff_segment line 49
  8. lemma OAI.GeneralizedStarHeight.WordIntervals.realizes_segment line 61
  9. lemma OAI.GeneralizedStarHeight.WordIntervals.realizes_exists line 66
  10. lemma OAI.GeneralizedStarHeight.WordIntervals.Realizes.prefix line 77
  11. lemma OAI.GeneralizedStarHeight.WordIntervals.Realizes.agrees line 82
  12. lemma OAI.GeneralizedStarHeight.WordIntervals.Realizes.append line 91
  13. lemma OAI.GeneralizedStarHeight.WordIntervals.Realizes.append_left line 96
  14. lemma OAI.GeneralizedStarHeight.WordIntervals.Realizes.append_right line 99
  15. def OAI.GeneralizedStarHeight.WordIntervals.piece line 108
  16. lemma OAI.GeneralizedStarHeight.WordIntervals.length_piece line 110
  17. lemma OAI.GeneralizedStarHeight.WordIntervals.piece_append line 115
  18. lemma OAI.GeneralizedStarHeight.WordIntervals.piece_congr line 121
  19. lemma OAI.GeneralizedStarHeight.WordIntervals.realizes_piece line 127
  20. def OAI.GeneralizedStarHeight.WordIntervals.product line 133
  21. lemma OAI.GeneralizedStarHeight.WordIntervals.product_append line 135
  22. lemma OAI.GeneralizedStarHeight.WordIntervals.product_congr line 142
  23. structure OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters line 154
  24. def OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.width line 172
  25. def OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.small line 174
  26. def OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.large line 177
  27. def OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.Visible line 180
  28. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.Visible.mono line 184
  29. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.width_nonneg line 189
  30. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.small_width_le line 195
  31. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.searches_congr line 199
  32. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.seed_pos line 212
  33. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.seed_square line 214
  34. def OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.complete line 219
  35. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.not_nil line 224
  36. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.prefix_code line 232
  37. def OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.Guard line 247
  38. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.guard_shared_end line 254
  39. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.guard_available line 282