OAI/Computability/DirectedFeedback/Encoding/PreprocessingRegularWords.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.actualRow line 60
2. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.vertexRows line 65
3. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.originalVertexRows line 70
4. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexRows line 71
5. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.vertexBits line 74
6. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.originalVertexBits line 77
7. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits line 78
8. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.actualRow_internal line 81
9. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.actualRow_eq line 85
10. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.actualRow_tail line 95
11. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_reverse line 99
12. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_reverse line 111
13. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.relation_ext_inline_PreprocessingRegularWords line 124
14. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_relation line 132
15. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_relation line 139
16. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_words line 149
17. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_words line 156
18. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.encodeWords_flatMap_inline_PreprocessingRegularWords line 165
19. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.actualRow_bits line 171
20. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.vertexBits_eq line 179
21. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.paddingOrder_ofFn line 196
22. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.vertexOrder_ofFn line 207
23. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.paddingList_flatMap line 234
24. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.rowsBits_ofCloudTables line 241
25. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularWords.tableBits_ofCloudTables line 260
26. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.PortLabel line 285
27. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portEntry line 287
28. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portInstruction line 291
29. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portBits line 297
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_eq line 301
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_all line 311
32. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits line 315
33. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps line 320
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.joinTrace_inline_MachineRegularVertexBlock line 328
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portPrefixTrace line 332
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portTrace line 361
37. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalTapes line 377
38. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalView line 380
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_left line 385
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_right line 388
41. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalStateEquiv line 393
42. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction line 401
43. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory line 408
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_input line 412
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_update line 416
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalFrame line 420
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreTrace line 426
48. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTapes line 458
49. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView line 460
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_left line 465
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_right line 468
52. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreInstruction line 473
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMemory_update line 479
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyFrame line 484
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreTrace line 490
56. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.Label line 519
57. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry line 526
58. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry line 529
59. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.instruction line 532
60. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.oldCloud line 541
61. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps line 544
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps_eq line 548
63. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_flatMap_inline_MachineRegularVertexBlock line 559
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_pair_inline_MachineRegularVertexBlock line 565
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.vertexBits_split line 568
66. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps line 581
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalTraceAt line 588
68. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps line 631
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTraceAt line 638
70. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.rowSizeBound line 680
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits_length_le line 682
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_length_le line 688
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.allRowBits_length_le line 702
74. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portTimeBound line 710
75. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps_le line 714
76. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalTimeBound line 746
77. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTimeBound line 751
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps_le line 755
79. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps_le line 785
80. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachine line 803
81. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine line 814
82. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachineInTime line 825
83. def OAI.DFVSGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachineInTime line 845