OAI/Computability/DirectedFeedback/Machines/VertexLabel.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.VertexLabel line 54
2. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexInstruction line 56
3. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.recordsInput line 66
4. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.recordsOutput line 69
5. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamFrame line 72
6. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexSteps line 77
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.recordsInput_eq_codec line 83
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamFrame_afterRow_inline_MachineLazyRows line 92
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexSuffixTrace line 109
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexTrace line 193
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.encodeWords_flatMap_inline_MachineLazyRows line 209
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.recordsOutput_lazy line 215
13. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.valueBound line 230
14. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.rowSizeBound line 231
15. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.rowCostBound line 232
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexValue_le line 235
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexRowBits_length_le line 244
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamRowSteps_le line 254
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexSteps_le_capacity_inline_MachineLazyRows line 266
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexSteps_le line 291
21. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexInTime line 297
22. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.vertexMachine line 318
23. abbrev OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.row line 341
24. abbrev OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.trueRelation line 342
25. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.oldReverseMap line 344
26. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.expanderReverseMap line 345
27. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.oldRow line 347
28. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow line 353
29. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.relation_ext_inline_PreprocessingOverlayWords line 358
30. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_old line 365
31. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_expander line 378
32. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_reverse_val line 394
33. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_reverse_val line 402
34. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_words line 410
35. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_words line 417
36. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.ofFn_overlayPorts line 427
37. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows line 433
38. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_length line 437
39. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.flatRows_overlay line 441
40. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_words line 451
41. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.tableWords_overlay line 474
42. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.tableBits_overlay line 479
43. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayWords.rotationWords_vertices line 485
44. abbrev OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.State line 513
45. inductive OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.Label line 515
46. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.bodyIndex line 521
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.bodyIndex_injective line 523
48. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.trueBits line 527
49. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.instruction line 529
50. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowBits line 544
51. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowSteps line 547
52. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.resultTapes line 551
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.joinTrace_inline_MachineOverlayRows line 556
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowTrace line 560
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowBits_eq_expanderRow line 702
56. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.machine line 715
57. abbrev OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.VertexLabel line 726
58. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexInstruction line 728
59. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.streamFrame line 738
60. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.streamOutput line 743
61. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexSteps line 746
62. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.valueBound line 751
63. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowSizeBound line 752
64. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowCostBound line 753
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.value_le line 756
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowBits_length line 764
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowBits_length_le line 770
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.rowSteps_le line 777
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le_capacity_inline_MachineOverlayRows line 787
70. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le line 812
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.streamFrame_afterRow_inline_MachineOverlayRows line 819
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexSuffixTrace line 835
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexTrace line 909
74. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexInTime line 925
75. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.encodeWords_flatMap_inline_MachineOverlayRows line 947
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.streamOutput_expanderRows line 953
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.expanderValues_bounded line 965
78. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayRows.vertexMachine line 970