OAI/Combinatorics/UniformKServer/TierLifetimes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual tier lifetimes on one fixed finite independent tape. The chronological schedule is formed before this tape and is not redefined by realized survival.

  1. abbrev OAI.UniformKServer.TierLifetimes.Tape line 20
  2. def OAI.UniformKServer.TierLifetimes.live line 22
  3. theorem OAI.UniformKServer.TierLifetimes.live_congr line 32
  4. def OAI.UniformKServer.TierLifetimes.law line 45
  5. def OAI.UniformKServer.TierLifetimes.state line 48
  6. theorem OAI.UniformKServer.TierLifetimes.fresh_step line 55
  7. theorem OAI.UniformKServer.TierLifetimes.valid line 66
  8. theorem OAI.UniformKServer.TierLifetimes.young_present line 129
  9. theorem OAI.UniformKServer.TierLifetimes.coverage line 168