OAI/Computability/StarHeight/AffineClock.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.ClockAffine.Edge line 21
  2. def OAI.GeneralizedStarHeight.ClockAffine.offChoice line 24
  3. lemma OAI.GeneralizedStarHeight.ClockAffine.offChoice_some line 27
  4. lemma OAI.GeneralizedStarHeight.ClockAffine.offChoice_none line 43
  5. lemma OAI.GeneralizedStarHeight.ClockAffine.offChoice_of_offedge line 51
  6. lemma OAI.GeneralizedStarHeight.ClockAffine.edge_add line 62
  7. def OAI.GeneralizedStarHeight.ClockAffine.productTable line 72
  8. structure OAI.GeneralizedStarHeight.ClockAffine.Factors line 75
  9. structure OAI.GeneralizedStarHeight.ClockAffine.Snapshot line 80
  10. def OAI.GeneralizedStarHeight.ClockAffine.shift line 88
  11. def OAI.GeneralizedStarHeight.ClockAffine.update line 95
  12. lemma OAI.GeneralizedStarHeight.ClockAffine.update_off line 98
  13. lemma OAI.GeneralizedStarHeight.ClockAffine.update_main line 104
  14. lemma OAI.GeneralizedStarHeight.ClockAffine.update_periodic line 109
  15. lemma OAI.GeneralizedStarHeight.ClockAffine.independent_pair line 114
  16. structure OAI.GeneralizedStarHeight.ClockAffine.Later line 131
  17. def OAI.GeneralizedStarHeight.ClockAffine.Later.substitute line 136
  18. def OAI.GeneralizedStarHeight.ClockAffine.hypothetical line 145
  19. lemma OAI.GeneralizedStarHeight.ClockAffine.hypothetical_at line 150
  20. lemma OAI.GeneralizedStarHeight.ClockAffine.hypothetical_actual line 155