OAI/Combinatorics/UniformKServer/TapeController.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.TapeController.Tape line 14
  2. structure OAI.UniformKServer.TapeController.State line 16
  3. instance OAI.UniformKServer.TapeController.(instance at line 21) line 21
  4. def OAI.UniformKServer.TapeController.initial line 29
  5. def OAI.UniformKServer.TapeController.boundary line 32
  6. instance OAI.UniformKServer.TapeController.(instance at line 35) line 35
  7. def OAI.UniformKServer.TapeController.chosen line 38
  8. def OAI.UniformKServer.TapeController.choose line 41
  9. def OAI.UniformKServer.TapeController.step line 46
  10. theorem OAI.UniformKServer.TapeController.step_seen line 59
  11. def OAI.UniformKServer.TapeController.expected line 69
  12. def OAI.UniformKServer.TapeController.loaded line 78
  13. theorem OAI.UniformKServer.TapeController.step_loaded line 81
  14. theorem OAI.UniformKServer.TapeController.loaded_cons line 88
  15. theorem OAI.UniformKServer.TapeController.fresh_mean line 102