OAI/Computability/Superstring/SchedulerCode.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.CollectionCode.pick line 8
  2. def OAI.Superstring.CollectionCode.without line 9
  3. def OAI.Superstring.CollectionCode.inRequests line 10
  4. def OAI.Superstring.CollectionCode.restRequests line 11
  5. def OAI.Superstring.CollectionCode.charge line 12
  6. abbrev OAI.Superstring.CollectionCode.State line 13
  7. def OAI.Superstring.CollectionCode.advance line 14
  8. theorem OAI.Superstring.CollectionCode.pick_spec line 21
  9. theorem OAI.Superstring.CollectionCode.mem_without line 32
  10. theorem OAI.Superstring.CollectionCode.without_lt line 34
  11. theorem OAI.Superstring.CollectionCode.mem_inRequests line 37
  12. theorem OAI.Superstring.CollectionCode.mem_restRequests line 40
  13. theorem OAI.Superstring.CollectionCode.sum_partition line 43
  14. theorem OAI.Superstring.CollectionCode.charge_remove line 50
  15. structure OAI.Superstring.CollectionCode.Invariant line 77
  16. def OAI.Superstring.CollectionCode.budget line 86
  17. theorem OAI.Superstring.CollectionCode.length_one_same line 89
  18. theorem OAI.Superstring.CollectionCode.Model.advance_spec line 99