OAI/Computability/MinUncut/Machines/RuntimeModel.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.BodyWork line 12
2. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.BodyExtra line 20
3. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.Arena line 21
4. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.QueryState line 22
5. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.ArithmeticState line 23
6. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.State line 24
7. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.QueryMetadata line 25
8. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.ArithmeticMetadata line 27
9. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.workTape line 32
10. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.variableHeader line 33
11. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.clauseHeader line 34
12. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.canonicalSignature line 36
13. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.canonicalState line 39
14. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.queryStateEquiv line 43
15. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.arithmeticStateEquiv line 49
16. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.rankControls line 55
17. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.clauseRankSlots line 65
18. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.variableRankSlots line 68
19. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.baseSlots line 71
20. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.querySources line 93
21. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.queryLayout line 98
22. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.perSlotCleanup line 110
23. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.finalBaseCleanup line 111
24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeModel.initializer_arena line 113
25. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial line 122
26. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval line 126
27. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval_reverse line 132
28. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficients line 137
29. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients line 157
30. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.width line 160
31. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit line 162
32. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.digitBound line 165
33. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.le_sum_of_mem line 167
34. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit_le_bound line 177
35. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients_foldl line 183
36. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.range_map_digit line 190
37. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFields line 204
38. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes line 210
39. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_prependFields line 216
40. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes_apply line 226
41. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.popN line 240
42. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_popN line 245
43. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields line 256
44. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes line 261
45. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_clearFields line 266
46. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes_apply line 276
47. abbrev OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.Layout line 294
48. abbrev OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.Label line 295
49. abbrev OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.State line 296
50. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldWord line 298
51. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices line 302
52. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices_nodup line 305
53. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.inl_not_mem_fields line 308
54. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.inr_mem_fields line 311
55. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.initialTapes line 314
56. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes line 317
57. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inl line 320
58. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inr line 325
59. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.slots line 330
60. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_clean line 332
61. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.innerLabels line 336
62. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.program line 339
63. abbrev OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.machine line 349
64. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterHornerTapes line 360
65. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterInputTapes line 363
66. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.finalTapes line 366
67. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields_final line 369
68. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.initList_eq line 380
69. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.haltList_eq line 386
70. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.initializationTrace line 392
71. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.cleanupTrace line 402
72. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial line 419
73. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial line 423
74. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial_eval line 429
75. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial_eval line 435
76. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial line 445
77. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial_eval line 449
78. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerValue_eq_eval line 456
79. theorem OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerStageTrace line 462
80. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.outputsInTime line 476
81. def OAI.MinUncutGames.Foundations.Complexity.CookLevin.PolynomialMachine.computableInPolyTime line 495