OAI/Computability/BinPacking/CookLevin/VerifierFront.lean

GitHub source file

135 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.Tape line 14
2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.Label line 15
3. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.State line 16
4. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.Alphabet line 17
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.scan line 19
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.program line 26
7. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.machine line 33
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.tapes line 44
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.cfg line 47
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.tapes_zero line 51
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.tapes_one line 54
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.tapes_two line 57
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.update_zero line 60
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.update_one line 66
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.update_two line 72
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.scanStep_nil line 78
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.scanStep_cons line 85
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.scanTrace line 93
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.startStep line 111
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.restoreTrace line 119
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.reverseCounterTrace line 135
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.prependTrace line 151
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.stopped_eq_haltList line 167
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.frameTrace line 174
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputFrame.computableInPolyTime line 200
26. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.PhasePrivate line 225
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Private line 227
28. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Layout line 231
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Label line 233
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Output line 237
31. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.privateFintype line 241
32. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.privateDecidableEq line 248
33. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.labelFintype line 255
34. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.labelDecidableEq line 262
35. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.outputFintype line 269
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.controlSlots line 276
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.headLayout line 288
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.tailLayout line 306
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.headSlots line 322
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.tailSlots line 326
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.headSlots_input line 330
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.headSlots_output line 335
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.tailSlots_input line 339
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.head_output_ne_tail line 344
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Clean line 351
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.head_clean line 354
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.head_coefficients_clean line 359
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.tail_clean_after_head line 366
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.entry line 374
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.statement line 378
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes line 388
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.steps line 395
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.timePolynomial line 399
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.steps_le_timePolynomial line 403
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.trace_trans line 414
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.trace line 418
57. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot line 446
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.outputPolynomial line 451
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot_private line 456
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot_ne_input line 469
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot_injective line 476
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_off_outputs line 496
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_input line 508
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_output line 515
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_work_clear line 534
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_ambient line 541
67. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.ProgramLabel line 548
68. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.program line 550
69. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.programTrace line 556
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.programInTime line 573
71. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Tape line 587
72. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.machineSlots line 589
73. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.machine line 592
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.machine_rawInput_preserved line 603
75. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.machineInTime line 610
76. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Clock line 619
77. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Clock.enumList line 623
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Clock.enumList_getElem?_ctorIdx_eq line 626
79. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.Clock.enumList_nodup line 630
80. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.(instance at line 632) line 632
81. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.clockPolynomial line 636
82. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.clockPolynomials line 645
83. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.clockOutput line 649
84. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.clockValue line 657
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.outputPolynomial_clockOutput line 665
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.clockPolynomial_eval line 669
87. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.clockResult_output line 675
88. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClockPreparation.clocksInTime line 683
89. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.Tape line 699
90. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.ExtraLabel line 700
91. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.Label line 701
92. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.State line 702
93. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.EmbeddedAlphabet line 703
94. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.raw line 706
95. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.stream line 707
96. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.scratch line 708
97. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.clockSlots line 709
98. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.lengthTape line 711
99. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.clockTape line 712
100. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.phase line 714
101. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.clockLabel line 715
102. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.frameStates line 718
103. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.clockStates line 724
104. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.alphabet_eq line 730
105. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.extraProgram line 736
106. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.innerExtra line 747
107. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.embeddedProgram line 752
108. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.program line 756
109. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.program_extra line 760
110. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.frameTapes line 770
111. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.framedTapes line 774
112. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.copiedTapes line 777
113. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.seedTapes line 780
114. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.preparedTapes line 784
115. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.alphabet_tapes_apply line 788
116. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.uniform_frame_tapes line 795
117. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.frameInTime line 804
118. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.copyInTime line 832
119. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.fieldInTime line 848
120. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.seed_input line 862
121. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.seed_clean line 866
122. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.clocksInTime line 871
123. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.timePolynomial line 888
124. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.prepareInTime line 891
125. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.callerInTime line 911
126. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.prepared_raw line 922
127. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.prepared_stream line 929
128. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.prepared_length line 936
129. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.prepared_clock line 943
130. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.clockOutput_surjective line 949
131. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.prepared_work_clear line 961
132. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.machine line 976
133. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.initial_configuration line 987
134. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.machineInTime line 997
135. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierFront.finite_work_alphabets line 1004