OAI/Combinatorics/IndependentSets/PCP/FinalCNFTemplate.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.Reference line 10
2. structure OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate line 15
3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate line 20
4. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.queryLiteral line 22
5. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.auxiliaryLiteral line 25
6. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.tautologyTemplate line 28
7. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.chainTemplates line 31
8. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.blockTemplates line 44
9. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.templates line 47
10. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.literalAt line 50
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.templates_length line 54
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.templates_true line 57
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.templates_false line 60
14. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates line 63
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates_length line 66
16. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.literalWords line 71
17. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.clauseWords line 74
18. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.words line 77
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.words_length line 80
20. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.resolve line 89
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.resolve_query_value line 93
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.resolve_auxiliary_value line 97
23. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.instantiateLiteral line 105
24. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause line 108
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.splitLong_twelve line 112
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates line 127
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates_of_acceptance line 141
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause_words line 148
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.words_eq_block line 152
30. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFTemplate.block_words_length line 160