OAI/Computability/DirectedFeedback/Games/LocalEquation.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.LocalKey line 13
2. abbrev OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.LocalInput line 14
3. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.signatureEncoding line 16
4. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.signatureList line 22
5. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.mem_signatureList line 24
6. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.signatureList_nodup line 27
7. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.signatureList_length line 30
8. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.localInputEncoding line 34
9. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.localInputs line 37
10. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.mem_localInputs line 39
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.localInputs_nodup line 42
12. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.localInputs_length line 45
13. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.localKeyEncoding line 49
14. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.emptyLocalAddress line 53
15. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.foldedLocalAddress line 57
16. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.equationFor line 63
17. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.equation line 71
18. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.emit line 75
19. def OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.addressMap line 78
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.mapEquation_comp line 84
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.addressMap_emptyLocalAddress line 87
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.addressMap_foldedLocalAddress line 93
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map_equationFor line 102
24. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map line 115
25. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalEquation.sourceEquation_eq_map_emit line 128
26. abbrev OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.Descriptor line 144
27. def OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.descriptor line 146
28. def OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.baseValue line 151
29. def OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.realize line 158
30. def OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.words line 160
31. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.realize_descriptor line 164
32. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.descriptor_offset_bound line 181
33. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_numeric line 204
34. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_words line 213
35. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.baseValue_lt line 222
36. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressDescriptors.equation_emit_steps_le line 239
37. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.Alphabet line 258
38. def OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.finish line 260
39. def OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.emitStatement line 265
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.emitStep line 269
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.prefix_encodeWord line 280
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.registerEmitTrace line 284
43. def OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.registerEmitInTime line 313
44. def OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.program line 336
45. def OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.programInTime line 344
46. def OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.machine line 359
47. def OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.machineInTime line 370
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.emitStatement_pushes line 382
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.program_pushes_le line 388
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegisterEmit.machine_pushes_le line 401
51. inductive OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.Label line 424
52. instance OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.instFintypeLabel line 429
53. abbrev OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.Alphabet line 431
54. abbrev OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.State line 432
55. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.rhsBit line 434
56. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.steps line 436
57. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.statement line 441
58. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.program line 464
59. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.prefixTapes line 468
60. theorem OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.prefixTapes_other line 471
61. theorem OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.equationTrace line 475
62. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.equationInTime line 546
63. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.programInTime line 565
64. abbrev OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.Tape line 580
65. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.machine line 582
66. def OAI.DFVSGames.Foundations.Hastad.SourceEquationEmit.machineInTime line 593
67. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.dispatch line 615
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.stepAux_dispatch line 622
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.dispatch_push_bound line 640
70. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.emit line 652
71. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.tableBound line 656
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.stepAux_emit line 659
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.emit_push_bound line 666
74. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.emitInTime line 672
75. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteTable.output_frame line 689
76. def OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.codedEquation line 704
77. def OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.descriptorWords line 708
78. def OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.descriptorBits line 711
79. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.descriptorWords_length line 714
80. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.descriptorBits_length_le line 718
81. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.decode_descriptorBits line 722
82. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.parse_descriptorWords line 726
83. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.decode_codedEquation line 732
84. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.codedEquation_global line 743
85. def OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound line 752
86. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound_le line 755
87. instance OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.localInputDecidableEq line 772
88. def OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor line 778
89. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.stepAux_emitDescriptor line 784
90. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor_push_bound line 795
91. def OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptorInTime line 802
92. theorem OAI.DFVSGames.Foundations.Hastad.SourceDescriptorEmission.descriptor_output_frame line 815