OAI/Computability/UniqueGames/Machines/MachineUnaryAddAt.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.Alphabet line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.finish line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.loop line 23

    Source documentation

    A fixed finite statement; arithmetic is performed by the physical unary tapes.

    def loop (source destination : K) (loopLabel : Λ) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.Alphabet

  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.loopPushBound line 33
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.unaryTapes line 38

    Source documentation

    A caller's tape frame with the two unary prefixes and their unread suffixes.

    def unaryTapes (source destination : K) (base : K → List Bool) (a b : Nat)
    (sourceSuffix destinationSuffix : List Bool) : K → List Bool :=
…
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_source line 43
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_destination line 49
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_other line 55
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.update_source line 62
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.update_destination line 75
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.stepAux_true line 85
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.stepAux_false line 95

    Source documentation

    The zero branch restores the delimiter, clears the register, and exits.

    theorem stepAux_false (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ) (base : K → List Bool)
    (input output : List Bool) (ambient : σ) (register : Option Bool) :
    TM2.stepAux (loop source destination loopLabel exit) (ambient, register)
      (tapesAt source destination base (false :: input) output) =
      ⟨exit, (ambient, none), tapesAt source destination base (false :: input) output⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.loop

  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.stepAux_succ line 103
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.stepAux_zero line 114
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.step_succ line 126
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.step_zero line 140
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.addTrace line 155

    Source documentation

    Exactly a positive-bit transitions followed by the delimiter transition.

    theorem addTrace (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.Alphabet

  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.addFromTapes line 180

    Source documentation

    The same actual execution from a caller's supplied tape configuration.

    theorem addFromTapes (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.Alphabet

  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.addInTime line 201

    Source documentation

    A composable time witness whose stored transition count is exactly a + 1.

    def addInTime (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.Alphabet

  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.addInTime_steps line 219