OAI/Computability/DirectedFeedback/Games/SignaturePrepare.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.Width line 13
2. abbrev OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.Arena line 14
3. abbrev OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.ProfileState line 15
4. abbrev OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.State line 16
5. abbrev OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.ProfileLabel line 17
6. inductive OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.Label line 19
7. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.variableField line 26
8. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.polarityField line 29
9. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.place line 32
10. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.unplace line 36
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.unplace_place line 46
12. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.place_injective line 59
13. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.place_unplace line 64
14. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.fill line 96
15. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.fill_place line 102
16. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.fill_self line 107
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.fill_frame line 115
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.fill_update line 122
19. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.placedLabel line 145
20. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.placedConfiguration line 149
21. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.placedStatement line 155
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.placed_stepAux line 170
23. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.signStateEquiv line 197
24. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.commitStatement line 204
25. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.program line 210
26. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.placed_step line 215
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.stepAux_commit line 232
28. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.profileInTime line 244
29. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.commitInTime line 264
30. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.prepareInTime line 277
31. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.loaded_name_field line 316
32. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.loaded_sign_field line 334
33. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.loadedPrepareInTime line 347
34. def OAI.DFVSGames.Foundations.Hastad.SourceSignaturePrepare.machine line 377
35. def OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameStatement line 399
36. def OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameConfiguration line 411
37. def OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameProgram line 414
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_state line 417
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_metadata line 420
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_tapes line 423
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameStatement_pushBound line 426
42. def OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.statement line 430
43. def OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.configuration line 434
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.configuration_state line 438
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.configuration_metadata line 442
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.configuration_tapes line 446
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.statement_pushBound line 450
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frame_stepAux line 460
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frame_step line 481
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frame_advance line 493
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frame_iterate line 502
52. def OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameExecution line 514
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.frameExecution_steps line 528
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.stepAux_simulation line 533
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.step_simulation line 540
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.trace line 553
57. def OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.execution line 564
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateFrame.execution_steps line 574
59. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.Arena line 589
60. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.LoadState line 590
61. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.PrepareState line 591
62. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.State line 592
63. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.Label line 593
64. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.prepareEntry line 597
65. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.stateSwap line 601
66. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.program line 604
67. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.preparationConfiguration line 610
68. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.preparation_step line 618
69. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.initialState line 637
70. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.finalState line 641
71. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.loadInTime line 646
72. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.signatureInTime line 667
73. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.prepareInTime line 689
74. def OAI.DFVSGames.Foundations.Hastad.SourceContextPrepare.machine line 711