OAI/Combinatorics/IndependentSets/PCP/FinalBooleanVerifier.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.Label line 11
2. def OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.bitIndex line 15
3. def OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits line 18
4. def OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels line 21
5. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits_bitsOfLabels line 26
6. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels_labelsOfBits line 31
7. abbrev OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.verifier line 36
8. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.query_tail line 46
9. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.query_head line 52
10. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.eventValue_eq line 58
11. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.count_false_map_filter line 66
12. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.count_false_finRange line 72
13. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.rejection_count_eq line 86
14. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.verifier_completeness line 102
15. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.verifier_reflects line 111
16. def OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf line 119
17. abbrev OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.OutputAssignment line 122
18. def OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.extractLabeling line 126
19. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_completeness line 130
20. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_count_bridge line 136
21. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.failedCount_zero_of_satisfied line 144
22. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.all_satisfied_of_rejectionCount_zero line 151
23. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_reflects line 162
24. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_satisfiable_iff line 172
25. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_clause_count line 177
26. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.twelve_query_auxiliary_factor line 181
27. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_variable_count line 183
28. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_nonempty line 188
29. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.cnf_gap line 192
30. abbrev OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.ReducedVertex line 206
31. abbrev OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.ReducedDart line 209
32. def OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF line 214
33. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_completeness line 219
34. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_clause_count line 225
35. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_gap line 230