OAI/Combinatorics/UniformKServer/EpochControl.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniformKServer.EpochControl.State line 13
  2. def OAI.UniformKServer.EpochControl.asRaw line 20
  3. def OAI.UniformKServer.EpochControl.initial line 23
  4. def OAI.UniformKServer.EpochControl.label line 26
  5. def OAI.UniformKServer.EpochControl.step line 32
  6. def OAI.UniformKServer.EpochControl.runTrace line 44
  7. theorem OAI.UniformKServer.EpochControl.rawChoice_congr line 49
  8. theorem OAI.UniformKServer.EpochControl.rawStep_congr line 55
  9. theorem OAI.UniformKServer.EpochControl.fallbackTrace line 63
  10. theorem OAI.UniformKServer.EpochControl.normalTrace line 79
  11. theorem OAI.UniformKServer.EpochControl.initial_trace line 113