OAI/Computability/BinPacking/CookLevin/InitializationMachineAt.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.Ports line 14
2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.Alphabet line 15
3. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.State line 16
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.initialState line 18
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.frame line 20
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.frame_at line 26
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.frame_other line 30
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.update_frame line 34
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.contents line 47
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.tapes line 56
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.tapes_at line 59
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.tapes_other line 64
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.update_remaining line 68
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.update_current line 77
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.update_threshold line 86
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.update_reversed line 95
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.update_count line 104
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.push_current line 113
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.statement line 121
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.Agrees line 137
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.chain line 141
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.inputTagStep line 145
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.identity_output line 155
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.indexTrace line 162
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.thresholdStep line 179
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.resultStep line 198
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.bodyTrace line 208
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.guardStep_zero line 246
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.guardStep_succ line 255
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.prepend_three line 270
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.selectorTrace line 276
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.selectorInTime line 309
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.increment_count line 322
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.standalone_agrees line 329
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.machine line 335
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.closurePorts line 346
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.presenceTrace line 354
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.presenceSteps_le line 401
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachineAt.presence_count line 410