OAI/Computability/MinUncut/Machines/PCPIterationMachine.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.rounds line 12
  2. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.rounds_le line 14
  3. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.two_pow_rounds_le line 17
  4. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.growth_pow_rounds_le line 24
  5. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.sizeEnvelope line 32
  6. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.semanticSize_geometric line 34
  7. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.semanticSize_bound line 48
  8. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial line 61
  9. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial_eval line 64
  10. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.timePolynomial line 68
  11. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.timePolynomial_eval line 73
  12. abbrev OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.Alphabet line 81
  13. abbrev OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.State line 82
  14. abbrev OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.Labels line 83
  15. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.program line 85
  16. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.program_guard line 93
  17. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.machine line 98
  18. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.haltedConfiguration line 111
  19. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.haltStep line 116
  20. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.iterationTrace line 126
  21. theorem OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.bodyCosts_bound line 142
  22. def OAI.MinUncutGames.Foundations.Complexity.PCPIterationMachine.iterationInTime line 159