OAI/Computability/MinUncut/Games/GraphCounterModel.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraTape line 10
  2. abbrev OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList line 14
  3. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_getElem?_ctorIdx_eq line 16
  4. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_nodup line 20
  5. instance OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.(instance at line 22) line 22
  6. inductive OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel line 26
  7. abbrev OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList line 31
  8. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_getElem?_ctorIdx_eq line 34
  9. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_nodup line 38
  10. instance OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.(instance at line 40) line 40
  11. abbrev OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.Tape line 44
  12. abbrev OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.Label line 45
  13. abbrev OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.Alphabet line 46
  14. abbrev OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.State line 47
  15. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.initialState line 49
  16. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockLabel line 51
  17. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockStatement line 55
  18. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.readHeader line 65
  19. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.program line 71
  20. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.machine line 89
  21. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockTapes line 100
  22. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockConfiguration line 104
  23. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockTapes_update line 108
  24. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockStatement_simulation line 115
  25. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockStep line 140
  26. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockInTime line 155
  27. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.startExtra line 165
  28. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.startMemory line 170
  29. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.startMemory_input_update line 174
  30. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.startMemory_sum_update line 182
  31. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.headerStep_zero line 190
  32. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.headerStep_succ line 204
  33. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.headerTrace line 221
  34. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.headerInTime line 238
  35. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.initialMemory line 250
  36. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.clockInitialMemory line 262
  37. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterModel.startInTime line 276
  38. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.extraTapes line 342
  39. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.frame line 347
  40. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.trace_trans line 354
  41. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.start_eq line 358
  42. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.finish_eq line 371
  43. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.drainTrace line 383
  44. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.clockCopyTrace line 400
  45. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.archiveCopyTrace line 421
  46. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.reverseTrace line 443
  47. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.finishTrace line 468
  48. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterFinish.finishInTime line 483
  49. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.rawOutput line 498
  50. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.rawInTime line 501
  51. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.count line 525
  52. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.output line 527
  53. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.rowsBits line 530
  54. theorem OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.tableBits_decomposition line 533
  55. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.outputsInTime line 537
  56. def OAI.MinUncutGames.Foundations.Complexity.GraphCounterPrefix.computableInPolyTime line 543