OAI/Computability/StarHeight/SplitMetadata.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GeneralizedStarHeight.SplitMetadata.Omitted line 15
  2. def OAI.GeneralizedStarHeight.SplitMetadata.insert line 17
  3. lemma OAI.GeneralizedStarHeight.SplitMetadata.insert_at line 20
  4. lemma OAI.GeneralizedStarHeight.SplitMetadata.insert_away line 23
  5. lemma OAI.GeneralizedStarHeight.SplitMetadata.insert_actual line 26
  6. lemma OAI.GeneralizedStarHeight.SplitMetadata.insert_eq_update line 31
  7. structure OAI.GeneralizedStarHeight.SplitMetadata.MainTag line 36
  8. instance OAI.GeneralizedStarHeight.SplitMetadata.(instance at line 45) line 45
  9. structure OAI.GeneralizedStarHeight.SplitMetadata.PeriodicTag line 61
  10. abbrev OAI.GeneralizedStarHeight.SplitMetadata.Tag line 69
  11. def OAI.GeneralizedStarHeight.SplitMetadata.Tag.input line 71
  12. def OAI.GeneralizedStarHeight.SplitMetadata.Tag.output line 75
  13. def OAI.GeneralizedStarHeight.SplitMetadata.Tag.residue line 79
  14. structure OAI.GeneralizedStarHeight.SplitMetadata.Kind line 83
  15. instance OAI.GeneralizedStarHeight.SplitMetadata.(instance at line 90) line 90
  16. abbrev OAI.GeneralizedStarHeight.SplitMetadata.Roster line 112
  17. lemma OAI.GeneralizedStarHeight.SplitMetadata.certificate_at_actual line 115
  18. lemma OAI.GeneralizedStarHeight.SplitMetadata.certificate_available line 121
  19. lemma OAI.GeneralizedStarHeight.IntegerSchedules.multiple_gt line 133
  20. structure OAI.GeneralizedStarHeight.IntegerSchedules.Inner line 141
  21. lemma OAI.GeneralizedStarHeight.IntegerSchedules.exists_inner line 161
  22. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.extension_pos line 205
  23. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.max_pos line 210
  24. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.halfGap_large line 213
  25. def OAI.GeneralizedStarHeight.IntegerSchedules.Inner.boundary line 220
  26. def OAI.GeneralizedStarHeight.IntegerSchedules.Inner.mainBase line 222
  27. def OAI.GeneralizedStarHeight.IntegerSchedules.Inner.mainOffset line 224
  28. def OAI.GeneralizedStarHeight.IntegerSchedules.Inner.periodicOffset line 226
  29. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.main_multiple line 229
  30. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.periodic_multiple line 234
  31. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.main_before line 243
  32. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.main_after line 255
  33. lemma OAI.GeneralizedStarHeight.IntegerSchedules.Inner.periodic_before line 269