OAI/Computability/StarHeight/Translation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.StreamShift.shift line 16
  2. lemma OAI.GeneralizedStarHeight.StreamShift.shift_add line 18
  3. lemma OAI.GeneralizedStarHeight.StreamShift.map_injective line 21
  4. lemma OAI.GeneralizedStarHeight.StreamShift.map_none line 25
  5. lemma OAI.GeneralizedStarHeight.StreamShift.realizes line 28
  6. lemma OAI.GeneralizedStarHeight.StreamShift.piece line 33
  7. lemma OAI.GeneralizedStarHeight.StreamShift.product line 41
  8. lemma OAI.GeneralizedStarHeight.StreamShift.markers line 46
  9. lemma OAI.GeneralizedStarHeight.StreamShift.marker_search line 51
  10. lemma OAI.GeneralizedStarHeight.StreamShift.end_search line 68
  11. lemma OAI.GeneralizedStarHeight.StreamShift.agrees line 89
  12. lemma OAI.GeneralizedStarHeight.StreamShift.continuation line 94
  13. lemma OAI.GeneralizedStarHeight.StreamShift.mismatch line 103
  14. lemma OAI.GeneralizedStarHeight.StreamShift.ending line 109
  15. lemma OAI.GeneralizedStarHeight.StreamShift.inner_failure line 119
  16. lemma OAI.GeneralizedStarHeight.StreamShift.unstable line 145
  17. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.small_shift line 168
  18. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.large_shift line 172
  19. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.visible_shift line 176
  20. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.end_shift line 181
  21. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.guard_shift line 187
  22. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.inner_shift line 210
  23. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.anchor_shift line 217
  24. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.innerVisible_shift line 223
  25. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.visible_shift line 228
  26. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.failed_shift line 240
  27. lemma OAI.GeneralizedStarHeight.SuffixDecoder.test_shift line 263
  28. def OAI.GeneralizedStarHeight.BoundarySnapshot.translated line 299
  29. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.translated_none line 302
  30. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.translated_position line 305
  31. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.present_shift line 311
  32. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.present_shift_iff line 317
  33. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.factors_shift line 332
  34. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.actual_shift line 345
  35. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.later_shift line 351