OAI/Computability/DirectedFeedback/Machines/MachinePortReindex.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.Alphabet line 58
2. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.State line 59
3. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.clean line 61
4. inductive OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.Label line 64
5. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.exitAt line 70
6. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.emit line 75
7. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.instruction line 80
8. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.steps line 101
9. theorem OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.steps_le line 103
10. theorem OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.steps_le_encodedLength line 108
11. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.value line 114
12. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.frame_inline_MachinePortReindex line 116
13. theorem OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.joinTrace_inline_MachinePortReindex line 120
14. theorem OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.reindexTrace line 124
15. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.reindexInTime line 280
16. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.machine line 299
17. def OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.machineInTime line 310
18. theorem OAI.DFVSGames.Foundations.Complexity.MachinePortReindex.lazy_value line 324
19. def OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.row line 342
20. def OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.trueRelation line 346
21. def OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.stayRow line 348
22. def OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.moveRow line 351
23. def OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.reverseMap line 357
24. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.relation_ext_inline_PreprocessingLazyWords line 359
25. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_stay line 366
26. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_move line 379
27. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.stayRow_reverse_val line 392
28. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.moveRow_reverse_val line 397
29. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.relationWords_true line 405
30. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.stayRow_words line 409
31. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.moveRow_words line 415
32. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.ofFn_rowIndex line 422
33. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.flatRows_list line 436
34. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.ofFn_lazyPorts line 443
35. def OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.vertexRows line 456
36. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_length line 460
37. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.flatRows_lazy line 465
38. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_words line 475
39. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.tableWords_lazy line 495
40. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLazyWords.tableBits_lazy line 500
41. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.Label line 519
42. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.State line 520
43. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.addressIndex line 522
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.addressIndex_injective line 524
45. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.fields line 528
46. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexInstruction line 530
47. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.instruction line 539
48. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexRowBits line 544
49. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexMappedTapes line 548
50. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexResultTapes line 552
51. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexSteps line 557
52. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.rowBits line 561
53. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.mappedTapes line 564
54. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.resultTapes line 567
55. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.steps line 572
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.reindexRowTrace line 575
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.rowTrace line 638
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.rowBits_eq_moveRow line 659
59. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.machine line 667
60. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.Buffer line 678
61. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.StreamState line 679
62. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamClean line 681
63. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.relationStateEquiv line 684
64. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy line 691
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy_step line 696
66. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.bodyIndex line 721
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.bodyIndex_injective line 723
68. inductive OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.StreamLabel line 728
69. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamInstruction line 734
70. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.inputRowBits line 752
71. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamRowSteps line 755
72. def OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamResultTapes line 760
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.joinTrace_inline_MachineLazyRows line 765
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyRows.streamRowTrace line 769