OAI/Computability/PerfectCompleteness/Machines/CircuitFinish.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Tape line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Tape.enumList line 20

    Source documentation

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

    protected abbrev Tape.enumList : List Tape := [.current, .freeInputs, .root, .reversedRecords,
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Tape

  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Tape.enumList_getElem?_ctorIdx_eq line 23
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Tape.enumList_nodup line 27
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.(instance at line 29) line 29
  6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Label line 33
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Label.enumList line 39

    Source documentation

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

    protected abbrev Label.enumList : List Label := [.copyOut, .copyBack, .cancel, .records, .rootOut,
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Label

  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Label.enumList_getElem?_ctorIdx_eq line 42
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Label.enumList_nodup line 46
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.(instance at line 48) line 48
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Alphabet line 52
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.State line 53
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.memory line 55
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.update_current line 65
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.update_freeInputs line 68
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.update_root line 71
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.update_reversedRecords line 74
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.update_output line 77
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.update_gateCount line 80
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.update_scratch line 83
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.cancelLoop line 89
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.program line 95
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.appendTrace line 116
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.prependTrace line 120
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.cancelStep_zero line 178
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.cancelStep_succ line 188
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.cancelTrace line 199
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.initialTapes line 222
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.finalTapes line 225
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.totalTime line 228
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.finishTrace line 232
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.finalTapes_output line 279
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.finalTapes_clean line 282
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.totalTime_eq line 286
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.totalTime_le line 291
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.circuit_finalTapes line 297
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.circuitTrace line 305
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.circuitInTime line 315
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.placedCircuitInTime line 325