OAI/Probability/SATComputability/FiniteEnumeration.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FixedClauseThreshold.Computability.words line 11
  2. theorem OAI.FixedClauseThreshold.Computability.mem_words line 15
  3. theorem OAI.FixedClauseThreshold.Computability.nodup_words line 24
  4. theorem OAI.FixedClauseThreshold.Computability.words_primrec line 37
  5. theorem OAI.FixedClauseThreshold.Computability.length_of_enumeration line 50
  6. def OAI.FixedClauseThreshold.Computability.clauseAlphabet line 65
  7. def OAI.FixedClauseThreshold.Computability.clauseWords line 67
  8. def OAI.FixedClauseThreshold.Computability.encodeClause line 70
  9. theorem OAI.FixedClauseThreshold.Computability.literal_count_ofFn line 73
  10. theorem OAI.FixedClauseThreshold.Computability.mem_clauseWords_iff line 83
  11. theorem OAI.FixedClauseThreshold.Computability.encodeClause_injective line 104
  12. def OAI.FixedClauseThreshold.Computability.formulaWords line 110
  13. def OAI.FixedClauseThreshold.Computability.encodeFormula line 113
  14. theorem OAI.FixedClauseThreshold.Computability.encodeFormula_injective line 116
  15. theorem OAI.FixedClauseThreshold.Computability.mem_formulaWords_iff line 123
  16. theorem OAI.FixedClauseThreshold.Computability.formulaWords_length line 144
  17. def OAI.FixedClauseThreshold.Computability.clauseHolds line 150
  18. instance OAI.FixedClauseThreshold.Computability.(instance at line 153) line 153
  19. def OAI.FixedClauseThreshold.Computability.formulaHolds line 157
  20. instance OAI.FixedClauseThreshold.Computability.(instance at line 160) line 160
  21. def OAI.FixedClauseThreshold.Computability.formulaSatisfiable line 164
  22. instance OAI.FixedClauseThreshold.Computability.(instance at line 167) line 167
  23. theorem OAI.FixedClauseThreshold.Computability.clauseHolds_ofFn line 171
  24. theorem OAI.FixedClauseThreshold.Computability.formulaHolds_ofFn line 180
  25. theorem OAI.FixedClauseThreshold.Computability.formulaSatisfiable_encode line 189
  26. def OAI.FixedClauseThreshold.Computability.satisfiableWords line 203
  27. theorem OAI.FixedClauseThreshold.Computability.satisfiableWords_length line 206
  28. def OAI.FixedClauseThreshold.Computability.enumeratedProbability line 221
  29. theorem OAI.FixedClauseThreshold.Computability.enumeratedProbability_eq line 224
  30. theorem OAI.FixedClauseThreshold.Computability.clauseWords_primrec line 229
  31. theorem OAI.FixedClauseThreshold.Computability.formulaWords_primrec line 241
  32. theorem OAI.FixedClauseThreshold.Computability.clauseHolds_primrec line 247
  33. theorem OAI.FixedClauseThreshold.Computability.formulaHolds_primrec line 257
  34. theorem OAI.FixedClauseThreshold.Computability.formulaSatisfiable_primrec line 262
  35. theorem OAI.FixedClauseThreshold.Computability.satisfiableWords_primrec line 266
  36. theorem OAI.FixedClauseThreshold.Computability.rationalProbability_computable line 272
  37. theorem OAI.FixedClauseThreshold.Computability.probabilities_map_computable line 283
  38. theorem OAI.FixedClauseThreshold.Computability.cap_computable line 293
  39. theorem OAI.FixedClauseThreshold.Computability.rationalCenter_computable line 297