OAI/Computability/MinUncut/PCP/TupleBound.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.clauseRank_le_power line 14
  2. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.variableRank_le_power line 20
  3. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.leftValue_le_numberBound line 27
  4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.rightValue_le_numberBound line 33
  5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.leftBlock_le_numberBound line 38
  6. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.rankPolynomial line 46
  7. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.numberPolynomial line 47
  8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.rankPolynomial_eval line 50
  9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.numberPolynomial_eval line 52
  10. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.slotPolynomial line 56
  11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.slotPolynomial_eval line 63
  12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.slotBudget_le line 72
  13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.prefixBudget_le line 91
  14. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.preparePolynomial line 105
  15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.preparePolynomial_eval line 110
  16. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.setupPolynomial line 117
  17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.setupPolynomial_eval line 123
  18. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.finishPolynomial line 131
  19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.finishPolynomial_eval line 135
  20. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.bodyPolynomial line 141
  21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.setupBudget_le line 144
  22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.finishBudget_le line 161
  23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.bodyBudget_le line 168
  24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.fixed_parameters_body_bound line 177
  25. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleBound.bodyInPolynomialTime line 182
  26. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.accumulatorRole line 214
  27. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.leafTapes line 217
  28. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_accumulator line 222
  29. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_work_blank line 226
  30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_ready line 235
  31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.body_result_leaf line 262
  32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.source_initial line 272
  33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.actual_bodies line 276
  34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.resetDigits_ready line 299
  35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.allBits_eq_records line 305
  36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.accumulated_eq_input line 316
  37. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput line 328
  38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_accumulator line 332
  39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_frame line 337
  40. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.resetLabel line 342
  41. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalInTime line 345
  42. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.timePolynomial line 389
  43. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalInPolynomialTime line 392