OAI/Computability/StarHeight/OriginSplicing.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.anchor_phase line 20
  2. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.failed line 41
  3. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.failedLanguage line 57
  4. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.failed_regular line 60
  5. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.exists_uniform_horizon line 99
  6. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.exists_inner_horizon line 119
  7. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.InnerVisible.mono line 136
  8. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Visible.from_bounds line 140
  9. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.factors line 159
  10. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.later line 185
  11. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.guard line 204
  12. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.anchor_relative_phase line 223
  13. lemma OAI.GeneralizedStarHeight.StreamSplice.Frame.decoder line 245
  14. def OAI.GeneralizedStarHeight.StreamSplice.wordTest line 281
  15. structure OAI.GeneralizedStarHeight.StreamSplice.SummaryEq line 284
  16. lemma OAI.GeneralizedStarHeight.StreamSplice.clock_eq_of_dvd line 293
  17. lemma OAI.GeneralizedStarHeight.StreamSplice.wordTest_regular line 298
  18. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.ending_middle line 351
  19. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.ending_height line 384
  20. structure OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Inspection line 398
  21. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.exists_inspection line 405