OAI/Computability/MinUncut/Machines/MachineCanonicalOutput.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.Program line 10
  2. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.extendedLabel line 21
  3. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.extendedCfg line 25
  4. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.extendedStmt line 30
  5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.stepAux_extended line 48
  6. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.sourceMachine line 72
  7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.Label line 83
  8. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.cleanupLabel line 85
  9. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.resetLabel line 88
  10. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry line 90
  11. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.completedProgram line 93
  12. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.completedMachine line 100
  13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.finiteAlphabet line 111
  14. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.embeddedCfg line 116
  15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.step_simulation line 120
  16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.embedded_init line 135
  17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.finalTapes_eq line 140
  18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.haltList_eq line 151
  19. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.cleanupExecution line 156
  20. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.outputsInTime line 186
  21. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.completedTime line 211
  22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.completedTime_eval line 216
  23. structure OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun line 223
  24. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime line 230
  25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime_finite_alphabet line 249
  26. def OAI.MinUncutGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTimeOfEnumeration line 260