OAI/Computability/MinUncut/Machines/PoweringMachineRowHeaders.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement line 16
2. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_injective line 19
3. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_table line 23
4. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_query line 27
5. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scan line 31
6. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_reverse line 35
7. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scratch line 39
8. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_output line 43
9. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_start line 47
10. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_succ line 51
11. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.Label line 55
12. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.entry line 58
13. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.tailEntry line 60
14. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.affineInstruction line 63
15. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.instruction line 70
16. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.afterReverse line 83
17. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes line 88
18. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.steps line 97
19. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerTrace line 103
20. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_other line 175
21. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_shared line 198
22. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.steps_le line 212
23. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowHeaders.machine line 228
24. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.capacity line 248
25. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize line 249
26. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.State line 250
27. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.commands line 252
28. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.Label line 255
29. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.planMain line 259
30. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.plan_entry_eq line 266
31. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.entry line 273
32. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement line 276
33. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_output line 281
34. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_other line 286
35. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_injective line 292
36. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_excludes_data line 308
37. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.instruction line 320
38. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.afterPlan line 331
39. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.rowRelation line 335
40. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.rowWords line 340
41. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit line 345
42. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes line 352
43. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.planSteps line 360
44. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.planSteps_eq line 365
45. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.steps line 378
46. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.Ready line 383
47. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.plan_other line 388
48. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_data line 401
49. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_role line 408
50. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_ready line 418
51. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_data line 440
52. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_ready line 453
53. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_other line 478
54. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.rowBlock_eq_rowRelation line 497
55. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_output line 513
56. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.rowTrace line 542
57. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.budget line 594
58. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.steps_le line 598
59. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRowBody.rowInTime line 609