OAI/Computability/MinUncut/Machines/MachineRegularTableTrace.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.joinCompleteTrace line 11
2. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.normalizeEmptyAppend line 15
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerStartTrace line 19
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerOldTrace line 31
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.beforeCleanupTrace line 47
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupFinalTrace line 63
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.fullTrace line 71
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_output line 79
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.input_stacks_eq line 92
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.initial_cfg_eq line 114
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.trace line 122
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_mono line 152
13. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial line 159
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial_eval line 167
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.internal_steps_le line 176
16. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.familyPolynomial line 195
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.family_budget_le line 199
18. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial line 211
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial_eval line 215
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.actual_row_bound_le line 221
21. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial line 228
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_add_output line 231
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularExecutionBounds.block_core_bound_le line 237
24. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide line 273
25. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.rowPolynomial line 274
26. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.outputPolynomial line 276
27. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.corePolynomial line 278
28. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial line 282
29. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupPolynomial line 285
30. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.timePolynomial line 286
31. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.bodySize line 290
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial_eval line 293
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalTimeBound_le line 308
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide_le line 319
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.vertexSteps_le line 329
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.clearSteps_frame line 355
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupSteps_le line 362
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.totalSteps_le line 393
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalInTime line 411
40. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize line 428
41. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide line 431
42. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.rowPolynomial line 433
43. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.outputPolynomial line 436
44. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.corePolynomial line 439
45. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial line 444
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial_eval line 448
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummyTimeBound_le line 464
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide_le line 475
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerPrefix_length_le line 485
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.growingOutput_length_le line 493
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummySteps_le line 504
52. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.prePolynomial line 535
53. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopPolynomial line 538
54. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupPolynomial line 541
55. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.timePolynomial line 544
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.preSteps_le line 548
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopSteps_le line 567
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.allLoopSteps_le line 584
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupSteps_working line 595
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupCost_le line 605
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerTime_le line 642
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.totalSteps_le line 659
63. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerInTime line 664
64. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopPolynomial line 683
65. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopPolynomial line 688
66. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.timePolynomial line 693
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_prefix_le line 699
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_le line 721
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_prefix_le line 729
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_le line 753
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.totalTime_le line 762
72. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.machineInTime line 778