OAI/Computability/StarHeight/BoundarySnapshots.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GeneralizedStarHeight.WordIntervals.product_self line 15
  2. lemma OAI.GeneralizedStarHeight.WordIntervals.product_chain line 20
  3. lemma OAI.GeneralizedStarHeight.WordIntervals.product_chain_with_ends line 34
  4. theorem OAI.GeneralizedStarHeight.ScheduleClock.exists_ordered_stencil_clock line 51
  5. lemma OAI.GeneralizedStarHeight.ClockAffine.Snapshot.ext line 106
  6. def OAI.GeneralizedStarHeight.BoundarySnapshot.Present line 118
  7. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.present_unique line 122
  8. def OAI.GeneralizedStarHeight.BoundarySnapshot.factors line 127
  9. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.factors_present line 136
  10. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.factors_absent line 147
  11. def OAI.GeneralizedStarHeight.BoundarySnapshot.actual line 156
  12. def OAI.GeneralizedStarHeight.BoundarySnapshot.later line 168
  13. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.actual_eq_substitute line 174
  14. lemma OAI.GeneralizedStarHeight.CanonicalEpisodes.Parameters.end_lower line 210
  15. lemma OAI.GeneralizedStarHeight.ClockAffine.no_off_outside line 241
  16. lemma OAI.GeneralizedStarHeight.ClockAffine.net_cut line 249
  17. def OAI.GeneralizedStarHeight.BoundarySnapshot.positions line 267
  18. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.positions_return line 270
  19. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.present_of_bounds line 276
  20. lemma OAI.GeneralizedStarHeight.BoundarySnapshot.factors_positions line 286