OAI/Computability/UniqueGames/Machines/MachineClone100Run.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.tm line 17
2. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.emptyTapes line 20
3. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.sourceBody line 22
4. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.outputHeaders line 25
5. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.outputBody line 29
6. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.outputBits line 34
7. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.inputTapes line 38
8. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.guardTapes line 41
9. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.afterLoopTapes line 46
10. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.inputBits_eq line 51
11. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.initList_eq line 56
12. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.headers_result_eq line 69
13. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.afterLoop_reversed line 76
14. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.afterLoop_length line 81
15. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.finish_eq line 87
16. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.runInTime line 101

    Source documentation

    Actual execution from the existing input codec to the complete literal halt configuration, with the sum of the three proved phase budgets.

    def runInTime (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
        (input : SourceEncoding.Input) :
        TM2OutputsInTime (tm triples nonempty) (SourceEncoding.inputBits input)
          (some (outputBits triples input))
          (((outputBits triples input).length + 2) +
            (((2 + 3 * triples.length) * (sourceBody input).length +
                (9 + 12 * triples.length) * input.equations.length + 1) +
              (5 * input.variables + 4 * input.equations.length + 18))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.tm, OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.outputBits, OAI.UniqueGamesTheorem.Explicit.MachineClone100Run.sourceBody