OAI/Computability/BinPacking/CookLevin/CircuitEncodingBridge.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.gateTemplate line 14
2. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Record line 28
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.slot line 35
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.words line 41
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.bits line 44
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.fieldValue line 46
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.templateWords line 53
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.outputWords line 57
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.outputBits line 58
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.outputWords line 60
11. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Tape line 63
12. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Context line 68
13. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.State line 74
14. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Alphabet line 75
15. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.Label line 77
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.defaultControl line 92
17. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.initialState line 93
18. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.headerTape line 95
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.headerNext line 101
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.contextSource line 105
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.affineEmit line 112
22. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.literalEmit line 116
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.emission line 120
24. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.contextNext line 125
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.cleanupNext line 132
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.drain line 135
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.resetGoto line 141
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.tagDecoder line 144
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.program line 153
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerModel.machine line 176
31. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateRecord line 193
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateRecords line 200
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.records line 204
34. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.recordsWords line 206
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.recordsBits line 207
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuitWords line 209
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuitBits line 212
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateRecords_length line 214
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.records_length line 220
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.recordsWords_cons line 223
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.recordsBits_cons line 226
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.recordsWords_length line 230
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuitWords_length line 239
44. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateFromFields line 244
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.decodeGateWords line 252
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.decodeGateWords_gateRecord line 257
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.decodeGateWords_gateRecords line 266
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuitWords_injective line 273
49. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuitBits_injective line 297
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateRecord_fields_le line 301
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateRecords_fields_le line 310
52. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuitWords_bounded line 326
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuitBits_length_le line 338
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.circuit_header_le_length line 344
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextSource_ne_scratch line 358
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextSource_ne_reversed line 365
57. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextOutput line 372
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextSteps line 376
59. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes line 379
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes_other line 382
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes_source line 387
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes_scratch line 391
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextOutput_update line 395
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextSteps_update line 400
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.setupStep line 405
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextTrace line 409
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextInTime line 429
68. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.output_eq_flatMap line 439
69. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.literalEmit_word line 447
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.affineEmit_word line 456
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextWords line 468
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.output_word line 474
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextTrace_word line 485
74. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextListOutput line 496
75. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextListSteps line 499
76. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextListStart line 502
77. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.ContextListLinked line 507
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextListOutput_update line 512
79. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextListSteps_update line 517
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.chain line 522
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextListTrace line 526
82. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateContexts line 553
83. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.outputContexts line 556
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateContexts_linked line 558
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.outputContexts_linked line 563
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.contextOutput_gate_word line 567
87. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.encodeWords_flatMap line 587
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateOutput_words line 593
89. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps line 604
90. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps_eq line 608
91. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.slot_le_sum line 625
92. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.sum_map_le_length_mul line 630
93. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps_le line 641
94. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.length_flatMap_le_length_mul line 653
95. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.outputBits_length_le line 665
96. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.recordBits_length line 683
97. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps_le_inputSize line 688
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.outputBits_length_le_inputSize line 694
99. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateTrace line 700
100. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.gateInTime line 715
101. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.outputTrace line 729
102. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitEmission.outputInTime line 747
103. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.Token line 763
104. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.Token.tag line 771
105. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.Token.words line 779
106. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.Token.bits line 787
107. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.Token.takeGate line 789
108. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.tokenWords line 799
109. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.tokenBits line 800
110. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.compileTokens line 802
111. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixModel.inputBits line 810
112. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateClauses_words line 819
113. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.unitClause_words line 827
114. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateRecords_outputWords line 830
115. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.gateBlocks_words line 848
116. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.formulaWords_eq_records line 860
117. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.formulaBits_eq_records line 874