OAI/Computability/UniqueGames/Machines/MachineUnaryEqualityBit.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet line 14
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.State line 15
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.clean line 17
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.compareStateEquiv line 20

    Source documentation

    Reassociate the actual three comparison registers into the shared state.

    def compareStateEquiv (A : Type) : MachineCompare.State A ≃ State A where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.State

  5. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Label line 26
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList line 32
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_getElem?_ctorIdx_eq line 35
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_nodup line 39
  9. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.(instance at line 41) line 41
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.exitAt line 45
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.bitEncoding line 50
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.emit line 53

    Source documentation

    Two fixed exits, each containing only literal push instructions.

    def emit (destination : K) (bit : Bool) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (State A) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.State

  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.instruction line 58
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.copySteps line 76
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.compareSteps line 77
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.steps line 78
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.steps_le line 80
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.encodeWord_eq_iff line 84
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.emit_step line 93
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.joinTrace line 105
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.equalityTrace line 111

    Source documentation

    Actual execution of the two copies, the translated comparison, and the literal bit writer, inside any program containing the stated instructions.

    theorem equalityTrace (tape : Fin 6 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.State

  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime line 214

    Source documentation

    Timed correctness has only concrete input-tape and instruction premises.

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

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.State

  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.machine line 233
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.machineInTime line 244