OAI/Computability/PerfectCompleteness/Machines/BinaryFormulaLemmas.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BinaryFormula.clauseNames line 14
  2. def OAI.PerfectCompleteness.BinaryFormula.sourceNames line 17
  3. def OAI.PerfectCompleteness.BinaryFormula.activeNames line 20
  4. theorem OAI.PerfectCompleteness.BinaryFormula.literal_mem_active line 23
  5. def OAI.PerfectCompleteness.BinaryFormula.compactIndex line 31
  6. def OAI.PerfectCompleteness.BinaryFormula.decodeName line 35
  7. def OAI.PerfectCompleteness.BinaryFormula.compactLiteral line 38
  8. def OAI.PerfectCompleteness.BinaryFormula.compactClause line 42
  9. def OAI.PerfectCompleteness.BinaryFormula.compactClauses line 48
  10. def OAI.PerfectCompleteness.BinaryFormula.dense line 51
  11. def OAI.PerfectCompleteness.BinaryFormula.restrictAssignment line 55
  12. def OAI.PerfectCompleteness.BinaryFormula.extendAssignment line 58
  13. theorem OAI.PerfectCompleteness.BinaryFormula.decode_compactIndex line 62
  14. theorem OAI.PerfectCompleteness.BinaryFormula.compactIndex_injective line 66
  15. theorem OAI.PerfectCompleteness.BinaryFormula.compactLiteral_positive line 72
  16. theorem OAI.PerfectCompleteness.BinaryFormula.eval_compact_restrict line 75
  17. theorem OAI.PerfectCompleteness.BinaryFormula.eval_compact_extend line 81
  18. def OAI.PerfectCompleteness.BinaryFormula.evaluationList line 91
  19. theorem OAI.PerfectCompleteness.BinaryFormula.evaluationList_restrict line 94
  20. theorem OAI.PerfectCompleteness.BinaryFormula.evaluationList_extend line 102
  21. def OAI.PerfectCompleteness.BinaryFormula.failedCount line 116
  22. theorem OAI.PerfectCompleteness.BinaryFormula.failedCount_restrict line 119
  23. theorem OAI.PerfectCompleteness.BinaryFormula.failedCount_extend line 123
  24. theorem OAI.PerfectCompleteness.BinaryFormula.clauseNames_flat_length line 127
  25. theorem OAI.PerfectCompleteness.BinaryFormula.dense_clause_count line 136
  26. theorem OAI.PerfectCompleteness.BinaryFormula.dense_variable_bound line 140
  27. theorem OAI.PerfectCompleteness.BinaryFormula.dense_completeness line 145
  28. theorem OAI.PerfectCompleteness.BinaryFormula.dense_reflects line 154
  29. theorem OAI.PerfectCompleteness.BinaryFormula.dense_satisfiable_iff line 164
  30. theorem OAI.PerfectCompleteness.BinaryFormula.dense_preserves_gap line 168
  31. theorem OAI.PerfectCompleteness.BinaryFormula.dense_encoding_bound line 175
  32. theorem OAI.PerfectCompleteness.BinaryEncoding.bitsValue_bits line 200
  33. def OAI.PerfectCompleteness.BinaryEncoding.frame line 207
  34. theorem OAI.PerfectCompleteness.BinaryEncoding.parseFrame_encoded line 211
  35. theorem OAI.PerfectCompleteness.BinaryEncoding.frame_length line 217
  36. def OAI.PerfectCompleteness.BinaryEncoding.nameBits line 223
  37. theorem OAI.PerfectCompleteness.BinaryEncoding.parseName_encoded line 225
  38. theorem OAI.PerfectCompleteness.BinaryEncoding.nameBits_length line 229
  39. theorem OAI.PerfectCompleteness.BinaryEncoding.nameBits_length_le_of_lt_pow line 233
  40. def OAI.PerfectCompleteness.BinaryEncoding.literalBits line 239
  41. theorem OAI.PerfectCompleteness.BinaryEncoding.parseLiteral_encoded line 242
  42. theorem OAI.PerfectCompleteness.BinaryEncoding.literalBits_length line 247
  43. def OAI.PerfectCompleteness.BinaryEncoding.clauseBits line 251
  44. theorem OAI.PerfectCompleteness.BinaryEncoding.clause_three_entries line 254
  45. theorem OAI.PerfectCompleteness.BinaryEncoding.parseClause_encoded line 260
  46. def OAI.PerfectCompleteness.BinaryEncoding.clauseNameSize line 264
  47. theorem OAI.PerfectCompleteness.BinaryEncoding.clauseBits_length line 267
  48. def OAI.PerfectCompleteness.BinaryEncoding.clausesBits line 272
  49. def OAI.PerfectCompleteness.BinaryEncoding.formulaBits line 276
  50. def OAI.PerfectCompleteness.BinaryEncoding.namesBitSize line 278
  51. theorem OAI.PerfectCompleteness.BinaryEncoding.namesBitSize_nil line 281
  52. theorem OAI.PerfectCompleteness.BinaryEncoding.namesBitSize_cons line 283
  53. theorem OAI.PerfectCompleteness.BinaryEncoding.clausesBits_length line 287
  54. theorem OAI.PerfectCompleteness.BinaryEncoding.formulaBits_length line 296
  55. theorem OAI.PerfectCompleteness.BinaryEncoding.clauses_length_lt_bits line 301
  56. def OAI.PerfectCompleteness.BinaryEncoding.ordinarySize line 306
  57. theorem OAI.PerfectCompleteness.BinaryEncoding.ordinarySize_le_bits line 309
  58. theorem OAI.PerfectCompleteness.BinaryEncoding.bits_le_three_ordinarySize line 315
  59. theorem OAI.PerfectCompleteness.BinaryEncoding.parseClauses_encoded line 321
  60. theorem OAI.PerfectCompleteness.BinaryEncoding.decodeFormula_encoded line 336
  61. theorem OAI.PerfectCompleteness.BinaryEncoding.formulaBits_injective line 345
  62. theorem OAI.PerfectCompleteness.BinaryEncoding.dense_encoding_bound line 350