OAI/Computability/MinUncut/Machines/MachineLazyTableRuntime.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyTableRuntime.rawProgram line 13
  2. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyTableRuntime.sourceMachine_eq line 21
  3. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyTableRuntime.cleanupTapes line 25
  4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyTableRuntime.cleanup_complete line 29
  5. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyTableRuntime.terminalRun line 33
  6. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyTableRuntime.computableInPolyTime line 43
  7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyTableRuntime.finite_alphabet line 50
  8. def OAI.MinUncutGames.Foundations.PCP.PreprocessingFinishRuntime.finish line 65
  9. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingFinishRuntime.output_eq_finish line 70
  10. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingFinishRuntime.finish_degree_positive line 74
  11. def OAI.MinUncutGames.Foundations.PCP.PreprocessingFinishRuntime.computableInPolyTime line 77
  12. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingFinishRuntime.finite_alphabet line 88
  13. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRuntime.tablePolynomialTime line 106
  14. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRuntime.finiteAlphabet line 119
  15. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.bitLength line 138
  16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.bitLength_zero line 140
  17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.bitLength_positive line 142
  18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.bitLength_half line 145
  19. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.increments line 152
  20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.increments_true line 155
  21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.increments_half line 158
  22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.increments_false line 162
  23. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.coreTime line 167
  24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.coreTime_zero line 172
  25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.coreTime_positive line 174
  26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.coreTime_bound line 178
  27. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.Alphabet line 188
  28. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.State line 189
  29. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.initialState line 191
  30. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.rawTapes line 193
  31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.update_input line 198
  32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.update_scratch line 203
  33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.update_output line 208
  34. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.stripLoop line 213
  35. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.guardLoop line 219
  36. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.halfLoop line 228
  37. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.program line 237
  38. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.machine line 244
  39. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.configuration line 255
  40. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.next line 259
  41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.stripStep_true line 261
  42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.stripStep_false line 269
  43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.stripTrace line 277
  44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.halfStep_nil line 293
  45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.halfStep_false line 301
  46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.halfStep_true line 310
  47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.halfTrace line 319
  48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.restoreTrace line 351
  49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.guardStep_zero line 368
  50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.guardStep_positive line 376
  51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.coreTrace line 388
  52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.initList_eq line 420
  53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.haltList_eq line 428
  54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.initialStep line 436
  55. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.totalTime line 445
  56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.totalTime_bound line 447
  57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.machineTrace line 452
  58. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.outputsInTime line 467
  59. def OAI.MinUncutGames.Foundations.Complexity.MachineLogCounter.computableInPolyTime line 473