OAI/Computability/DirectedFeedback/Machines/PoweringMachineOuterLoop.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.Placement line 57
2. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.State line 58
3. structure OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.Ready line 60
4. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.counter line 68
5. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.counter_other line 71
6. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_vertex line 78
7. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_of_vertex line 97
8. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexStart line 103
9. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexEntry line 106
10. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.bridge line 124
11. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes line 128
12. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.steps line 136
13. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.steps_le line 142
14. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_ready line 154
15. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows line 179
16. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_ofFn line 184
17. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_all line 201
18. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_output line 208
19. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_other line 234
20. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.loopTrace line 246
21. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineOuterLoop.loopInTime line 312
22. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.Alphabet line 346
23. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.Label line 348
24. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.copyInstruction line 352
25. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.instruction line 359
26. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.program line 371
27. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.afterD line 376
28. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders line 379
29. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_output line 382
30. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_other line 386
31. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.copySteps line 390
32. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.copySteps_eq line 392
33. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.steps line 396
34. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.budget line 400
35. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.trace_trans_inline_PoweringMachineFinish line 404
36. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.traceAt line 408
37. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.trace line 457
38. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.steps_le_budget line 473
39. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_length_le line 479
40. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.steps_le_uniform line 492
41. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineFinish.execution line 506
42. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.Tape line 532
43. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.State line 535
44. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.placement line 538
45. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.inputTape line 542
46. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.outputTape line 545
47. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.headerVertices line 548
48. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.headerDarts line 549
49. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.enumeration line 551
50. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.FinishLabel line 555
51. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.Label line 557
52. instance OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.labelFintype line 560
53. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.initLabels line 564
54. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.guardLabel line 565
55. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel line 566
56. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.vertexLabels line 568
57. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.finishLabels line 571
58. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.finishEntry line 574
59. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.main line 576
60. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.program line 578
61. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.atInit line 594
62. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.atGuard line 599
63. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.atBridge line 604
64. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.atVertex line 608
65. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.atFinish line 612
66. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.machine line 618
67. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.machine_code line 629
68. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.machine_main line 632
69. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.machine_initialState line 634
70. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineGlobal.input_ne_output line 637
71. def OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra line 652
72. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_table line 657
73. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_other line 661
74. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_scratch line 666
75. def OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.preparedTapes line 671
76. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_commonRole line 677
77. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_ready line 685
78. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_start line 695
79. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_counter line 702
80. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_output line 709
81. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_vertices line 714
82. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_darts line 717
83. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.prepared_source line 721
84. def OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.preparedCfg line 724
85. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.initialGlobalTapes_eq line 729
86. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.machine_initialStacks_inline_PoweringInitializeFrame line 744
87. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.initList_eq line 751
88. theorem OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.tableBits_head line 760
89. def OAI.DFVSGames.Foundations.Complexity.PoweringInitializeFrame.initializeInTime line 764
90. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_injective line 787
91. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_output line 790
92. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.output_ne_placement line 796
93. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_placement line 800
94. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_placement line 806
95. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerVertices line 812
96. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerDarts line 816
97. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_headerDarts line 820
98. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_output line 823
99. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_output line 826
100. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_scratch line 829
101. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_scratch line 834
102. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.scratch_ne_output line 839
103. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.boolList_mpr_eq line 844
104. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_tapes line 847
105. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_eq line 854