OAI/Computability/StarHeight/ExceptionalOrigins.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters line 19
  2. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.residue line 39
  3. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.residue_val line 44
  4. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.residue_ne line 48
  5. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.inner line 58
  6. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Z line 61
  7. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Star line 67
  8. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Failed line 71
  9. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.anchor line 73
  10. def OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.bad line 76
  11. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.width_inner_count line 80
  12. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.bad_card line 109
  13. lemma OAI.GeneralizedStarHeight.MarkerSearch.search_congr line 203
  14. lemma OAI.GeneralizedStarHeight.MarkerSearch.innerFailure_congr line 212
  15. lemma OAI.GeneralizedStarHeight.EndSearch.unstable_congr line 239
  16. structure OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Visible line 260
  17. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Visible.mono line 269
  18. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Visible.min line 277
  19. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Z_congr line 286
  20. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.Failed_congr line 313