OAI/Computability/MinUncut/Machines/MachineFiniteAlphabet.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet line 11
2. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.input_finite line 13
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.of_homogeneous line 17
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.of_bool line 23
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.of_equiv line 26
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.symbols_finite line 31
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.sequential_machine line 37
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.compose line 48
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.composeBits line 59
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteAlphabet.repeat_machine line 68
11. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Driver.finiteAlphabet line 85
12. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Runtime.finiteAlphabet line 91
13. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.statement line 105
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.statement_symm_statement line 108
15. def OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configuration line 114
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configuration_label line 117
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configuration_state line 120
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configuration_tapes line 123
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configuration_symm_configuration line 126
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configuration_configuration_symm line 131
21. def OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv line 136
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv_apply line 142
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.control_configuration line 145
24. def OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.program line 150
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.program_symm_program line 153
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.statementPushBound line 158
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.supportsStmt_iff line 163
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.supports_iff line 185
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport line 191
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport_symm line 198
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.step_transport line 205
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.step_iff line 217
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.advance_transport line 229
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.iterate_transport line 237
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.trace_iff line 248
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.trace line 264
37. def OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.execution line 271
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.execution_steps line 285
39. def OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.execution_reflect line 290
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateEquiv.execution_reflect_steps line 305
41. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.Alphabet line 323
42. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.finish line 325
43. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.scan line 328
44. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.seed line 338
45. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes line 342
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_source line 346
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_scratch line 352
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_destination line 357
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.update_source line 362
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.update_scratch line 376
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.update_destination line 387
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.prepend_replicate_word line 393
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_succ line 398
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_zero line 418
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.scanTrace line 435
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.restoreTapes line 465
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.affineTrace line 484
58. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.affineInTime line 520
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.seededAffineTrace line 540
60. inductive OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.Label line 574
61. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList line 578
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_getElem?_ctorIdx_eq line 580
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_nodup line 584
64. instance OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.(instance at line 586) line 586
65. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.program line 590
66. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAffineAt.machine line 596
67. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet line 618
68. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.State line 619
69. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.clean line 621
70. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.compareStateEquiv line 623
71. inductive OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label line 629
72. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList line 635
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_getElem?_ctorIdx_eq line 638
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_nodup line 642
75. instance OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.(instance at line 644) line 644
76. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.exitAt line 648
77. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.bitEncoding line 653
78. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.emit line 655
79. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.instruction line 660
80. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.copySteps line 678
81. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.compareSteps line 679
82. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.steps line 680
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.steps_le line 682
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.encodeWord_eq_iff line 686
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.emit_step line 695
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.joinTrace line 707
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityTrace line 711
88. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime line 813
89. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.machine line 832
90. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryEqualityBit.machineInTime line 843