OAI/Computability/BinPacking/Information/SourceLoopInit.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.discardFieldsTrace line 15
2. inductive OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.Tape line 58
3. inductive OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.Label line 62
4. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.fieldDestination line 68
5. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.readStart line 69
6. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.readLoop line 70
7. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.skipLabel line 71
8. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.headerLabel line 72
9. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.program line 75
10. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.machine line 92
11. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.atSkip line 103
12. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.atReadStart line 107
13. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.atReadLoop line 111
14. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.atReadDone line 116
15. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.discardHeadersTrace line 119
16. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.discardSixTrace line 131
17. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.readSixTrace line 141
18. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.scanTapes line 157
19. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.scanTapes_work line 161
20. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.scanTapes_index line 165
21. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.scanTapes_other line 170
22. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.update_scanTapes_work line 175
23. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.skipClausesTrace line 182
24. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_eq line 230
25. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_injective_below line 236
26. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.readSix_output_field line 242
27. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.readSix_output_work line 254
28. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.readSix_output_frame line 262
29. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.outputTapes line 270
30. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.scanSteps line 276
31. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.scanReadTrace line 282
32. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.lookupSteps line 310
33. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitTrace line 314
34. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.output_formula line 344
35. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.output_index line 350
36. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.output_work line 356
37. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.output_field line 362
38. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.output_frame line 369
39. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.clauseWords_six line 376
40. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.fieldWords line 382
41. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.output_fieldWords line 386
42. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.lookupSteps_le_input line 392
43. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.timePolynomial line 411
44. theorem OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.timePolynomial_eval line 413
45. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitInTime line 416
46. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.lookupInTime line 436
47. def OAI.BinPackingGames.Foundations.Hastad.SourceClauseLookup.machineInTime line 455
48. inductive OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.Tape line 475
49. inductive OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.Label line 482
50. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.place line 491
51. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.fill line 495
52. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.fill_place line 502
53. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.fill_self line 507
54. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.fill_update line 517
55. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.placedLabel line 526
56. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.placedConfiguration line 530
57. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.placedStatement line 536
58. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.placed_stepAux line 548
59. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.nextLabel line 573
60. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.program line 576
61. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.placed_step line 587
62. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.lookupOutput line 604
63. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.placedLookupInTime line 609
64. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.copiedTapes line 625
65. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.coordinateOutput line 628
66. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.cleanup_lookupOutput line 636
67. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_current line 665
68. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_remaining line 670
69. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_field line 675
70. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_other_field line 682
71. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.suffix_length_le_input line 687
72. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.coordinateInTime line 699
73. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.labelAt line 744
74. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.nextLabel_eq line 747
75. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.stageTapes line 749
76. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.stageTapes_frame line 757
77. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.stageTapes_clean line 770
78. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.stageTapes_field line 782
79. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.prefixInTime line 807
80. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.loadInTime line 850
81. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.clauses_length_le_input line 873
82. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.loadUnaryInTime line 878
83. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.timePolynomial line 901
84. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.timePolynomial_eval line 904
85. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.variableSlot line 910
86. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.polaritySlot line 911
87. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.variableField line 912
88. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.polarityField line 913
89. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.clauseWords_variable line 915
90. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.clauseWords_polarity line 921
91. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.output_variable line 929
92. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.output_polarity line 936
93. def OAI.BinPackingGames.Foundations.Hastad.SourceContextLoad.machine line 945
94. inductive OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.HeaderTape line 963
95. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList line 967
96. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_getElem?_ctorIdx_eq line 969
97. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_nodup line 973
98. instance OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.(instance at line 975) line 975
99. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.Tape line 979
100. inductive OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.Label line 981
101. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.variableHeader line 989
102. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.clauseHeader line 990
103. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.headerDestination line 991
104. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.readStart line 992
105. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.readLoop line 993
106. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.labelAt line 994
107. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.program line 996
108. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.atReadStart line 1015
109. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.atReadLoop line 1020
110. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.atReadDone line 1025
111. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.copiedInput line 1031
112. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.readOutput line 1034
113. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.headerOutput line 1038
114. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.clear_readOutput line 1043
115. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.readOutput_work line 1053
116. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.headerOutput_frame line 1058
117. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.headerInTime line 1062
118. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.digitOutput line 1098
119. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.digitOutput_frame line 1101
120. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.digitInTime line 1105
121. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.stageTapes line 1148
122. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.stageTapes_frame line 1153
123. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.stageTapes_current line 1164
124. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.stageTapes_remaining line 1184
125. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.prefixInTime line 1205
126. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.digitsInTime line 1233
127. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.outputTapes line 1252
128. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.initializeInTime line 1255
129. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_current line 1287
130. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_remaining line 1291
131. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_frame line 1295
132. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_work line 1301
133. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_variableHeader line 1306
134. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_clauseHeader line 1311
135. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_headers line 1316
136. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.output_formula line 1322
137. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.timePolynomial line 1327
138. theorem OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.timePolynomial_eval line 1330
139. def OAI.BinPackingGames.Foundations.Hastad.SourceLoopInit.machine line 1334