OAI/Computability/DirectedFeedback/Encoding/VerifierCNF.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.PCP.VerifierToCNF.BoolTriple line 10
  2. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.tripleValue line 12
  3. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.chainView line 14
  4. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.fillBits line 19
  5. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.chainView_length line 27
  6. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.chainView_sound line 51
  7. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.fillBits_length line 78
  8. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.fillBits_correct line 94
  9. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.zero_false_count_iff_all line 113
  10. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.chainView_failed line 119
  11. abbrev OAI.DFVSGames.Foundations.PCP.VerifierToCNF.Pattern line 131
  12. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.patterns line 133
  13. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.flatMap_pair_length line 137
  14. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.patterns_length line 146
  15. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.mem_patterns line 153
  16. abbrev OAI.DFVSGames.Foundations.PCP.VerifierToCNF.PatternIndex line 174
  17. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.patternAt line 175
  18. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.patternAt_surjective line 177
  19. structure OAI.DFVSGames.Foundations.PCP.VerifierToCNF.FiniteVerifier line 182
  20. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.eventValue line 188
  21. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.rejectedEventCount line 191
  22. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.auxiliaryCount line 194
  23. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.outputVariables line 197
  24. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.oldIndex line 199
  25. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.freshIndex line 202
  26. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.freshIndex_value line 206
  27. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.liftLiteral line 212
  28. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral line 215
  29. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.forbiddenClause line 219
  30. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.auxiliaryNames line 223
  31. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.splitLong line 227
  32. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.tautology line 233
  33. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.block line 238
  34. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.eventBlock line 243
  35. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.convert line 247
  36. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.clauseFailures line 251
  37. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.splitLong_values line 254
  38. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.splitLong_length line 277
  39. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.restrictAssignment line 286
  40. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.mismatchBits line 290
  41. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.mismatchBits_length line 294
  42. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral_false line 298
  43. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.forbiddenClause_values line 304
  44. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.mismatchBits_false line 311
  45. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.mismatchBits_true line 321
  46. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.mismatchFill_length line 340
  47. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.mismatchFill line 347
  48. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.extendAssignment line 354
  49. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.extend_old line 361
  50. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.extend_fresh line 366
  51. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.restrict_extend line 374
  52. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.ofFn_getElem_of_length line 379
  53. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.extended_auxiliary_values line 384
  54. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.tautology_satisfied line 390
  55. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.block_length line 395
  56. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.block_honest line 408
  57. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.length_flatMap_constant line 424
  58. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.eventBlock_length line 435
  59. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.convert_clause_count line 440
  60. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.convert_nonempty line 446
  61. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.convert_completeness line 455
  62. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.clauseFailures_append line 463
  63. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.clauseFailures_le_flatMap line 467
  64. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.block_failed line 481
  65. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.eventBlock_failed line 498
  66. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.count_false_map_sum line 510
  67. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.clauseFailures_flatMap line 516
  68. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.nat_sum_map_le line 524
  69. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.convert_count_bridge line 532
  70. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.convert_gap line 545
  71. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.twelve_query_factor line 560
  72. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.twelve_query_clause_count line 562
  73. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padLiteral line 566
  74. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padClause line 569
  75. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padTautology line 572
  76. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padInput line 576
  77. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padClause_eval line 580
  78. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padTautology_satisfied line 583
  79. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padInput_satisfiable_iff line 587
  80. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padInput_clause_count line 608
  81. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.padInput_nonempty line 611
  82. def OAI.DFVSGames.Foundations.PCP.VerifierToCNF.prepareInput line 617
  83. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.prepareInput_satisfiable_iff line 619
  84. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.prepareInput_clause_count line 623
  85. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.prepareInput_nonempty line 627
  86. theorem OAI.DFVSGames.Foundations.PCP.VerifierToCNF.prepareInput_variable_bound line 633
  87. abbrev OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.Label line 643
  88. def OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.bitIndex line 647
  89. def OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits line 650
  90. def OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels line 653
  91. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits_bitsOfLabels line 658
  92. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels_labelsOfBits line 663
  93. abbrev OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.verifier line 668
  94. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.query_tail line 678
  95. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.query_head line 684
  96. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.eventValue_eq line 690
  97. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.count_false_map_filter line 698
  98. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.count_false_finRange line 704
  99. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.rejection_count_eq line 718
  100. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.verifier_completeness line 734
  101. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.verifier_reflects line 743
  102. def OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf line 751
  103. abbrev OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.OutputAssignment line 754
  104. def OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.extractLabeling line 758
  105. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_completeness line 762
  106. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_count_bridge line 768
  107. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.failedCount_zero_of_satisfied line 776
  108. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.all_satisfied_of_rejectionCount_zero line 783
  109. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_reflects line 794
  110. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_satisfiable_iff line 804
  111. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_clause_count line 809
  112. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.twelve_query_auxiliary_factor line 813
  113. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_variable_count line 815
  114. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_nonempty line 820
  115. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.cnf_gap line 824
  116. abbrev OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.ReducedVertex line 838
  117. abbrev OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.ReducedDart line 841
  118. def OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF line 846
  119. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_completeness line 851
  120. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_clause_count line 857
  121. theorem OAI.DFVSGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_gap line 862