OAI/Computability/BinPacking/CookLevin/ValidityComposition.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.rowMap line 14
2. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.Ready line 16
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.Ready.emitted line 20
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.ext_slots line 28
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.frame line 38
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.closurePorts line 41
7. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.CopyContext line 49
8. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.(instance at line 53) line 53
9. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.CopyLabel line 57
10. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.(instance at line 61) line 61
11. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.Label line 65
12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.copyTarget line 74
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.copyExit line 79
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.statement line 85
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.copySteps line 108
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.copyTrace line 110
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.closureTrace line 131
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.emitted_frame line 158
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.bodySteps line 167
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.bodySteps_eq line 170
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.bodyTrace line 174
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.counter_frame line 285
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.loopTokens line 293
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.loopTokens_succ line 296
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.loopSteps line 305
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.loopTrace line 309
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.bodyBudget line 338
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.bodySteps_le line 340
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.loopSteps_le line 348
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.steps line 358
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.trace line 361
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.bodyPolynomial line 446
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.timePolynomial line 451
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.timePolynomial_eval line 455
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.steps_le_time line 459
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.inTime line 465
37. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.machine line 477
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Full.machineInTime line 488
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.nonemptyMap line 505
40. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.Label line 507
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.statement line 513
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.steps line 522
43. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.timePolynomial line 524
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.timePolynomial_eval line 528
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.steps_le_time line 532
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.chain line 537
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.trace line 541
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.inTime line 576
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.machine line 592
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.machineTrace line 604
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Full.machineInTime line 611