OAI/Combinatorics/ParityLifts/SAT.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.Complexity.Literal line 6
  2. structure OAI.ParityWL.Complexity.Clause line 8
  3. abbrev OAI.ParityWL.Complexity.Formula line 12
  4. def OAI.ParityWL.Complexity.Clause.Satisfied line 14
  5. def OAI.ParityWL.Complexity.Formula.Satisfied line 17
  6. def OAI.ParityWL.Complexity.Formula.Satisfiable line 20
  7. def OAI.ParityWL.Complexity.encodeNat line 25

    Source documentation

    Self-delimiting binary natural numbers, followed by the explicit formula. The clause width is encoded even for an empty clause.

    def encodeNat (n : ℕ) : List Bool :=
…
  8. def OAI.ParityWL.Complexity.encodeClause line 28
  9. def OAI.ParityWL.Complexity.encodeFormula line 31
  10. lemma OAI.ParityWL.Complexity.treeEncode_ticks line 39
  11. def OAI.ParityWL.Complexity.PolyProgram.ticks line 44
  12. def OAI.ParityWL.Complexity.PolyProgram.natSucc line 47
  13. def OAI.ParityWL.Complexity.PolyProgram.natPred line 50
  14. def OAI.ParityWL.Complexity.PolyProgram.natZero line 53
  15. lemma OAI.ParityWL.Complexity.list_foldl_succ line 56
  16. def OAI.ParityWL.Complexity.PolyProgram.length line 62
  17. def OAI.ParityWL.Complexity.truePrefix line 76
  18. lemma OAI.ParityWL.Complexity.truePrefix_foldr line 81
  19. lemma OAI.ParityWL.Complexity.truePrefix_le line 87
  20. def OAI.ParityWL.Complexity.PolyProgram.truePrefix line 92
  21. def OAI.ParityWL.Complexity.listShift line 105
  22. lemma OAI.ParityWL.Complexity.listShift_size line 110
  23. def OAI.ParityWL.Complexity.PolyProgram.listShift line 116
  24. lemma OAI.ParityWL.Complexity.fold_shift line 122
  25. def OAI.ParityWL.Complexity.PolyProgram.splitAt line 135
  26. def OAI.ParityWL.Complexity.readNatBits line 152
  27. def OAI.ParityWL.Complexity.PolyProgram.readNatBits line 156
  28. lemma OAI.ParityWL.Complexity.truePrefix_encodeNat line 164
  29. lemma OAI.ParityWL.Complexity.readNatBits_encode line 173
  30. lemma OAI.ParityWL.Complexity.readNatBits_sizes line 178
  31. abbrev OAI.ParityWL.Complexity.BitLiteral line 186
  32. abbrev OAI.ParityWL.Complexity.BitClause line 187
  33. def OAI.ParityWL.Complexity.readLiteral line 189
  34. def OAI.ParityWL.Complexity.PolyProgram.readLiteral line 193
  35. def OAI.ParityWL.Complexity.readLiterals line 200
  36. def OAI.ParityWL.Complexity.PolyProgram.readLiterals line 207
  37. def OAI.ParityWL.Complexity.readWidth line 218
  38. lemma OAI.ParityWL.Complexity.readWidth_le line 222
  39. lemma OAI.ParityWL.Complexity.readWidth_bits line 224
  40. def OAI.ParityWL.Complexity.readClause line 227
  41. def OAI.ParityWL.Complexity.PolyProgram.readClause line 231
  42. lemma OAI.ParityWL.Complexity.readNatBits_remainder line 242
  43. lemma OAI.ParityWL.Complexity.readNatBits_consumes line 245
  44. lemma OAI.ParityWL.Complexity.readNatBits_account line 251
  45. lemma OAI.ParityWL.Complexity.readLiteral_remainder line 256
  46. lemma OAI.ParityWL.Complexity.readLiteral_account line 260
  47. lemma OAI.ParityWL.Complexity.readLiterals_remainder line 269
  48. lemma OAI.ParityWL.Complexity.readLiterals_account line 275
  49. lemma OAI.ParityWL.Complexity.readClause_consumes line 286
  50. lemma OAI.ParityWL.Complexity.readClause_account line 289
  51. lemma OAI.ParityWL.Complexity.readLiteral_encode line 298
  52. lemma OAI.ParityWL.Complexity.readLiterals_encode line 302
  53. lemma OAI.ParityWL.Complexity.readClause_encode line 309