OAI/Computability/StarHeight/Episodes.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.EpisodeAlgebra.PrefixCode line 16
  2. def OAI.GeneralizedStarHeight.EpisodeAlgebra.AllIn line 19
  3. def OAI.GeneralizedStarHeight.EpisodeAlgebra.updateWord line 22
  4. def OAI.GeneralizedStarHeight.EpisodeAlgebra.graph line 25
  5. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.AllIn.mono line 28
  6. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.AllIn.append line 31
  7. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.AllIn.of_append_right line 38
  8. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.updateWord_nil line 41
  9. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.updateWord_cons line 44
  10. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.updateWord_append line 48
  11. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.graph_nil line 53
  12. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.graph_singleton line 56
  13. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.graph_mono line 60
  14. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.graph_concat line 65
  15. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.flatten_prefix line 73
  16. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.consume_graph_prefix line 106
  17. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.flatten_injective line 120
  18. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.graph_iff_update line 127
  19. def OAI.GeneralizedStarHeight.EpisodeAlgebra.SplitSound line 136
  20. def OAI.GeneralizedStarHeight.EpisodeAlgebra.SplitAvailable line 142
  21. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.consume_pair_prefix line 146
  22. def OAI.GeneralizedStarHeight.EpisodeAlgebra.start line 158
  23. def OAI.GeneralizedStarHeight.EpisodeAlgebra.middle line 161
  24. def OAI.GeneralizedStarHeight.EpisodeAlgebra.finish line 164
  25. def OAI.GeneralizedStarHeight.EpisodeAlgebra.body line 167
  26. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.mem_start_iff line 170
  27. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.mem_middle_iff line 176
  28. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.mem_finish_iff line 186
  29. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.mem_body_iff line 192
  30. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.suffix_sound line 206
  31. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.body_sound line 232
  32. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.body_prepend_skip line 246
  33. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.body_prepend_pair line 259
  34. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.body_available line 280
  35. theorem OAI.GeneralizedStarHeight.EpisodeAlgebra.split_identity line 296
  36. theorem OAI.GeneralizedStarHeight.EpisodeAlgebra.split_height line 308
  37. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.graph_empty line 333
  38. lemma OAI.GeneralizedStarHeight.EpisodeAlgebra.empty_skip_height line 357