OAI/Combinatorics/IndependentSets/Encoding/BinaryNormalize.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LargeIndependentSets.BinaryNormalize.varCount line 11
  2. def OAI.LargeIndependentSets.BinaryNormalize.dense line 13
  3. def OAI.LargeIndependentSets.BinaryNormalize.constant line 16
  4. def OAI.LargeIndependentSets.BinaryNormalize.triple line 18
  5. def OAI.LargeIndependentSets.BinaryNormalize.tautology line 20
  6. def OAI.LargeIndependentSets.BinaryNormalize.unitClause line 23
  7. def OAI.LargeIndependentSets.BinaryNormalize.sourceClause line 26
  8. def OAI.LargeIndependentSets.BinaryNormalize.eventAt line 30
  9. def OAI.LargeIndependentSets.BinaryNormalize.row line 33
  10. def OAI.LargeIndependentSets.BinaryNormalize.normalize line 39
  11. lemma OAI.LargeIndependentSets.BinaryNormalize.literal_eval_iff line 42
  12. lemma OAI.LargeIndependentSets.BinaryNormalize.triple_eval line 46
  13. lemma OAI.LargeIndependentSets.BinaryNormalize.foldr_bits line 50
  14. lemma OAI.LargeIndependentSets.BinaryNormalize.tautology_eval line 55
  15. lemma OAI.LargeIndependentSets.BinaryNormalize.unitClause_eval line 59
  16. lemma OAI.LargeIndependentSets.BinaryNormalize.eventAt_iff line 63
  17. def OAI.LargeIndependentSets.BinaryNormalize.Realizes line 68
  18. lemma OAI.LargeIndependentSets.BinaryNormalize.raw_literal line 72
  19. lemma OAI.LargeIndependentSets.BinaryNormalize.dense_eval_iff line 77
  20. lemma OAI.LargeIndependentSets.BinaryNormalize.exists_realizes_forward line 85
  21. lemma OAI.LargeIndependentSets.BinaryNormalize.exists_realizes_backward line 93
  22. lemma OAI.LargeIndependentSets.BinaryNormalize.sourceClause_one line 113
  23. lemma OAI.LargeIndependentSets.BinaryNormalize.sourceClause_two line 121
  24. lemma OAI.LargeIndependentSets.BinaryNormalize.sourceClause_three line 134
  25. def OAI.LargeIndependentSets.BinaryNormalize.PairSatisfied line 151
  26. lemma OAI.LargeIndependentSets.BinaryNormalize.pair_first line 154
  27. lemma OAI.LargeIndependentSets.BinaryNormalize.pair_empty line 159
  28. lemma OAI.LargeIndependentSets.BinaryNormalize.pair_none line 163
  29. lemma OAI.LargeIndependentSets.BinaryNormalize.atClause line 167
  30. lemma OAI.LargeIndependentSets.BinaryNormalize.pairs_iff line 214
  31. lemma OAI.LargeIndependentSets.BinaryNormalize.formula_atClause line 234
  32. theorem OAI.LargeIndependentSets.BinaryNormalize.satisfiable_iff line 255