OAI/Computability/BinPacking/CookLevin/CircuitFinish.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Tape line 11
2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Tape.enumList line 15
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Tape.enumList_getElem?_ctorIdx_eq line 18
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Tape.enumList_nodup line 22
5. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.(instance at line 24) line 24
6. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Label line 28
7. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Label.enumList line 33
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Label.enumList_getElem?_ctorIdx_eq line 36
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Label.enumList_nodup line 40
10. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.(instance at line 42) line 42
11. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.Alphabet line 46
12. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.State line 47
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.memory line 49
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.update_current line 59
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.update_freeInputs line 62
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.update_root line 65
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.update_reversedRecords line 68
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.update_output line 71
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.update_gateCount line 74
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.update_scratch line 77
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.cancelLoop line 83
22. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.program line 89
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.appendTrace line 110
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.prependTrace line 114
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.cancelStep_zero line 172
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.cancelStep_succ line 182
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.cancelTrace line 193
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.initialTapes line 216
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.finalTapes line 219
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.totalTime line 222
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.finishTrace line 226
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.finalTapes_output line 273
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.finalTapes_clean line 276
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.totalTime_eq line 280
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.totalTime_le line 285
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.circuit_finalTapes line 291
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.circuitTrace line 299
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.circuitInTime line 309
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.placedCircuitInTime line 319