OAI/Computability/VertexCover/PCP/VerifierToCNF.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.VerifierToCNF.BoolTriple line 34
2. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.tripleValue line 36
3. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.chainView line 38
4. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.fillBits line 43
5. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.chainView_length line 51
6. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.chainView_sound line 75
7. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.fillBits_length line 102
8. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.fillBits_correct line 118
9. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.zero_false_count_iff_all line 137
10. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.chainView_failed line 143
11. abbrev OAI.UniqueGames.Foundations.PCP.VerifierToCNF.Pattern line 155
12. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.patterns line 157
13. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.flatMap_pair_length line 161
14. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.patterns_length line 170
15. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.mem_patterns line 177
16. abbrev OAI.UniqueGames.Foundations.PCP.VerifierToCNF.PatternIndex line 198
17. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.patternAt line 199
18. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.patternAt_surjective line 201
19. structure OAI.UniqueGames.Foundations.PCP.VerifierToCNF.FiniteVerifier line 206
20. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.eventValue line 212
21. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.rejectedEventCount line 215
22. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.auxiliaryCount line 218
23. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.outputVariables line 221
24. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.oldIndex line 223
25. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.freshIndex line 226
26. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.freshIndex_value line 230
27. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.liftLiteral line 236
28. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral line 239
29. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.forbiddenClause line 243
30. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.auxiliaryNames line 247
31. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.splitLong line 251
32. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.tautology line 257
33. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.block line 262
34. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.eventBlock line 267
35. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.convert line 271
36. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.clauseFailures line 275
37. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.splitLong_values line 278
38. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.splitLong_length line 301
39. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.restrictAssignment line 310
40. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.mismatchBits line 314
41. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.mismatchBits_length line 318
42. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral_false line 322
43. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.forbiddenClause_values line 328
44. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.mismatchBits_false line 335
45. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.mismatchBits_true line 345
46. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.mismatchFill_length line 364
47. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.mismatchFill line 371
48. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.extendAssignment line 378
49. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.extend_old line 385
50. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.extend_fresh line 390
51. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.restrict_extend line 398
52. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.ofFn_getElem_of_length line 403
53. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.extended_auxiliary_values line 408
54. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.tautology_satisfied line 414
55. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.block_length line 419
56. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.block_honest line 432
57. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.length_flatMap_constant line 448
58. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.eventBlock_length line 459
59. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.convert_clause_count line 464
60. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.convert_nonempty line 470
61. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.convert_completeness line 479
62. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.clauseFailures_append line 487
63. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.clauseFailures_le_flatMap line 491
64. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.block_failed line 505
65. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.eventBlock_failed line 522
66. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.count_false_map_sum line 534
67. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.clauseFailures_flatMap line 540
68. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.nat_sum_map_le line 548
69. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.convert_count_bridge line 556
70. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.convert_gap line 569
71. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.twelve_query_factor line 584
72. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.twelve_query_clause_count line 586
73. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padLiteral line 590
74. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padClause line 593
75. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padTautology line 596
76. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padInput line 600
77. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padClause_eval line 604
78. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padTautology_satisfied line 607
79. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padInput_satisfiable_iff line 611
80. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padInput_clause_count line 632
81. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.padInput_nonempty line 635
82. def OAI.UniqueGames.Foundations.PCP.VerifierToCNF.prepareInput line 641
83. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.prepareInput_satisfiable_iff line 643
84. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.prepareInput_clause_count line 647
85. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.prepareInput_nonempty line 651
86. theorem OAI.UniqueGames.Foundations.PCP.VerifierToCNF.prepareInput_variable_bound line 657