OAI/Computability/UniqueGames/Machines/MachineBinaryLiteralMachine.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.BinaryLiteralMachine.Alphabet line 18
  2. abbrev OAI.UniqueGamesTheorem.BinaryLiteralMachine.State line 19
  3. abbrev OAI.UniqueGamesTheorem.BinaryLiteralMachine.clean line 20
  4. inductive OAI.UniqueGamesTheorem.BinaryLiteralMachine.Label line 23
  5. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.searchTapes line 31

    Source documentation

    Cursor, permanent stream, key, search stream, candidate, key-copy, copy scratch, index counter, reversed output.

    def searchTapes (tape : Fin 9 → K) : Fin 6 → K
  | 0 => tape 3
  | 1 => tape 2
  | 2 => tape 4
  | 3 => tape 5
  | 4 => tape 6
  | 5 => tape 7

omit [DecidableEq K] in
  6. theorem OAI.UniqueGamesTheorem.BinaryLiteralMachine.searchTapes_injective line 40
  7. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.finish line 46
  8. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.readSign line 52
  9. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.emitSign line 60
  10. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.instruction line 66
  11. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.signWord line 86
  12. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.index line 88
  13. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.outputWord line 91
  14. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.steps line 94
  15. theorem OAI.UniqueGamesTheorem.BinaryLiteralMachine.afterMatch_length_le line 100
  16. theorem OAI.UniqueGamesTheorem.BinaryLiteralMachine.steps_le line 109
  17. theorem OAI.UniqueGamesTheorem.BinaryLiteralMachine.stepAux_finish line 125
  18. theorem OAI.UniqueGamesTheorem.BinaryLiteralMachine.joinTrace line 129
  19. theorem OAI.UniqueGamesTheorem.BinaryLiteralMachine.literalTrace line 133
  20. def OAI.UniqueGamesTheorem.BinaryLiteralMachine.literalInTime line 304

    Source documentation

    Polynomial resource bound attached to the proved literal execution.

    def literalInTime (tape : Fin 9 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit malformed : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A))
…

    Mentions: OAI.UniqueGamesTheorem.BinaryLiteralMachine.Label, OAI.UniqueGamesTheorem.BinaryLiteralMachine.Alphabet, OAI.UniqueGamesTheorem.BinaryLiteralMachine.State