OAI/Computability/DirectedFeedback/Machines/MachineTableRows.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DFVSGames.Foundations.Complexity.MachineTableRows.Label line 56
2. instance OAI.DFVSGames.Foundations.Complexity.MachineTableRows.(instance at line 61) line 61
3. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTableRows.Alphabet line 65
4. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.routine line 67
5. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.fieldBits line 89
6. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.fieldSize line 92
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableRows.fieldBits_length line 96
8. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.prefixTapes line 100
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableRows.prefixTrace line 103
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableRows.appendTrace line 155
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableRows.rowBits_eq line 199
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableRows.fieldBits_eq_rowBits line 205
13. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.timePolynomial line 213
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableRows.timePolynomial_bounds line 216
15. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.rowAppendInTime line 223
16. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.machine line 248
17. def OAI.DFVSGames.Foundations.Complexity.MachineTableRows.machineRowInTime line 259
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableRows.outputFrame line 288
19. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedIndex line 304
20. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow line 309
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_eq line 314
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_tail line 322
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_reverse line 327
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_relation line 340
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_words line 353
26. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords line 360
27. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.suffixWords line 363
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords_length line 366
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_at_row line 371
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_drop_row line 383
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.selected_reverse line 389
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.remaining_relation line 396
33. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.Tape line 403
34. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.Buffer line 404
35. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.State line 405
36. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.Alphabet line 406
37. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer line 408
38. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape line 410
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape_injective line 412
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.source_outside line 419
41. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.fields line 425
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.fields_zero line 427
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.fields_one line 428
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.fields_two line 429
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.fields_separate line 431
46. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.copyStateEquiv line 434
47. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.Label line 440
48. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt line 446
49. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.instruction line 451
50. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.machine line 463
51. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.looked line 474
52. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.copied line 478
53. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.affined line 483
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.looked_other line 488
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.looked_reverse line 493
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.looked_relation line 497
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.vectorBits_eq_encodedBlock line 507
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.relationBits_eq_encodedBlock line 519
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_step line 523
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_pushBound line 552
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.copied_other line 557
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.copied_reverse line 563
63. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.copied_relation line 568
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.affined_other line 572
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.affined_reverse line 577
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.affined_relation line 581
67. structure OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.Input line 585
68. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.emittedWords line 594
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.affined_fields line 597
70. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.rowSteps line 607
71. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.steps line 610
72. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.finalTapes line 614
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.join_trace_inline_MachineRegularOriginalRow line 622
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTrace line 626
75. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.copyTrace line 640
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.affineTrace line 655
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.emitTrace line 676
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.traceAt line 702
79. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.timeBound line 718
80. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.steps_le line 721
81. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalRow.machineInTime line 738