OAI/Combinatorics/IndependentSets/Encoding/FinalTableFormula.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.output line 13
2. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.satisfiable_iff line 16
3. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.variable_count line 23
4. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.clause_count line 27
5. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.nonempty line 31
6. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.tableGraph_rejectionCount line 35
7. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.tableGraph_count_lower line 45
8. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.clauseGap line 54
9. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.total_size_le line 64
10. def OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.sizePolynomial line 71
11. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.sizePolynomial_eval line 76
12. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalTableFormula.formulaBits_length_le_polynomial line 80