OAI/Computability/VertexCover/PCP/FinalTableFormula.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.FinalTableFormula.output line 46
2. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.satisfiable_iff line 49
3. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.variable_count line 56
4. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.clause_count line 60
5. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.nonempty line 64
6. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.tableGraph_rejectionCount line 68
7. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.tableGraph_count_lower line 78
8. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.clauseGap line 87
9. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.total_size_le line 97
10. def OAI.UniqueGames.Foundations.PCP.FinalTableFormula.sizePolynomial line 104
11. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.sizePolynomial_eval line 109
12. theorem OAI.UniqueGames.Foundations.PCP.FinalTableFormula.formulaBits_length_le_polynomial line 113