OAI/Combinatorics/IndependentSets/Encoding/TargetFormula.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LargeIndependentSets.Normalization.TargetFormula line 11
  2. abbrev OAI.LargeIndependentSets.Normalization.TargetClause line 12
  3. abbrev OAI.LargeIndependentSets.Normalization.TargetLiteral line 13
  4. def OAI.LargeIndependentSets.Normalization.names line 15
  5. def OAI.LargeIndependentSets.Normalization.nameIndex line 17
  6. def OAI.LargeIndependentSets.Normalization.literal line 20
  7. def OAI.LargeIndependentSets.Normalization.pad line 23
  8. def OAI.LargeIndependentSets.Normalization.clause line 26
  9. lemma OAI.LargeIndependentSets.Normalization.literal_eval_true line 29
  10. lemma OAI.LargeIndependentSets.Normalization.clause_eval_true line 36
  11. lemma OAI.LargeIndependentSets.Normalization.name_mem line 55
  12. lemma OAI.LargeIndependentSets.Normalization.lookup_variable line 59
  13. def OAI.LargeIndependentSets.Normalization.contradiction line 65
  14. lemma OAI.LargeIndependentSets.Normalization.contradiction_unsat line 69
  15. def OAI.LargeIndependentSets.Normalization.normalize line 78
  16. lemma OAI.LargeIndependentSets.Normalization.normalize_satisfiable_iff line 82