OAI/Computability/BinPacking/CookLevin/PayloadPresenceMachine.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Alphabet line 13
2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Ports line 14
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.presenceMap line 16
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.closing_distinct line 19
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.closurePorts line 23
6. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext line 26
7. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext.enumList line 30
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext.enumList_getElem?_ctorIdx_eq line 32
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext.enumList_nodup line 36
10. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.(instance at line 38) line 38
11. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Label line 42
12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.presenceLabels line 49
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copySource line 52
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copyTarget line 56
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copyExit line 61
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.statement line 66
17. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Ready line 79
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.Ready.emitted line 84
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.working line 93
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.steps line 98
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.chain line 102
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.copyTrace line 106
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.trace line 131
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.steps_le line 244
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadPresenceMachine.inTime line 249