OAI/Combinatorics/IndependentSets/Machines/RawInitialMachineBudget.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.nameSum line 11
  2. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.bodyTime line 14
  3. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.loopTime line 18
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.nameSum_le line 22
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.bodyTime_le line 29
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.loopTime_le line 36
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.input_header_bound line 58
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.graph_size_bound line 64
  9. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.fullBudget line 71
  10. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.timePolynomial line 75
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.timePolynomial_eval line 79
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBudget.fullBudget_le line 83
  13. def OAI.IndependentSetsGames.Foundations.Complexity.Runtime.statementPushBound line 102
  14. def OAI.IndependentSetsGames.Foundations.Complexity.Runtime.maxLabelPushes line 112
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.maxLabelPushes_ge line 117
  16. def OAI.IndependentSetsGames.Foundations.Complexity.Runtime.programPushBound line 129
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.statement_le_programPushBound line 132
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.stepAuxStackLength line 137
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.iterateSizeBound line 180
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.executionSizeBound line 192
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.stepStackLength line 215
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.initialStackLength line 228
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.haltedOutputLength line 235
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.outputLength_le line 239
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.Runtime.encodedOutputLength line 251