OAI/Computability/UniqueGames/Machines/MachineBinaryRenameMachine.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

The finite Boolean-stack driver for first-occurrence renaming. Its permanent input is copied to a cursor, each literal is translated by the checked search loop, and the physical output is restored, prefixed with its count headers, and cleaned up. Every tape uses Bool and every control component is finite.

  1. abbrev OAI.UniqueGamesTheorem.BinaryRenameMachine.Tape line 23
  2. abbrev OAI.UniqueGamesTheorem.BinaryRenameMachine.Alphabet line 24
  3. abbrev OAI.UniqueGamesTheorem.BinaryRenameMachine.State line 25
  4. inductive OAI.UniqueGamesTheorem.BinaryRenameMachine.Label line 27
  5. def OAI.UniqueGamesTheorem.BinaryRenameMachine.loopTapes line 34
  6. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.loopTapes_injective line 36
  7. def OAI.UniqueGamesTheorem.BinaryRenameMachine.program line 41
  8. abbrev OAI.UniqueGamesTheorem.BinaryRenameMachine.machine line 54
  9. def OAI.UniqueGamesTheorem.BinaryRenameMachine.tapes line 65
  10. def OAI.UniqueGamesTheorem.BinaryRenameMachine.cfg line 75
  11. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.initList_eq line 80
  12. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.haltList_eq line 87
  13. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.copyTrace line 94
  14. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.restoreTrace line 111
  15. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.headerTrace line 132
  16. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.cleanupTrace line 156
  17. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.outputBody_eq line 174
  18. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.loopTrace line 189
  19. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.joinTrace line 232
  20. def OAI.UniqueGamesTheorem.BinaryRenameMachine.steps line 236
  21. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.renameTrace line 243
  22. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.clause_count_le_stream line 262
  23. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.body_length_le line 267
  24. def OAI.UniqueGamesTheorem.BinaryRenameMachine.timePolynomial line 278
  25. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.steps_le line 282
  26. def OAI.UniqueGamesTheorem.BinaryRenameMachine.outputsInTime line 302
  27. def OAI.UniqueGamesTheorem.BinaryRenameMachine.tokenComputation line 312

    Source documentation

    The token-stream phase has a displayed finite machine and actual execution bound; its polynomial argument is the token stream's physical bit length.

    noncomputable def tokenComputation :
    TM2ComputableInPolyTime (fun formula : BinaryFormula.Formula =>
      BinaryTokenMachine.tokens formula.clauses) formulaBits BinaryOccurrenceRename.renamed where
…

    Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Formula, OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens, OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed

  28. def OAI.UniqueGamesTheorem.BinaryRenameMachine.preprocessing line 327

    Source documentation

    Repackage the checked marker-removal machine without changing any machine or word: the intermediate semantic value is the same formula.

    noncomputable def preprocessing :
    TM2ComputableInPolyTime BinaryEncoding.formulaBits
      (fun formula : BinaryFormula.Formula => BinaryTokenMachine.tokens formula.clauses)
      (id : BinaryFormula.Formula → BinaryFormula.Formula) where
…

    Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits, OAI.UniqueGamesTheorem.BinaryFormula.Formula, OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens

  29. def OAI.UniqueGamesTheorem.BinaryRenameMachine.computableInPolyTime line 339

    Source documentation

    Actual finite-alphabet polynomial-time sparse binary to dense unary renaming. Sparse name magnitudes are never expanded in unary.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime BinaryEncoding.formulaBits formulaBits
      BinaryOccurrenceRename.renamed :=
…

    Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits, OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed

  30. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.machine_finiteAlphabet line 344
  31. theorem OAI.UniqueGamesTheorem.BinaryRenameMachine.computation_finiteAlphabet line 348