OAI/Combinatorics/IndependentSets/Machines/MachineCloudPadding.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes line 17
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.label line 23
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.configuration line 27
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.statement line 32
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_apply line 47
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_update line 53
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.stepAux_simulation line 72
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.step_simulation line 99
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Placement.trace line 119
10. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Tape line 136
11. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.(instance at line 140) line 140
12. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Label line 144
13. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.Alphabet line 150
14. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.State line 151
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.memory line 153
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.update_count line 166
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.update_scratch line 169
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.update_power line 172
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.update_level line 176
20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.countTape line 180
21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.countView line 188
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.countView_left line 197
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.countView_right line 199
24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.powerTape line 203
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.powerView line 213
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.powerView_left line 224
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.powerView_right line 226
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.countMemory line 230
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.powerMemory line 235
30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.countTapes line 240
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.powerTapes line 245
32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.subtractLoop line 252
33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.program line 260
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.appendTrace line 275
35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.countTrace line 279
36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.powerTrace line 295
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.subtractStep_zero line 310
38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.subtractStep_succ line 320
39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.subtractScanTrace line 330
40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.subtractTrace line 353
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.branchStep_zero line 373
42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.branchStep_succ line 381
43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.padding line 390
44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.postTime line 392
45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.postTrace line 395
46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.initStep line 423
47. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.totalTime line 430
48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingTrace line 434
49. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.inputLength line 455
50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.count_length_le line 458
51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.table_length_le line 465
52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.postTime_le line 470
53. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.timePolynomial line 476
54. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.totalTime_le line 479
55. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingInTime line 494
56. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPadding.count_add_padding line 510