OAI/Computability/DirectedFeedback/Machines/Label.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.Label line 54
  2. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.copyExit line 69
  3. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.clearTape line 73
  4. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.clearEntry line 77
  5. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.program line 80
  6. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.machine line 100
  7. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.frame line 111
  8. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cfg line 117
  9. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.frame_core line 122
  10. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.bodyPlacement line 126
  11. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerAux line 135
  12. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerAux_empty line 141
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerPlacement line 145
  14. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.inputData line 172
  15. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerData line 185
  16. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerStacks line 188
  17. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerTrace line 192
  18. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldData line 211
  19. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.originalData_eq line 214
  20. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldBodyTrace line 217
  21. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.counterStacks line 232
  22. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.frame_oldFuel line 235
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.frame_ownerFuel line 239
  24. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_oldFuel line 243
  25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_ownerFuel line 254
  26. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_global line 265
  27. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_owner line 278
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardStep line 291
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardExit line 305
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldIncrementStep line 316
  31. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefix line 330
  32. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed line 333
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.joinTrace_inline_MachineRegularTable line 340
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefixTrace line 344
  35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopTrace line 375
  36. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.frame_scratch line 387
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.frame_darts line 391
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.frame_header_n line 394
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldSeedStep line 398
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.copyOldTrace line 411
  41. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldStageTrace line 426
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_offset line 436
  43. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerData line 449
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerSeedStep line 457
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.copyOwnerTrace line 475
  46. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerPlacement line 489
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerInitialData_eq line 501
  48. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerBodyTrace line 504
  49. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardStep line 520
  50. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardExit line 534
  51. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerIncrementStep line 545
  52. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefix line 565
  53. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed line 568
  54. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefixTrace line 575
  55. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopTrace line 605
  56. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerStageTrace line 617
  57. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.owner_output_eq_ownerPrefix line 627
  58. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleaned line 643
  59. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime line 648
  60. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.drainTrace line 653
  61. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleanupPrefixTrace line 661
  62. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTrace line 675
  63. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.finalStacks line 681
  64. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_finalStacks line 684
  65. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_length_le line 704
  66. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_le line 718
  67. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_final_le line 734
  68. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerOutput line 798
  69. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldOutput line 801
  70. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput line 804
  71. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.totalTime line 807
  72. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.old_output_eq_originalPrefix line 813
  73. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput_eq line 818
  74. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.joinTraceRegularTableTrace_inline_MachineRegularTableTrace line 846
  75. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.normalizeEmptyAppend_inline_MachineRegularTableTrace line 850
  76. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerStartTrace line 854
  77. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerOldTrace line 866
  78. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.beforeCleanupTrace line 882
  79. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.cleanupFinalTrace line 898
  80. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.fullTrace line 906
  81. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_output line 914
  82. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.input_stacks_eq line 927
  83. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.initial_cfg_eq line 949
  84. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.trace line 957