OAI/Computability/MinUncut/PCP/Generator.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.prefixPolynomial line 17
  2. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.timePolynomial line 20
  3. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.beforeFinish line 24
  4. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.enterFinishInTime line 28
  5. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.prefixInTime line 44
  6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.output_empty line 60
  7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.halted_configuration line 67
  8. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.outputInTime line 86
  9. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.computableInPolyTime line 112
  10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.finite_work_alphabets line 131
  11. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.forErrorComputableInPolyTime line 137
  12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.forError_finite_work_alphabets line 145
  13. structure OAI.MinUncutGames.Foundations.PCP.ConstraintGraph line 157
  14. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.head line 168
  15. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.head_reverse line 170
  16. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.edgeSatisfied line 174
  17. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.edgeSatisfied_reverse line 177
  18. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.Satisfiable line 183
  19. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectedDarts line 186
  20. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectionCount line 189
  21. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.mem_rejectedDarts line 192
  22. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectionCount_le line 197
  23. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejected_exists_of_not_satisfiable line 201
  24. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectionCount_positive line 213