OAI/Computability/BinPacking/PCP/FinalBooleanVerifier.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.Label line 10
2. def OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.bitIndex line 14
3. def OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits line 17
4. def OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels line 20
5. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits_bitsOfLabels line 25
6. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels_labelsOfBits line 30
7. abbrev OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.verifier line 35
8. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.query_tail line 45
9. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.query_head line 51
10. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.eventValue_eq line 57
11. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.count_false_map_filter line 65
12. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.count_false_finRange line 71
13. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.rejection_count_eq line 85
14. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.verifier_completeness line 101
15. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.verifier_reflects line 110
16. def OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf line 118
17. abbrev OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.OutputAssignment line 121
18. def OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.extractLabeling line 125
19. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_completeness line 129
20. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_count_bridge line 135
21. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.failedCount_zero_of_satisfied line 143
22. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.all_satisfied_of_rejectionCount_zero line 150
23. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_reflects line 161
24. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_satisfiable_iff line 171
25. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_clause_count line 176
26. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.twelve_query_auxiliary_factor line 180
27. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_variable_count line 182
28. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_nonempty line 187
29. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.cnf_gap line 191
30. abbrev OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.ReducedVertex line 205
31. abbrev OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.ReducedDart line 208
32. def OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF line 213
33. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_completeness line 218
34. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_clause_count line 224
35. theorem OAI.BinPackingGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_gap line 229