OAI/Computability/MinUncut/Machines/MachineExpanderTableRows.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.singleStep line 13
2. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.sequence line 19
3. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.widen line 26
4. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.tableRowData line 32
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalValue line 36
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.tableRowData_frame0 line 40
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalFrame line 47
8. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.rowAfterState line 60
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.rowAfterState_position line 66
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller_rowAfterState line 71
11. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.preparedRowInTime line 75
12. structure OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.VertexSuffixRun line 104
13. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.suffixRun_aux line 118
14. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.suffixInTime line 172
15. structure OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.VertexRun line 179
16. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexInTime line 193
17. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.oldTableWord line 207
18. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices line 210
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_zero line 214
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_succ line 218
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_full line 224
22. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexBodyBudget line 229
23. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexLoopBudget line 232
24. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexLoopTapes line 235
25. structure OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.VertexLoopRun line 239
26. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.boundarySingleStep line 250
27. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexLoopInTime line 256
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_position line 310
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_register line 313
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_idempotent line 316
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_reverse_update line 319
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputTrace line 335
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltTrace line 367
34. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputInTime line 382
35. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltInTime line 395
36. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.completeBudget line 412
37. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.timeCoefficient line 415
38. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.timePolynomial line 418
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertices_le_word_length line 421
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.completeBudget_le line 430
41. structure OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.TableRun line 465
42. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.initializeInTime line 477
43. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.tableInTime line 494
44. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.cycleWords line 528
45. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.cycleTapes line 538
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.toBool_cycleTapes line 542
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_eq_cycleTapes line 547
48. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.copyFrame line 557
49. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.returnFrame line 562
50. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.installedFrame line 567
51. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame line 571
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_cycleTapes line 576
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.returnFrame_eq_cycleTapes line 588
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_update line 602
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame_eq_update line 613
56. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost line 630
57. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient line 636
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.wordLength_add_one_le line 640
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost_le line 651
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.vertexCount_monotone line 689
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.level_le_vertexCount line 695
62. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum line 707
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_zero line 710
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_succ line 713
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_add line 717
66. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget line 722
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_zero line 725
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_succ line 728
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_le line 734
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_le line 761
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.paddedSize_le_succ_input line 775
72. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient line 785
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_at_boundedLevel_le line 788