OAI/Combinatorics/IndependentSets/Machines/GraphCounterPrefix.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.rawOutput line 12
  2. def OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.rawInTime line 15
  3. def OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.count line 39
  4. def OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.output line 41
  5. def OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.rowsBits line 44
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.tableBits_decomposition line 47
  7. def OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.outputsInTime line 51
  8. def OAI.IndependentSetsGames.Foundations.Complexity.GraphCounterPrefix.computableInPolyTime line 57
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.rounds line 80
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.rounds_le line 82
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.two_pow_rounds_le line 85
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.growth_pow_rounds_le line 92
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.sizeEnvelope line 100
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.semanticSize_geometric line 102
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.semanticSize_bound line 116
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial line 129
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial_eval line 132
  18. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.timePolynomial line 136
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.timePolynomial_eval line 141
  20. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.Alphabet line 149
  21. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.State line 150
  22. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.Labels line 151
  23. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.program line 153
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.program_guard line 161
  25. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.machine line 166
  26. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.haltedConfiguration line 179
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.haltStep line 184
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.iterationTrace line 194
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.bodyCosts_bound line 210
  30. def OAI.IndependentSetsGames.Foundations.Complexity.PCPIterationMachine.iterationInTime line 227