OAI/Computability/VertexCover/PCP/RawInitialMachineBudget.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.nameSumline 45 - def
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.bodyTimeline 48 - def
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.loopTimeline 52 - theorem
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.nameSum_leline 56 - theorem
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.bodyTime_leline 63 - theorem
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.loopTime_leline 70 - theorem
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.input_header_boundline 92 - theorem
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.graph_size_boundline 98 - def
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.fullBudgetline 105 - def
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.timePolynomialline 109 - theorem
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.timePolynomial_evalline 113 - theorem
OAI.UniqueGames.Foundations.PCP.RawInitialMachineBudget.fullBudget_leline 117