OAI/Computability/Superstring/HostNormalized.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Superstring.HostCode.filter_sum_reserve line 9
  2. def OAI.Superstring.HostCode.entryOf line 29
  3. theorem OAI.Superstring.HostCode.normalized_spec line 33
  4. def OAI.Superstring.HostCode.normalDelta line 144
  5. theorem OAI.Superstring.HostCode.normalDelta_self line 148
  6. theorem OAI.Superstring.HostCode.normalDelta_spec line 151
  7. theorem OAI.Superstring.HostCode.poly_normalDelta line 193
  8. def OAI.Superstring.HostCode.normalizeEntry line 202
  9. def OAI.Superstring.HostCode.requestPath line 204
  10. def OAI.Superstring.HostCode.requestPool line 206
  11. theorem OAI.Superstring.HostCode.poly_normalizeEntry line 210
  12. theorem OAI.Superstring.HostCode.poly_requestPath line 215
  13. theorem OAI.Superstring.HostCode.poly_requestPool line 223
  14. theorem OAI.Superstring.PeriodWord.shift_zero line 233
  15. theorem OAI.Superstring.HostCode.requestPath_spec line 246
  16. theorem OAI.Superstring.HostCode.requestPool_complete line 339
  17. abbrev OAI.Superstring.LayerArray.LayerData line 381
  18. def OAI.Superstring.LayerArray.saturateAll line 383
  19. theorem OAI.Superstring.LayerArray.saturateAll_spec line 386
  20. theorem OAI.Superstring.LayerArray.poly_saturateAll line 414