OAI/Computability/DirectedFeedback/Machines/MachineExpanderTableLoop.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.oldTableWord line 57
2. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices line 60
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_zero line 64
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_succ line 68
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_full line 74
6. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexBodyBudget line 79
7. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexLoopBudget line 82
8. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexLoopTapes line 85
9. structure OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.VertexLoopRun line 89
10. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.boundarySingleStep_inline_MachineExpanderTableLoop line 100
11. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexLoopInTime line 106
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.clearRegister_position line 167
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.clearRegister_register line 170
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.clearRegister_idempotent line 173
15. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_reverse_update line 176
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.reverseOutputTrace line 192
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltTrace line 224
18. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.reverseOutputInTime line 239
19. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltInTime line 252
20. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.completeBudget line 276
21. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.timeCoefficient line 279
22. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.timePolynomial line 282
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertices_le_word_length line 285
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.completeBudget_le line 294
25. structure OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.TableRun line 329
26. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.initializeInTime_inline_MachineExpanderTable line 341
27. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.tableInTime line 358
28. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.cycleWords line 395
29. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.cycleTapes line 405
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.toBool_cycleTapes line 409
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_eq_cycleTapes line 414
32. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.copyFrame line 424
33. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.returnFrame line 429
34. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.installedFrame line 434
35. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame line 438
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_cycleTapes line 443
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.returnFrame_eq_cycleTapes line 455
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_update line 469
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame_eq_update line 480
40. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost line 500
41. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient line 506
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.wordLength_add_one_le line 510
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost_le line 521
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.vertexCount_monotone line 559
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.level_le_vertexCount line 565
46. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum line 577
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_zero line 580
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_succ line 583
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_add line 587
50. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget line 592
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_zero line 595
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_succ line 598
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_le line 604
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_le line 631
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.paddedSize_le_succ_input line 645
56. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient line 655
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_at_boundedLevel_le line 658
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.installed_returnFrame line 693
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.cleaned_multipliedFrame line 704
60. structure OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.ResizeRun line 720
61. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.resizeInTime line 733