OAI/Computability/MinUncut/Machines/Driver.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.headerPlan line 14
2. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.rowPlan line 15
3. inductive OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.Label line 17
4. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.headerEntry line 29
5. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.rowEntry line 32
6. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.clearNext line 35
7. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.program line 38
8. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.machine line 72
9. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.program_setup line 85
10. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.program_guard line 89
11. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.program_headLookup line 92
12. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.program_compare line 96
13. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.program_increment line 99
14. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.inputBits line 110
15. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords line 113
16. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits line 118
17. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords line 121
18. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits line 124
19. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_zero line 127
20. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_zero line 133
21. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_succ line 139
22. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_succ line 152
23. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_reverse_succ line 159
24. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_full line 166
25. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_full line 175
26. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_zero line 180
27. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords_succ line 185
28. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_succ line 196
29. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_full line 204
30. structure OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready line 212
31. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.of_agree line 230
32. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_scan line 250
33. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_indexScan line 257
34. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_succ line 264
35. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_at_end line 271
36. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.cursor_at_end line 276
37. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.reversed_at_end line 280
38. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.bodyTime line 295
39. structure OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.RowStepResult line 298
40. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.guardTapes line 308
41. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.parsedTapes line 312
42. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingTapes line 317
43. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.emittedTapes line 321
44. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.clearFieldsTapes line 326
45. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.resultTapes line 329
46. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_other line 334
47. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_counter line 344
48. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_cursor line 350
49. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_tail line 356
50. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_reverse line 362
51. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_head line 368
52. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.clearFieldsInTime line 375
53. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.incrementInTime line 397
54. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.emitterView_at line 412
55. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.context_rowState line 422
56. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.emitInTime line 431
57. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.result_ready line 469
58. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.workingOperands line 480
59. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Body.rowStep line 490
60. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.inputTapes line 614
61. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.rowsBits line 618
62. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.headerBits line 621
63. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.setupTapes line 625
64. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.loopTapes line 633
65. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.loopStart line 642
66. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.setupResult_eq line 646
67. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.headerResult_eq line 652
68. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.machineInitial_eq line 657
69. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.setupInTime line 667
70. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.headerView_at line 686
71. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.headerInTime line 696
72. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.time line 734
73. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.time_eq line 736
74. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Initialization.initializeInTime line 740