OAI/Combinatorics/UniformKServer/CausalRosters.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dependence of the chronological insertion/slot schedule only on past true inputs. No realized lifetime is used to decide a chronological insertion.

  1. lemma OAI.UniformKServer.CausalRosters.age_congr line 17
  2. lemma OAI.UniformKServer.CausalRosters.young_congr line 25
  3. lemma OAI.UniformKServer.CausalRosters.trigger_congr line 31
  4. lemma OAI.UniformKServer.CausalRosters.schedule line 44
  5. lemma OAI.UniformKServer.CausalRosters.reserved line 60
  6. lemma OAI.UniformKServer.CausalRosters.birth line 67
  7. lemma OAI.UniformKServer.CausalRosters.labels line 79