OAI/Computability/PerfectCompleteness/Machines/ClashMachine.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Alphabet line 17
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.State line 18
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.clean line 20
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.emitted line 22
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.emitted_output line 26
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.emitted_count line 31
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.emitted_other line 35
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.tokenBits_append line 39
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.emitted_append line 43
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.emitted_nil line 59
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.chain line 63
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.literal line 67
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.stepAux_literal line 73
14. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Input.Label line 82
15. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Input.(instance at line 86) line 86
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Input.statement line 94
17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Input.steps line 105
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Input.identity_output line 107
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Input.trace line 114
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.leftMap line 163
21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.rightMap line 164
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.inputLeftMap line 165
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.inputRightMap line 166
24. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.Label line 168
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.choose line 177
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.stepAux_choose line 182
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.statement line 187
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.offSteps line 204
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.offTrace line 206
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.steps line 247
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.trace line 251
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Pair.steps_le line 311
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.pairMap line 321
34. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.Label line 323
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.statement line 329
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.frame line 336
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.frame_current line 339
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.frame_remaining line 342
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.counter_frame line 345
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.emitted_frame line 353
41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.increment_frame line 367
42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.tokens line 372
43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.tokens_zero line 375
44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.tokens_succ line 377
45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.steps line 386
46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.trace line 390
47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Row.steps_le line 447