OAI/Computability/DirectedFeedback/Machines/MachineStateEquiv.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Driver.finiteAlphabet line 10
2. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Runtime.finiteAlphabet line 16
3. abbrev OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.statement line 28
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.statement_symm_statement line 31
5. def OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configuration line 37
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configuration_label line 40
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configuration_state line 43
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configuration_tapes line 46
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configuration_symm_configuration line 49
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configuration_configuration_symm line 54
11. def OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv line 59
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv_apply line 65
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.control_configuration line 68
14. def OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.program line 73
15. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.program_symm_program line 76
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.statementPushBound line 81
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.supportsStmt_iff line 86
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.supports_iff line 108
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport line 114
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport_symm line 121
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.step_transport line 128
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.step_iff line 140
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.advance_transport line 152
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.iterate_transport line 160
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.trace_iff line 171
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.trace line 187
27. def OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.execution line 194
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.execution_steps line 208
29. def OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.execution_reflect line 213
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineStateEquiv.execution_reflect_steps line 228
31. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet line 243
32. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.State line 244
33. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.clean line 246
34. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.compareStateEquiv line 248
35. inductive OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.Label line 254
36. instance OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.(instance at line 260) line 260
37. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.exitAt line 265
38. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.bitEncoding line 270
39. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.emit line 272
40. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.instruction line 277
41. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.copySteps line 295
42. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.compareSteps line 296
43. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.steps line 297
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.steps_le line 299
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.encodeWord_eq_iff line 303
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.emit_step line 312
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.joinTrace_inline_MachineUnaryEqualityBit line 324
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityTrace line 328
49. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime line 430
50. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.machine line 449
51. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryEqualityBit.machineInTime line 460
52. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.Field line 481
53. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.inputSize line 483
54. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.fieldEquiv line 485
55. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.inputEquiv line 489
56. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.packData line 492
57. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.packData_inputEquiv line 495
58. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.basePredicate line 500
59. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.leftMatches line 504
60. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.rightMatches line 508
61. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.firstMatch line 512
62. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.firstMatch_spec line 515
63. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.firstMatch_none line 522
64. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.edgeAccept line 526
65. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.edgeAccept_of_matches line 532
66. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.rowAccept line 540
67. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.rowAccept_eq_true line 544
68. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.rowBlock line 550
69. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.rowBlock_at line 556
70. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.encodeBit line 563
71. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.encodeBits line 565
72. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.encodeBits_append line 569
73. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.encodeBits_graphWords line 575
74. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.encodeBits_length_le line 582
75. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.readEncodedSlots line 594
76. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedSlots line 607
77. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedAll line 626
78. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_readEncodedSlots line 642
79. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.writeEncodedSlots line 650
80. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.stepAux_writeEncodedSlots line 658
81. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_writeEncodedSlots line 675
82. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.encodedBlockStmt line 692
83. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.encodedBlockAt line 699
84. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_encodedBlockAt line 703
85. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockStmt line 712
86. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockAt line 727
87. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.step_encodedBlockAt line 738
88. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.rowAt line 755
89. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.machine line 760
90. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.machine_statementPushBound line 771
91. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRow.machineInTime line 776