OAI/Computability/PerfectCompleteness/Machines/BinaryRenameWords.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BinaryRenameWords.clauseLiterals line 14
  2. def OAI.PerfectCompleteness.BinaryRenameWords.literals line 16
  3. def OAI.PerfectCompleteness.BinaryRenameWords.token line 18
  4. def OAI.PerfectCompleteness.BinaryRenameWords.tokens line 21
  5. theorem OAI.PerfectCompleteness.BinaryRenameWords.literals_nil line 24
  6. theorem OAI.PerfectCompleteness.BinaryRenameWords.literals_cons line 26
  7. theorem OAI.PerfectCompleteness.BinaryRenameWords.literals_length line 29
  8. theorem OAI.PerfectCompleteness.BinaryRenameWords.tokens_length line 35
  9. theorem OAI.PerfectCompleteness.BinaryRenameWords.literals_names line 38
  10. theorem OAI.PerfectCompleteness.BinaryRenameWords.tokens_payloads line 43
  11. theorem OAI.PerfectCompleteness.BinaryRenameWords.token_bits line 48
  12. theorem OAI.PerfectCompleteness.BinaryRenameWords.tokens_stream line 53
  13. theorem OAI.PerfectCompleteness.BinaryRenameWords.tokens_canonical line 64
  14. theorem OAI.PerfectCompleteness.BinaryRenameWords.payload_index line 70
  15. theorem OAI.PerfectCompleteness.BinaryRenameWords.token_payload_mem line 75
  16. theorem OAI.PerfectCompleteness.BinaryRenameWords.payloadSize_tokens line 82
  17. def OAI.PerfectCompleteness.BinaryRenameWords.outputLiteral line 95
  18. def OAI.PerfectCompleteness.BinaryRenameWords.body line 99
  19. theorem OAI.PerfectCompleteness.BinaryRenameWords.encoded_clause line 102
  20. theorem OAI.PerfectCompleteness.BinaryRenameWords.encodeWords_flatMap line 110
  21. theorem OAI.PerfectCompleteness.BinaryRenameWords.encoded_body line 117
  22. theorem OAI.PerfectCompleteness.BinaryRenameWords.encoded_renamed line 130