OAI/Combinatorics/UniformKServer/RawGlobal.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.RawGlobal.S line 13
  2. def OAI.UniformKServer.RawGlobal.state line 15
  3. def OAI.UniformKServer.RawGlobal.initial line 17
  4. def OAI.UniformKServer.RawGlobal.chosen line 18
  5. def OAI.UniformKServer.RawGlobal.boundary line 19
  6. def OAI.UniformKServer.RawGlobal.label line 21
  7. def OAI.UniformKServer.RawGlobal.step line 24
  8. theorem OAI.UniformKServer.RawGlobal.initial_state line 29
  9. theorem OAI.UniformKServer.RawGlobal.chosen_state line 38
  10. theorem OAI.UniformKServer.RawGlobal.boundary_state line 44
  11. theorem OAI.UniformKServer.RawGlobal.label_state line 53
  12. theorem OAI.UniformKServer.RawGlobal.step_state line 62
  13. theorem OAI.UniformKServer.RawGlobal.primitive_initial line 86
  14. theorem OAI.UniformKServer.RawGlobal.primitive_chosen line 88
  15. theorem OAI.UniformKServer.RawGlobal.primitive_boundary line 92
  16. theorem OAI.UniformKServer.RawGlobal.primitive_label line 95
  17. theorem OAI.UniformKServer.RawGlobal.primitive_step line 98