OAI/Computability/Superstring/SchedulerMachine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Superstring.CollectionCode.Context line 8
  2. abbrev OAI.Superstring.CollectionCode.Input line 9
  3. def OAI.Superstring.CollectionCode.iterStep line 10
  4. def OAI.Superstring.CollectionCode.schedulerCapacity line 11
  5. def OAI.Superstring.CollectionCode.sweep line 14
  6. theorem OAI.Superstring.CollectionCode.iterate_iterStep line 19
  7. theorem OAI.Superstring.CollectionCode.Model.state_size line 27
  8. theorem OAI.Superstring.CollectionCode.Model.sweep_spec line 48
  9. theorem OAI.Superstring.CollectionCode.poly_gs line 98
  10. theorem OAI.Superstring.CollectionCode.poly_pick line 100
  11. theorem OAI.Superstring.CollectionCode.poly_without line 107
  12. theorem OAI.Superstring.CollectionCode.poly_inRequests line 111
  13. theorem OAI.Superstring.CollectionCode.poly_restRequests line 115
  14. theorem OAI.Superstring.CollectionCode.poly_charge line 119
  15. theorem OAI.Superstring.CollectionCode.poly_requestReserve line 121
  16. theorem OAI.Superstring.CollectionCode.poly_planBudget line 125
  17. theorem OAI.Superstring.CollectionCode.poly_budget line 134
  18. theorem OAI.Superstring.CollectionCode.poly_extraSizes line 140
  19. theorem OAI.Superstring.CollectionCode.poly_maxExtras line 149
  20. theorem OAI.Superstring.CollectionCode.poly_initial line 153
  21. theorem OAI.Superstring.CollectionCode.poly_advance line 154
  22. theorem OAI.Superstring.CollectionCode.poly_schedulerStep line 165
  23. theorem OAI.Superstring.CollectionCode.poly_schedulerCapacity line 167
  24. theorem OAI.Superstring.CollectionCode.poly_sweep line 172
  25. def OAI.Superstring.CollectionCode.tour line 186
  26. theorem OAI.Superstring.CollectionCode.poly_tour line 189
  27. theorem OAI.Superstring.CollectionCode.Model.tour_spec line 197