OAI/Computability/Superstring/FibreSelect.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.BitCode.firstGood line 7
  2. theorem OAI.Superstring.BitCode.firstGood_mem line 8
  3. def OAI.Superstring.CollectionCode.fibreCheck line 23
  4. def OAI.Superstring.CollectionCode.fibreSelect line 26
  5. theorem OAI.Superstring.CollectionCode.Model.fibreSelect_spec line 29
  6. theorem OAI.Superstring.CollectionCode.poly_request_reserve line 56
  7. theorem OAI.Superstring.CollectionCode.poly_request_ids line 60
  8. theorem OAI.Superstring.CollectionCode.poly_request_entry line 65
  9. theorem OAI.Superstring.CollectionCode.poly_entries line 69
  10. theorem OAI.Superstring.CollectionCode.poly_requestedData line 78
  11. theorem OAI.Superstring.CollectionCode.poly_fibrePool line 85
  12. theorem OAI.Superstring.CollectionCode.poly_fibreCheck line 88
  13. theorem OAI.Superstring.CollectionCode.poly_fibreSelect line 100
  14. def OAI.Superstring.CollectionCode.fibre line 113
  15. def OAI.Superstring.CollectionCode.recipients line 114
  16. def OAI.Superstring.CollectionCode.incoming line 116
  17. theorem OAI.Superstring.CollectionCode.mem_fibre line 120
  18. theorem OAI.Superstring.CollectionCode.fibre_ne line 124
  19. theorem OAI.Superstring.CollectionCode.mem_recipients line 132
  20. theorem OAI.Superstring.CollectionCode.nodup_recipients line 136
  21. theorem OAI.Superstring.CollectionCode.sum_indicator line 140
  22. theorem OAI.Superstring.CollectionCode.fibre_sum line 157
  23. theorem OAI.Superstring.CollectionCode.Model.incoming_spec line 175
  24. def OAI.Superstring.CollectionCode.baseIndex line 227
  25. def OAI.Superstring.CollectionCode.holes line 228
  26. def OAI.Superstring.CollectionCode.prepare line 229
  27. def OAI.Superstring.CollectionCode.process line 238
  28. theorem OAI.Superstring.CollectionCode.maxFold_mem line 243
  29. theorem OAI.Superstring.CollectionCode.base_mem line 253
  30. theorem OAI.Superstring.CollectionCode.mem_holes line 261
  31. theorem OAI.Superstring.CollectionCode.holes_length line 264
  32. theorem OAI.Superstring.CollectionCode.Model.prepare_spec line 277
  33. theorem OAI.Superstring.CollectionCode.Model.process_spec line 347