OAI/Computability/PerfectCompleteness/Machines/PayloadPresenceMachine.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Alphabet line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Ports line 16
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.presenceMap line 18
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.closing_distinct line 21
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.closurePorts line 25
  6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext line 28
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext.enumList line 33

    Source documentation

    A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.)

    protected abbrev CopyContext.enumList : List CopyContext := [.remaining, .threshold, .closing]

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext

  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext.enumList_getElem?_ctorIdx_eq line 35
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext.enumList_nodup line 39
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.(instance at line 41) line 41
  11. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Label line 45
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.presenceLabels line 52
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copySource line 55
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copyTarget line 59
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copyExit line 64
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.statement line 69
  17. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Ready line 82
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Ready.emitted line 87
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.working line 96
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.steps line 101
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.chain line 105
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copyTrace line 109
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.trace line 134
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.steps_le line 247
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.inTime line 252