OAI/Computability/MinUncut/Estimates/InputData.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.inputData line 13
2. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerData line 26
3. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerStacks line 29
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerTrace line 33
5. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldData line 52
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.originalData_eq line 55
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldBodyTrace line 58
8. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.counterStacks line 73
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.frame_oldFuel line 76
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.frame_ownerFuel line 80
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_oldFuel line 84
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_ownerFuel line 95
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_global line 106
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_owner line 119
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardStep line 132
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardExit line 146
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldIncrementStep line 157
18. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefix line 171
19. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed line 174
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.joinTrace line 181
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefixTrace line 185
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopTrace line 216
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.frame_scratch line 228
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.frame_darts line 232
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.frame_header_n line 235
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldSeedStep line 239
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.copyOldTrace line 252
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldStageTrace line 267
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_offset line 277
30. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerData line 290
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerSeedStep line 298
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.copyOwnerTrace line 316
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerPlacement line 330
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerInitialData_eq line 342
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerBodyTrace line 345
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardStep line 361
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardExit line 375
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerIncrementStep line 386
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefix line 406
40. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed line 409
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefixTrace line 416
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopTrace line 446
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerStageTrace line 458
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.owner_output_eq_ownerPrefix line 468
45. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleaned line 484
46. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime line 489
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.drainTrace line 494
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupPrefixTrace line 502
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTrace line 516
50. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.finalStacks line 522
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_finalStacks line 525
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_length_le line 545
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_le line 559
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_final_le line 575
55. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerOutput line 639
56. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldOutput line 642
57. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput line 645
58. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.totalTime line 648
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.old_output_eq_originalPrefix line 654
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput_eq line 659