OAI/Combinatorics/UniformKServer/EpochSide.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact side configuration of a marked held-vector epoch. An unmarked star has the actual empty side domain.

  1. def OAI.UniformKServer.EpochSide.active line 18
  2. def OAI.UniformKServer.EpochSide.config line 23
  3. theorem OAI.UniformKServer.EpochSide.mem line 31
  4. theorem OAI.UniformKServer.EpochSide.valid line 41
  5. theorem OAI.UniformKServer.EpochSide.size_formula line 54
  6. theorem OAI.UniformKServer.EpochSide.size_same line 71
  7. def OAI.UniformKServer.EpochSide.param line 78
  8. theorem OAI.UniformKServer.EpochSide.schedule_valid line 81