OAI/Combinatorics/ParityLifts/ReducedCNF.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Sparsification.CNF line 9
  2. def OAI.Sparsification.Reduced line 11
  3. def OAI.Sparsification.Holds line 14
  4. def OAI.Sparsification.minimize line 17
  5. lemma OAI.Sparsification.minimize_reduced line 20
  6. lemma OAI.Sparsification.minimal_subclause line 25
  7. lemma OAI.Sparsification.minimize_holds line 37
  8. def OAI.Sparsification.Fresh line 47

    Source documentation

    A new clause has no old subclause, including no equal old clause.

    def Fresh (F A : CNF α) : Prop := ∀ D ∈ A, ∀ C ∈ F, ¬ C ⊆ D

    Mentions: OAI.Sparsification.CNF

  9. def OAI.Sparsification.prune line 49
  10. lemma OAI.Sparsification.prune_holds line 52
  11. lemma OAI.Sparsification.prune_reduced line 71
  12. structure OAI.Sparsification.Flower line 81
  13. lemma OAI.Sparsification.Flower.core_fresh line 91
  14. lemma OAI.Sparsification.Flower.petals_fresh line 104
  15. lemma OAI.Sparsification.Flower.petals_reduced line 114
  16. lemma OAI.Sparsification.Flower.branch_holds line 120
  17. def OAI.Sparsification.units line 145
  18. def OAI.Sparsification.binaries line 147
  19. def OAI.Sparsification.degree line 149
  20. lemma OAI.Sparsification.mem_units line 151
  21. lemma OAI.Sparsification.clause_eq_singleton line 155
  22. lemma OAI.Sparsification.units_prune line 161
  23. lemma OAI.Sparsification.units_disjoint_of_fresh line 178
  24. lemma OAI.Sparsification.units_card_of_singletons line 184
  25. lemma OAI.Sparsification.units_empty_of_binaries line 201
  26. lemma OAI.Sparsification.card_le_sum_degrees line 208
  27. lemma OAI.Sparsification.marked_card_bound line 216
  28. def OAI.Sparsification.survived line 223
  29. lemma OAI.Sparsification.degree_survived_le line 226
  30. lemma OAI.Sparsification.removed_card_bound line 232
  31. lemma OAI.Sparsification.units_prune_card line 255
  32. lemma OAI.Sparsification.unit_resource line 260
  33. lemma OAI.Sparsification.survived_binary_eq line 269
  34. lemma OAI.Sparsification.marked_binary_disjoint line 279
  35. lemma OAI.Sparsification.binary_resource line 285
  36. lemma OAI.Sparsification.degree_union_le line 295
  37. lemma OAI.Sparsification.degree_le_of_subset line 302
  38. lemma OAI.Sparsification.binary_degree_invariant line 309