OAI/Combinatorics/IndependentSets/PCP/VerifierCNF.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.BoolTriple line 10
  2. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.tripleValue line 12
  3. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.chainView line 14
  4. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.fillBits line 19
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.chainView_length line 27
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.chainView_sound line 51
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.fillBits_length line 78
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.fillBits_correct line 94
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.zero_false_count_iff_all line 113
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.chainView_failed line 119
  11. abbrev OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.Pattern line 131
  12. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.patterns line 133
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.flatMap_pair_length line 137
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.patterns_length line 146
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.mem_patterns line 153
  16. abbrev OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.PatternIndex line 174
  17. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.patternAt line 175
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.patternAt_surjective line 177
  19. structure OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.FiniteVerifier line 182
  20. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.eventValue line 188
  21. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.rejectedEventCount line 191
  22. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.auxiliaryCount line 194
  23. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.outputVariables line 197
  24. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.oldIndex line 199
  25. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.freshIndex line 202
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.freshIndex_value line 206
  27. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.liftLiteral line 212
  28. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral line 215
  29. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.forbiddenClause line 219
  30. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.auxiliaryNames line 223
  31. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.splitLong line 227
  32. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.tautology line 233
  33. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.block line 238
  34. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.eventBlock line 243
  35. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.convert line 247
  36. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.clauseFailures line 251
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.splitLong_values line 254
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.splitLong_length line 277
  39. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.restrictAssignment line 286
  40. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.mismatchBits line 290
  41. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.mismatchBits_length line 294
  42. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral_false line 298
  43. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.forbiddenClause_values line 304
  44. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.mismatchBits_false line 311
  45. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.mismatchBits_true line 321
  46. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.mismatchFill_length line 340
  47. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.mismatchFill line 347
  48. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.extendAssignment line 354
  49. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.extend_old line 361
  50. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.extend_fresh line 366
  51. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.restrict_extend line 374
  52. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.ofFn_getElem_of_length line 379
  53. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.extended_auxiliary_values line 384
  54. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.tautology_satisfied line 390
  55. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.block_length line 395
  56. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.block_honest line 408
  57. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.length_flatMap_constant line 424
  58. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.eventBlock_length line 435
  59. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.convert_clause_count line 440
  60. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.convert_nonempty line 446
  61. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.convert_completeness line 455
  62. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.clauseFailures_append line 463
  63. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.clauseFailures_le_flatMap line 467
  64. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.block_failed line 481
  65. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.eventBlock_failed line 498
  66. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.count_false_map_sum line 510
  67. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.clauseFailures_flatMap line 516
  68. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.nat_sum_map_le line 524
  69. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.convert_count_bridge line 532
  70. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.convert_gap line 545
  71. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.twelve_query_factor line 560
  72. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.twelve_query_clause_count line 562
  73. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padLiteral line 566
  74. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padClause line 569
  75. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padTautology line 572
  76. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padInput line 576
  77. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padClause_eval line 580
  78. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padTautology_satisfied line 583
  79. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padInput_satisfiable_iff line 587
  80. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padInput_clause_count line 608
  81. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.padInput_nonempty line 611
  82. def OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.prepareInput line 617
  83. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.prepareInput_satisfiable_iff line 619
  84. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.prepareInput_clause_count line 623
  85. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.prepareInput_nonempty line 627
  86. theorem OAI.IndependentSetsGames.Foundations.PCP.VerifierToCNF.prepareInput_variable_bound line 633