OAI/Computability/VertexCover/PCP/FinalBooleanVerifier.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.Label line 33
2. def OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.bitIndex line 37
3. def OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits line 40
4. def OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels line 43
5. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits_bitsOfLabels line 48
6. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels_labelsOfBits line 53
7. abbrev OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.verifier line 58
8. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.query_tail line 68
9. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.query_head line 74
10. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.eventValue_eq line 80
11. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.count_false_map_filter line 88
12. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.count_false_finRange line 94
13. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.rejection_count_eq line 108
14. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.verifier_completeness line 124
15. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.verifier_reflects line 133
16. def OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf line 141
17. abbrev OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.OutputAssignment line 144
18. def OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.extractLabeling line 148
19. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_completeness line 152
20. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_count_bridge line 158
21. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.failedCount_zero_of_satisfied line 166
22. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.all_satisfied_of_rejectionCount_zero line 173
23. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_reflects line 184
24. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_satisfiable_iff line 194
25. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_clause_count line 199
26. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.twelve_query_auxiliary_factor line 203
27. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_variable_count line 205
28. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_nonempty line 210
29. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.cnf_gap line 214
30. abbrev OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.ReducedVertex line 228
31. abbrev OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.ReducedDart line 231
32. def OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF line 236
33. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_completeness line 241
34. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_clause_count line 247
35. theorem OAI.UniqueGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_gap line 252