OAI/Computability/StarHeight/ObservedActions.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.ObservedMain.Certificate line 23
  2. structure OAI.GeneralizedStarHeight.ObservedMain.Prefix line 27
  3. structure OAI.GeneralizedStarHeight.ObservedMain.Suffix line 35
  4. lemma OAI.GeneralizedStarHeight.ObservedMain.pair_present line 42
  5. lemma OAI.GeneralizedStarHeight.ObservedMain.pair_entries line 50
  6. lemma OAI.GeneralizedStarHeight.ObservedMain.pair_sound line 60
  7. lemma OAI.GeneralizedStarHeight.ObservedMain.available line 81
  8. def OAI.GeneralizedStarHeight.SplitMetadata.tagCoefficient line 114
  9. lemma OAI.GeneralizedStarHeight.SplitMetadata.mainTag_card line 118
  10. lemma OAI.GeneralizedStarHeight.SplitMetadata.periodicTag_card line 137
  11. lemma OAI.GeneralizedStarHeight.SplitMetadata.tag_card line 147
  12. lemma OAI.GeneralizedStarHeight.SplitMetadata.tagCoefficient_pos line 152
  13. lemma OAI.GeneralizedStarHeight.SplitMetadata.exists_copies line 159
  14. def OAI.GeneralizedStarHeight.SourceSchedule.blockOrder line 181
  15. lemma OAI.GeneralizedStarHeight.SourceSchedule.block_lt line 188
  16. def OAI.GeneralizedStarHeight.SourceSchedule.absoluteBound line 193
  17. lemma OAI.GeneralizedStarHeight.SourceSchedule.abs_le_absoluteBound line 196
  18. lemma OAI.GeneralizedStarHeight.SourceSchedule.difference_bound line 202
  19. def OAI.GeneralizedStarHeight.SourceSchedule.innerD line 206
  20. lemma OAI.GeneralizedStarHeight.SourceSchedule.innerD_ge line 209
  21. lemma OAI.GeneralizedStarHeight.SourceSchedule.innerD_bound line 213
  22. structure OAI.GeneralizedStarHeight.SourceSchedule.Early line 218
  23. lemma OAI.GeneralizedStarHeight.SourceSchedule.exists_early line 247
  24. def OAI.GeneralizedStarHeight.ObservedInner.table line 285
  25. def OAI.GeneralizedStarHeight.ObservedInner.Certificate line 291
  26. structure OAI.GeneralizedStarHeight.ObservedInner.Prefix line 295
  27. structure OAI.GeneralizedStarHeight.ObservedInner.Suffix line 301
  28. lemma OAI.GeneralizedStarHeight.ObservedInner.prefix_congr line 307
  29. lemma OAI.GeneralizedStarHeight.ObservedInner.suffix_congr line 321
  30. lemma OAI.GeneralizedStarHeight.ObservedInner.pair_sound line 334
  31. lemma OAI.GeneralizedStarHeight.ObservedInner.available line 349
  32. lemma OAI.GeneralizedStarHeight.ObservedInner.linear_part line 362