OAI/Computability/MinUncut/Machines/LoopInitialization.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.LoopInitialization.initialization_ready line 12
2. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.zeroGuardInTime line 48
3. structure OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.LoopResult line 62
4. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.runRemaining line 74
5. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.prefixTime line 106
6. structure OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult line 122
7. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.runPrefix line 132
8. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.reversed line 155
9. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.output line 159
10. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal line 173
11. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_output line 176
12. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_reversed line 180
13. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.finishBudget line 184
14. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.reverseInTime line 187
15. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.cleared_eq_haltList line 201
16. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.cleanupInTime line 208
17. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.finishInTime line 224
18. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_selected_length_le line 245
19. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.stackLength_after_prefix line 252
20. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.finishBudget_le_of_prefix line 264
21. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.completedPolynomial line 286
22. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPrefix line 291
23. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPolynomialPrefix line 307
24. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial line 331
25. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial_eval line 337
26. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Runtime.time line 344
27. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Runtime.tableOutputsInTime line 347
28. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Runtime.tablePolynomialTime line 363
29. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.ExtraTape line 390
30. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList line 394
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_getElem?_ctorIdx_eq line 396
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_nodup line 400
33. instance OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.(instance at line 402) line 402
34. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.Phase line 405
35. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.Phase.enumList line 409
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.Phase.enumList_getElem?_ctorIdx_eq line 412
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.Phase.enumList_nodup line 416
38. instance OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.(instance at line 418) line 418
39. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.Tape line 422
40. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.Symbols line 423
41. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.Label line 424
42. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.State line 425
43. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.extraTapes line 427
44. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.auxProgram line 433
45. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.program line 454
46. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.machine line 458
47. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.inputTapes line 476
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.inputTapes_input line 479
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.inputTapes_counter line 483
50. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.inputConfig line 486
51. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.embedded line 490
52. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.temporaryTapes line 495
53. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.temporaryConfig line 498
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.inputTapes_update_input line 502
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.inputTapes_update_counter line 514
56. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.oneStep line 523
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.parseStep_true line 531
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.parseStep_false line 540
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.parseTrace line 549
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.guardStep_some line 575
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.guardStep_none line 584
62. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.bodyExecution line 591
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.bodyToTemp_tapes line 601
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.tempToBody_tapes line 617
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.finalToTemp_tapes line 629
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.tempToOutput_tapes line 641
67. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.bodyToTemp line 653
68. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.tempToBody line 669
69. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.finalToTemp line 684
70. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.tempToOutput line 696
71. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.bodyReturn line 709
72. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.finish line 720
73. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.loopBudget line 732
74. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.loopExecution line 737
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.inputConfig_init line 775
76. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.executeSequence line 787
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.loopBudget_eq_sum line 814
78. def OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.executeSequenceSum line 825
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRepeat.loopBudget_le line 838