OAI/Computability/BinPacking/CookLevin/PolynomialMachine.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial line 9
2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval line 13
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval_reverse line 19
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficients line 24
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients line 44
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.width line 47
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit line 49
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.digitBound line 52
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.le_sum_of_mem line 54
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit_le_bound line 64
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients_foldl line 70
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.range_map_digit line 77
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFields line 91
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes line 97
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_prependFields line 103
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes_apply line 113
17. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.popN line 127
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_popN line 132
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields line 143
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes line 148
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_clearFields line 153
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes_apply line 163
23. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.Layout line 181
24. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.Label line 182
25. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.State line 183
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldWord line 185
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices line 189
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices_nodup line 192
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.inl_not_mem_fields line 195
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.inr_mem_fields line 198
31. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.initialTapes line 201
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes line 204
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inl line 207
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inr line 212
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.slots line 217
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_clean line 219
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.innerLabels line 223
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.program line 226
39. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.machine line 236
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterHornerTapes line 247
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterInputTapes line 250
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.finalTapes line 253
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields_final line 256
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.initList_eq line 267
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.haltList_eq line 273
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.initializationTrace line 279
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.cleanupTrace line 289
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial line 306
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial line 310
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial_eval line 316
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial_eval line 322
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial line 332
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial_eval line 336
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerValue_eq_eval line 343
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerStageTrace line 349
56. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.outputsInTime line 363
57. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialMachine.computableInPolyTime line 382