OAI/Computability/DirectedFeedback/Encoding/EmitRows.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.Context line 13
2. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.RowCommand line 14
3. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits line 16
4. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.vector_list_ofFn_inline_EmitRows line 21
5. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.bitValues_ofFn_inline_EmitRows line 26
6. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits_values line 35
7. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands line 43
8. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.rowContext line 52
9. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.rowValues line 56
10. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.encodedRow_inline_EmitRows line 62
11. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_bits line 68
12. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands line 99
13. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockWords line 104
14. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.tableWords_eq_blocks line 111
15. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands line 122
16. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_bits line 128
17. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_length line 142
18. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.headerInTime line 146
19. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.encodeWords_flatMap_inline_EmitRows line 171
20. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_bits line 177
21. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_length_le line 184
22. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.flatMap_length_le_inline_EmitRows line 192
23. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_length_le line 203
24. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTime line 214
25. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn line 243
26. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn_bits line 247
27. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTimeAmbient line 256
28. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet line 297
29. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.finish line 299
30. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.instruction line 304
31. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_drain line 313
32. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_finish line 321
33. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes line 326
34. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost line 331
35. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_apply line 337
36. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_selected line 350
37. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_unselected line 354
38. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost_le line 360
39. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupTrace line 376
40. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupInTime line 401
41. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.program line 417
42. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.machine line 421
43. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.machineInTime line 433
44. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_outputOnly line 444
45. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Cleanup.machineHaltInTime line 456
46. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.headerPlan line 483
47. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.rowPlan line 484
48. inductive OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.Label line 486
49. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.headerEntry line 498
50. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.rowEntry line 501
51. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.clearNext line 504
52. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.program line 507
53. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.machine line 541
54. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.program_setup line 554
55. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.program_guard line 558
56. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.program_headLookup line 561
57. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.program_compare line 565
58. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.program_increment line 568
59. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.inputBits line 580
60. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords line 583
61. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits line 588
62. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords line 591
63. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits line 594
64. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_zero line 597
65. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_zero line 603
66. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_succ line 609
67. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_succ line 622
68. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_reverse_succ line 629
69. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_full line 636
70. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_full line 645
71. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_zero line 650
72. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords_succ line 655
73. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_succ line 666
74. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_full line 674
75. structure OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready line 682
76. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready.of_agree line 700
77. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_scan line 720
78. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_indexScan line 727
79. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_succ line 734
80. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_at_end line 741
81. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready.cursor_at_end line 746
82. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopState.Ready.reversed_at_end line 750