OAI/Computability/DirectedFeedback/Machines/MachineDummyRows.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.trueRelation line 57
2. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.trueBits line 59
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.trueBits_length line 61
4. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowBits line 66
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowBits_length line 68
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowBits_eq_graph_row line 72
7. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowsBits line 77
8. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.Label line 81
9. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.start line 83
10. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowLabel line 84
11. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.bumpLabel line 86
12. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.fields line 88
13. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.afterPort line 90
14. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.entry line 93
15. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.Alphabet line 98
16. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.continueAt line 100
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.stepAux_continueAt line 106
18. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.program line 111
19. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.fieldTapes line 118
20. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.initialTapes line 121
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.initializeStep line 124
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowTrace line 137
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.bumpStep line 158
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowAndBumpTrace line 169
25. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.steps line 180
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.suffixTrace line 185
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.allTrace line 208
28. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.graphRows line 223
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.graphRows_length line 230
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.rowsBits_eq_graphRows line 236
31. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.dummyRows line 246
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.dummyRows_length line 251
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.dummyRowsTrace line 254
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.steps_le_bound line 266
35. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.inputSize line 298
36. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.timePolynomial line 301
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.timePolynomial_bounds line 307
38. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.machine line 328
39. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.machineInTime line 339
40. def OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.machineDummyInTime line 349
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineDummyRows.finalFrame line 361
42. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.Tape line 377
43. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet line 378
44. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.State line 379
45. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.Label line 381
46. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.reverseIndex line 387
47. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.emittedBits line 389
48. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.instruction line 392
49. structure OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.Input line 405
50. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.memory line 412
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.memory_input line 415
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.join_trace_inline_MachineRegularDummyRow line 418
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.affine_frame line 422
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.cleanup_frame line 430
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.rowTraceAt line 439
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.cleanupTraceAt line 461
57. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.steps line 486
58. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.timeBound line 491
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.steps_eq line 494
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.traceAt line 500
61. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.machine line 527
62. def OAI.DFVSGames.Foundations.Complexity.MachineRegularDummyRow.machineInTime line 538
63. inductive OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.Control line 560
64. instance OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.(instance at line 563) line 563
65. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.Tape line 565
66. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.Label line 566
67. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.Alphabet line 567
68. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.State line 569
69. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.bodyEntry line 571
70. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.extra line 574
71. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.program line 585
72. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.tapes line 588
73. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.cfg line 592
74. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.bodyTrace line 596
75. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.guard_succ line 614
76. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.guard_zero line 625
77. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.bump_step line 636
78. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.paddingBits line 648
79. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.steps line 652
80. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.loopTrace line 657
81. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.initialTapes line 679
82. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.initialize_step line 682
83. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.paddingTrace line 697
84. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.machine line 704
85. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingRows.execution line 715
86. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.encodeWords_flatMap_inline_PreprocessingPaddingWords line 736
87. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.ofFn_split line 742
88. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.flatten_ofFn_rowIndex line 752
89. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.rowBits line 767
90. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits line 771
91. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits line 774
92. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_flat line 777
93. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_eq_vertices line 783
94. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_old line 797
95. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_new line 809
96. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.dummy_rowsBits_eq_ofFn line 819
97. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.paddingBits_eq_ofFn line 833
98. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_old line 847
99. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_new line 851
100. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_pad line 863
101. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingWords.tableBits_pad line 870