OAI/Computability/PerfectCompleteness/Foundations/PCPSource.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.PCPSource.baseTable line 18
  2. theorem OAI.PerfectCompleteness.PCPSource.baseTable_certificate line 21
  3. def OAI.PerfectCompleteness.PCPSource.rawFormula line 25
  4. def OAI.PerfectCompleteness.PCPSource.normalizedFormula line 27
  5. theorem OAI.PerfectCompleteness.PCPSource.rawFormula_nonempty line 29
  6. theorem OAI.PerfectCompleteness.PCPSource.normalizedFormula_nonempty line 32
  7. theorem OAI.PerfectCompleteness.PCPSource.normalizedFormula_satisfiable_iff line 35
  8. theorem OAI.PerfectCompleteness.PCPSource.normalizedFormula_distinct line 40
  9. def OAI.PerfectCompleteness.PCPSource.baseDenominator line 45
  10. def OAI.PerfectCompleteness.PCPSource.sourceDenominator line 47
  11. def OAI.PerfectCompleteness.PCPSource.sourceGap line 49
  12. theorem OAI.PerfectCompleteness.PCPSource.baseDenominator_pos line 51
  13. theorem OAI.PerfectCompleteness.PCPSource.sourceDenominator_pos line 54
  14. theorem OAI.PerfectCompleteness.PCPSource.sourceGap_pos line 57
  15. theorem OAI.PerfectCompleteness.PCPSource.sourceGap_le_one line 61
  16. theorem OAI.PerfectCompleteness.PCPSource.finalClauseGap_eq line 66
  17. theorem OAI.PerfectCompleteness.PCPSource.sourceGap_eq line 69
  18. theorem OAI.PerfectCompleteness.PCPSource.rawFormula_count_gap line 73
  19. theorem OAI.PerfectCompleteness.PCPSource.normalizedFormula_count_gap line 95
  20. def OAI.PerfectCompleteness.PCPSource.clauseFamily line 103
  21. instance OAI.PerfectCompleteness.PCPSource.clauseCount_neZero line 110
  22. theorem OAI.PerfectCompleteness.PCPSource.failedCount_eq_fin_sum line 113
  23. theorem OAI.PerfectCompleteness.PCPSource.violatedCount_eq_failedCount line 120
  24. theorem OAI.PerfectCompleteness.PCPSource.clauseGap line 127
  25. def OAI.PerfectCompleteness.PCPSource.source line 140
  26. theorem OAI.PerfectCompleteness.PCPSource.source_complete line 142
  27. theorem OAI.PerfectCompleteness.PCPSource.source_sound line 147
  28. def OAI.PerfectCompleteness.PCPSource.repetitionLength line 151
  29. theorem OAI.PerfectCompleteness.PCPSource.repetitionLength_positive line 154
  30. def OAI.PerfectCompleteness.PCPSource.amplifiedSource line 157
  31. theorem OAI.PerfectCompleteness.PCPSource.amplifiedSource_complete line 160
  32. theorem OAI.PerfectCompleteness.PCPSource.amplifiedSource_sound line 166
  33. def OAI.PerfectCompleteness.PCPSource.binarySource line 171
  34. theorem OAI.PerfectCompleteness.PCPSource.binarySource_complete line 173
  35. theorem OAI.PerfectCompleteness.PCPSource.binarySource_sound line 177
  36. def OAI.PerfectCompleteness.PCPSource.binaryAmplifiedSource line 181
  37. theorem OAI.PerfectCompleteness.PCPSource.binaryAmplifiedSource_complete line 184
  38. theorem OAI.PerfectCompleteness.PCPSource.binaryAmplifiedSource_sound line 189