OAI/Combinatorics/UniformKServer/TierKeyEdits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual roster edits, including the noncoverage credit. The fixed-radius values are persistent over an insertion, and retirements use the true law.

  1. abbrev OAI.UniformKServer.TierKeyEdits.RadiusTape line 21
  2. def OAI.UniformKServer.TierKeyEdits.keep line 24
  3. theorem OAI.UniformKServer.TierKeyEdits.sorted_next line 30
  4. theorem OAI.UniformKServer.TierKeyEdits.retirement_eq line 46
  5. theorem OAI.UniformKServer.TierKeyEdits.stationary line 68
  6. theorem OAI.UniformKServer.TierKeyEdits.mover line 94