OAI/Computability/DirectedFeedback/Machines/MachineRegularOwnerBody.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.joinTrace_inline_MachineRegularOwnerBody line 57
2. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.oneStep_inline_MachineRegularOwnerBody line 61
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataPlacement line 65
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataTrace line 75
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_local line 92
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_fuel line 106
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_global line 113
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_output line 127
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.copyCountTrace line 141
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.copyFuelTrace line 157
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.guardZeroStep line 174
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.guardPositiveStep line 180
13. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.dummyBits line 189
14. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.vertexData line 193
15. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.loopData line 200
16. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.loopFrame line 204
17. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.preSteps line 208
18. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.loopSteps line 212
19. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupCost line 219
20. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTime line 225
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyPlacement line 231
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyResultPlacement line 240
23. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyExecution line 251
24. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familySteps line 257
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyTrace line 261
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.coreFrame_eq line 281
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.vertexPlacement line 299
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.vertexTrace line 314
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.working_fuel line 338
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.working_scratch line 341
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.loopPositiveStep line 344
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.loopZeroStep line 355
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.bumpStep line 360
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.loopPrefixTrace line 370
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.preparationTrace line 398
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupFrame line 407
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits_zero line 448
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroFrame line 455
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopFrame line 465
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroTrace line 476
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopTrace line 490
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.loopTrace line 504
43. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.ownerInTime line 519
44. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps line 551
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTrace line 554
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps_le line 560
47. def OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.inputLength line 575
48. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.cloudSize_le_input line 577
49. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.cloudTotal_le_input line 581
50. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.level_le_input line 587
51. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.regularVertices_le_input line 591
52. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.offset_le_sum line 596
53. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.prefix_le_input line 607
54. def OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.tablePolynomial line 615
55. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.tableBits_le_of_counts line 620
56. def OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.regularPolynomial line 630
57. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.regularBits_le line 633
58. def OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.rotorPolynomial line 647
59. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingMachineBounds.cloudRotorBits_le line 651
60. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.offset_succ line 677
61. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.blocksPrefix_length_le line 685
62. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.header line 691
63. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.ownerBits line 694
64. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix line 699
65. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix line 704
66. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix line 710
67. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix_length_le line 718
68. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix_length_le line 726
69. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix_length_le line 737
70. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.regular_originalPrefix_le line 751
71. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.regular_ownerPrefix_le line 758
72. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.regular_dummyPrefix_le line 765
73. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.visits_le_input line 772
74. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularBounds.sum_body_costs_le line 782