OAI/Computability/VertexCover/Encoding/Runtime.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Complexity.Runtime.statementPushBound line 41
  2. def OAI.UniqueGames.Foundations.Complexity.Runtime.maxLabelPushes line 51
  3. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.maxLabelPushes_ge line 56
  4. def OAI.UniqueGames.Foundations.Complexity.Runtime.programPushBound line 68
  5. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.statement_le_programPushBound line 71
  6. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.stepAuxStackLength line 76
  7. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.iterateSizeBound line 119
  8. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.executionSizeBound line 131
  9. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.stepStackLength line 154
  10. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.initialStackLength line 167
  11. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.haltedOutputLength line 174
  12. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.outputLength_le line 178
  13. theorem OAI.UniqueGames.Foundations.Complexity.Runtime.encodedOutputLength line 190