OAI/Computability/MinUncut/Machines/MachineCloudPadding.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes line 17
2. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.label line 23
3. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.configuration line 27
4. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.statement line 32
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_apply line 47
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_update line 53
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.stepAux_simulation line 72
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.step_simulation line 99
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Placement.trace line 119
10. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Tape line 136
11. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Tape.enumList line 140
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Tape.enumList_getElem?_ctorIdx_eq line 143
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Tape.enumList_nodup line 147
14. instance OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.(instance at line 149) line 149
15. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Label line 153
16. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.Alphabet line 159
17. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.State line 160
18. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.memory line 162
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.update_count line 175
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.update_scratch line 178
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.update_power line 181
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.update_level line 185
23. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.countTape line 189
24. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.countView line 197
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.countView_left line 206
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.countView_right line 208
27. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.powerTape line 212
28. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.powerView line 222
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.powerView_left line 233
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.powerView_right line 235
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.countMemory line 239
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.powerMemory line 244
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.countTapes line 249
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.powerTapes line 254
35. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.subtractLoop line 261
36. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.program line 269
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.appendTrace line 284
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.countTrace line 288
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.powerTrace line 304
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.subtractStep_zero line 319
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.subtractStep_succ line 329
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.subtractScanTrace line 339
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.subtractTrace line 362
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.branchStep_zero line 382
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.branchStep_succ line 390
46. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.padding line 399
47. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.postTime line 401
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.postTrace line 404
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.initStep line 432
50. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.totalTime line 439
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingTrace line 443
52. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.inputLength line 464
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.count_length_le line 467
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.table_length_le line 474
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.postTime_le line 479
56. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.timePolynomial line 485
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.totalTime_le line 488
58. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingInTime line 503
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPadding.count_add_padding line 519