OAI/Computability/UniqueGames/Machines/MachineBinaryRenameWords.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The word-level correspondence used by the ordinary-binary renaming machine. Literal occurrences stay in clause order, and equality is tested on canonical binary payloads. The output body consists of the first occurrence index and the sign of every literal, in the inherited dense formula codec.

  1. def OAI.UniqueGamesTheorem.BinaryRenameWords.clauseLiterals line 21
  2. def OAI.UniqueGamesTheorem.BinaryRenameWords.literals line 23
  3. def OAI.UniqueGamesTheorem.BinaryRenameWords.token line 25
  4. def OAI.UniqueGamesTheorem.BinaryRenameWords.tokens line 28
  5. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.literals_nil line 31
  6. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.literals_cons line 33
  7. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.literals_length line 36
  8. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.tokens_length line 42
  9. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.literals_names line 45
  10. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.tokens_payloads line 50
  11. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.token_bits line 55
  12. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.tokens_stream line 61

    Source documentation

    The marker-removal machine's actual output is the search machine's stream.

    theorem tokens_stream (cs : List Clause) :
    BinaryNameSearch.stream (tokens cs) = BinaryTokenMachine.tokens cs := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameSearch.stream, OAI.UniqueGamesTheorem.BinaryRenameWords.tokens, OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens

  13. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.tokens_canonical line 72
  14. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.payload_index line 78
  15. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.token_payload_mem line 83
  16. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.payloadSize_tokens line 90
  17. def OAI.UniqueGamesTheorem.BinaryRenameWords.outputLiteral line 103
  18. def OAI.UniqueGamesTheorem.BinaryRenameWords.body line 107
  19. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.encoded_clause line 110
  20. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.encodeWords_flatMap line 118
  21. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.encoded_body line 126

    Source documentation

    The output contains every literal occurrence, including repetitions.

    theorem encoded_body (F : Formula) :
    Complexity.encodeWords ((BinaryOccurrenceRename.renamed F).clauses.flatMap
      Complexity.clauseWords) = body F := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed, OAI.UniqueGamesTheorem.BinaryRenameWords.body

  22. theorem OAI.UniqueGamesTheorem.BinaryRenameWords.encoded_renamed line 140

    Source documentation

    Exact ordinary-binary-machine target, including its two count headers.

    theorem encoded_renamed (F : Formula) :
    Complexity.formulaBits (BinaryOccurrenceRename.renamed F) =
      Complexity.encodeWord (3 * F.clauses.length) ++
        Complexity.encodeWord F.clauses.length ++ body F := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed, OAI.UniqueGamesTheorem.BinaryRenameWords.body