OAI/Computability/MinUncut/Machines/RuntimeModel2.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape line 12
2. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList line 18
3. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_getElem?_ctorIdx_eq line 22
4. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_nodup line 26
5. instance OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.(instance at line 28) line 28
6. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet line 32
7. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Flags line 34
8. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Ambient line 35
9. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.State line 36
10. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.normal line 38
11. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.initial line 41
12. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.context line 43
13. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv line 46
14. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv_normal line 53
15. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterEquiv line 58
16. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts line 64
17. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts_injective line 67
18. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts line 71
19. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts_injective line 74
20. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.rowSources line 78
21. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.headerSources line 79
22. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.fieldPorts line 80
23. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts line 82
24. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_ne_output line 86
25. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_cover line 89
26. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareStatement line 111
27. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterStatement line 116
28. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.storeLoop line 120
29. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_storeLoop line 123
30. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.nextRow line 128
31. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_nextRow line 132
32. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.RuntimeModel.transportInTime line 140
33. inductive OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label line 163
34. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList line 168
35. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_getElem?_ctorIdx_eq line 171
36. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_nodup line 175
37. instance OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.(instance at line 177) line 177
38. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.statement line 183
39. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareProgram_at line 202
40. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime line 212
41. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime line 268
42. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.encodeWord_eq_iff line 271
43. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareInTime line 280
44. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le line 297
45. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le_of_lt line 304
46. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime_bounded line 311
47. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop line 330
48. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowState line 333
49. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop_eq_graph line 336
50. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowContext_eq line 343
51. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareRowInTime line 350
52. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.CompareLoop.relationFromRowState line 368
53. inductive OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.Command line 391
54. inductive OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.Phase line 398
55. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet line 405
56. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.State line 406
57. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.transition line 408
58. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.payload line 409
59. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.commandBits line 412
60. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps line 421
61. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.commandStatement line 430
62. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.output_encodeWord line 464
63. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.commandTrace line 478
64. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.Label line 555
65. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.labelAt line 557
66. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.commandAt line 560
67. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.statement line 564
68. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.program line 574
69. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.machine line 579
70. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits line 592
71. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps line 598
72. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes line 603
73. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_output line 606
74. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_other line 610
75. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.prefixTrace line 614
76. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.planTrace line 653
77. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps_le line 674
78. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.planInTime line 693
79. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.listCommands line 714
80. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits_listCommands line 717
81. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.bits_listCommands line 729
82. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands line 735
83. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.affineValue line 739
84. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.scaleBits line 742
85. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_bits line 752
86. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_length line 760
87. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands line 764
88. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands_bits line 766
89. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.affineInTime line 775
90. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient line 799
91. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.commandBits_mapAmbient line 807
92. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps_mapAmbient line 813