OAI/Computability/Superstring/RequestAttachment.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.WindowCode.requestAttachment line 8
  2. theorem OAI.Superstring.WindowCode.requestAttachment_realizes line 11
  3. theorem OAI.Superstring.WindowCode.poly_requestAttachment line 36
  4. theorem OAI.Superstring.WalkCode.realizes_spec line 46
  5. abbrev OAI.Superstring.HostCode.RequestData line 57
  6. def OAI.Superstring.HostCode.attachment line 59
  7. def OAI.Superstring.HostCode.raw line 62
  8. theorem OAI.Superstring.HostCode.raw_spec line 66
  9. theorem OAI.Superstring.HostCode.poly_attachment line 134
  10. theorem OAI.Superstring.HostCode.poly_raw line 138
  11. def OAI.Superstring.PeriodWord.shift line 155
  12. theorem OAI.Superstring.PeriodWord.length_shift line 156
  13. theorem OAI.Superstring.PeriodWord.text_shift line 159
  14. theorem OAI.Superstring.PeriodWord.poly_shift line 170
  15. abbrev OAI.Superstring.HostCode.Entry line 178
  16. def OAI.Superstring.HostCode.Entry.tag line 180
  17. def OAI.Superstring.HostCode.Entry.word line 181
  18. def OAI.Superstring.HostCode.Entry.start line 182
  19. def OAI.Superstring.HostCode.Entry.stop line 183
  20. def OAI.Superstring.HostCode.Entry.req line 184
  21. def OAI.Superstring.HostCode.Entry.target line 185
  22. def OAI.Superstring.HostCode.Entry.shift line 187
  23. def OAI.Superstring.HostCode.later line 191
  24. def OAI.Superstring.HostCode.normalized line 193
  25. theorem OAI.Superstring.HostCode.Entry.poly_tag line 198
  26. theorem OAI.Superstring.HostCode.Entry.poly_word line 200
  27. theorem OAI.Superstring.HostCode.Entry.poly_start line 202
  28. theorem OAI.Superstring.HostCode.Entry.poly_stop line 204
  29. theorem OAI.Superstring.HostCode.Entry.poly_req line 206
  30. theorem OAI.Superstring.HostCode.Entry.poly_target line 208
  31. theorem OAI.Superstring.HostCode.Entry.poly_shift line 212
  32. theorem OAI.Superstring.HostCode.poly_later line 216
  33. theorem OAI.Superstring.HostCode.poly_normalized line 220
  34. theorem OAI.Superstring.Hierarchical.hosted_targets_chain line 238
  35. theorem OAI.Superstring.Hierarchical.hosted_target_bounds line 280