OAI/Computability/Superstring/HostComplete.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.HostCode.completePool line 9
  2. theorem OAI.Superstring.HostCode.completePool_complete line 13
  3. theorem OAI.Superstring.HostCode.poly_completePool line 66
  4. abbrev OAI.Superstring.CollectionCode.Request line 79
  5. def OAI.Superstring.CollectionCode.Request.source line 81
  6. def OAI.Superstring.CollectionCode.Request.target line 82
  7. def OAI.Superstring.CollectionCode.Request.members line 83
  8. def OAI.Superstring.CollectionCode.Request.code line 84
  9. def OAI.Superstring.CollectionCode.Request.reserve line 85
  10. def OAI.Superstring.CollectionCode.Request.ids line 86
  11. def OAI.Superstring.CollectionCode.Request.entry line 87
  12. structure OAI.Superstring.CollectionCode.RequestWitness line 94
  13. def OAI.Superstring.CollectionCode.ValidRequest line 110
  14. theorem OAI.Superstring.CollectionCode.RequestWitness.later line 116
  15. def OAI.Superstring.CollectionCode.RequestWitness.hosted line 126
  16. def OAI.Superstring.CollectionCode.RequestWitness.request line 145
  17. theorem OAI.Superstring.CollectionCode.RequestWitness.data_rep line 163
  18. theorem OAI.Superstring.CollectionCode.RequestWitness.entry_eq line 169
  19. abbrev OAI.Superstring.CollectionCode.Plan line 181
  20. def OAI.Superstring.CollectionCode.planBudget line 182
  21. def OAI.Superstring.CollectionCode.hardPlan line 183
  22. def OAI.Superstring.CollectionCode.Covered line 186
  23. def OAI.Superstring.CollectionCode.GoodPlan line 189
  24. theorem OAI.Superstring.CollectionCode.Model.hardPlan_spec line 194