OAI/Computability/MinUncut/Machines/MachineDummyRows.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.trueRelation line 13
2. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.trueBits line 15
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.trueBits_length line 17
4. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowBits line 23
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowBits_length line 25
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowBits_eq_graph_row line 29
7. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowsBits line 34
8. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.Label line 38
9. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.start line 40
10. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowLabel line 41
11. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.bumpLabel line 43
12. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.fields line 45
13. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.afterPort line 47
14. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.entry line 50
15. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.Alphabet line 55
16. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.continueAt line 57
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.stepAux_continueAt line 63
18. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.program line 68
19. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.fieldTapes line 75
20. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.initialTapes line 78
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.initializeStep line 81
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowTrace line 94
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.bumpStep line 115
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowAndBumpTrace line 126
25. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.steps line 137
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.suffixTrace line 142
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.allTrace line 165
28. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.graphRows line 180
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.graphRows_length line 187
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.rowsBits_eq_graphRows line 193
31. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.dummyRows line 203
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.dummyRows_length line 208
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.dummyRowsTrace line 211
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.steps_le_bound line 223
35. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.inputSize line 255
36. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.timePolynomial line 258
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.timePolynomial_bounds line 264
38. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.machine line 285
39. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.machineInTime line 296
40. def OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.machineDummyInTime line 307
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDummyRows.finalFrame line 320
42. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.Tape line 334
43. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet line 335
44. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.State line 336
45. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.Label line 338
46. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.reverseIndex line 344
47. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.emittedBits line 346
48. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.instruction line 349
49. structure OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.Input line 362
50. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.memory line 369
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.memory_input line 372
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.join_trace line 375
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.affine_frame line 379
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.cleanup_frame line 387
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.rowTraceAt line 396
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.cleanupTraceAt line 418
57. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.steps line 443
58. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.timeBound line 448
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.steps_eq line 451
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.traceAt line 457
61. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.machine line 484
62. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularDummyRow.machineInTime line 495
63. inductive OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.Control line 515
64. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.Control.enumList line 519
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.Control.enumList_getElem?_ctorIdx_eq line 521
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.Control.enumList_nodup line 525
67. instance OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.(instance at line 527) line 527
68. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.Tape line 531
69. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.Label line 532
70. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.Alphabet line 533
71. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.State line 535
72. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.bodyEntry line 537
73. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.extra line 540
74. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.program line 551
75. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.tapes line 554
76. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.cfg line 558
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.bodyTrace line 562
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.guard_succ line 580
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.guard_zero line 591
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.bump_step line 602
81. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.paddingBits line 614
82. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.steps line 618
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.loopTrace line 623
84. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.initialTapes line 645
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.initialize_step line 648
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.paddingTrace line 663
87. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.machine line 670
88. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingRows.execution line 681