OAI/Computability/PerfectCompleteness/Foundations/CanonicalVertexNames.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CanonicalVertexNames.payload line 19
  2. theorem OAI.PerfectCompleteness.CanonicalVertexNames.payload_injective line 21
  3. theorem OAI.PerfectCompleteness.CanonicalVertexNames.finalDigit_append_true line 25
  4. theorem OAI.PerfectCompleteness.CanonicalVertexNames.payload_canonical line 31
  5. theorem OAI.PerfectCompleteness.CanonicalVertexNames.payload_length line 35
  6. def OAI.PerfectCompleteness.CanonicalVertexNames.tokens line 39
  7. theorem OAI.PerfectCompleteness.CanonicalVertexNames.tokens_length line 42
  8. theorem OAI.PerfectCompleteness.CanonicalVertexNames.tokens_payloads line 46
  9. theorem OAI.PerfectCompleteness.CanonicalVertexNames.payload_mem line 50
  10. theorem OAI.PerfectCompleteness.CanonicalVertexNames.tokens_canonical line 55
  11. def OAI.PerfectCompleteness.CanonicalVertexNames.name line 61
  12. theorem OAI.PerfectCompleteness.CanonicalVertexNames.name_val line 66
  13. theorem OAI.PerfectCompleteness.CanonicalVertexNames.name_eq_iff line 70
  14. theorem OAI.PerfectCompleteness.CanonicalVertexNames.name_injective line 80
  15. def OAI.PerfectCompleteness.CanonicalVertexNames.embedding line 85
  16. def OAI.PerfectCompleteness.CanonicalVertexNames.payloadBound line 88
  17. theorem OAI.PerfectCompleteness.CanonicalVertexNames.payload_length_le line 91
  18. theorem OAI.PerfectCompleteness.CanonicalVertexNames.payloadSize_le line 103
  19. theorem OAI.PerfectCompleteness.CanonicalVertexNames.stream_length_le line 121
  20. def OAI.PerfectCompleteness.CanonicalVertexNames.searchInTime line 138