OAI/Computability/PerfectCompleteness/Machines/PayloadRowsLoop.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.Ports line 15
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.Alphabet line 16
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.rowMap line 18
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.rowPorts line 24
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame line 26
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_index line 30
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_remaining line 33
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_capacity line 36
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.ext_ports line 39
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.update_remaining line 48
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.update_index line 56
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.update_capacity line 64
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_emitted line 68
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_ready line 77
15. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.Label line 109
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.rowLabels line 114
17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.statement line 118
18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.Agrees line 126
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.guardStep_zero line 130
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.guardStep_succ line 139
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.nextStep line 149
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.tokens line 166
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.steps line 170
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.trace line 174
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.steps_le line 217
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadRowsLoop.tokens_eq_forTokens line 227