OAI/Computability/UniqueGames/PCP/Setup.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Alphabet line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Ports line 17
  3. inductive OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Label line 19
  4. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Label.enumList line 24
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Label.enumList_getElem?_ctorIdx_eq line 27
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Label.enumList_nodup line 31
  7. instance OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.(instance at line 33) line 33
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.statement line 37
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.resultTapes line 56
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.resultTapes_other line 65
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.setupInTime line 73

    Source documentation

    Actual program placement is the only execution premise. Header values and unread row bits specify the input, and every auxiliary role starts empty.

    def setupInTime (ports : Ports K) (distinct : Function.Injective ports)
    (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Ports, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Alphabet

  12. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.tableSetupInTime line 165

    Source documentation

    Specialization to the checked graph-table codec. The bound follows from the actual copy and delimiter-scan traces above.

    def tableSetupInTime {q : Nat} (ports : Ports K) (distinct : Function.Injective ports)
    (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Ports, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.Alphabet

  13. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.program line 192
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.machine line 196

    Source documentation

    This stage itself has only seven tapes and nine control labels.

    def machine : FinTM2 where
…