OAI/Combinatorics/ParityLifts/SetLists.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.Complexity.dedupBy line 7
  2. lemma OAI.ParityWL.Complexity.fold_dedupBy_set line 10
  3. lemma OAI.ParityWL.Complexity.fold_dedupBy_nodup line 21
  4. lemma OAI.ParityWL.Complexity.dedupBy_set line 34
  5. lemma OAI.ParityWL.Complexity.dedupBy_nodup line 39
  6. lemma OAI.ParityWL.Complexity.fold_dedupBy_subset line 42
  7. lemma OAI.ParityWL.Complexity.dedupBy_subset line 52
  8. def OAI.ParityWL.Complexity.PolyProgram.dedupBy line 55
  9. abbrev OAI.ParityWL.Complexity.ClauseList line 76
  10. def OAI.ParityWL.Complexity.listCNF line 78
  11. lemma OAI.ParityWL.Complexity.mem_listCNF line 81
  12. lemma OAI.ParityWL.Complexity.listCNF_holds line 84
  13. def OAI.ParityWL.Complexity.compactCNF line 91
  14. lemma OAI.ParityWL.Complexity.listCNF_compact line 94
  15. lemma OAI.ParityWL.Complexity.compactCNF_length line 97
  16. def OAI.ParityWL.Complexity.PolyProgram.clauseEqual line 102
  17. def OAI.ParityWL.Complexity.PolyProgram.compactCNF line 113
  18. def OAI.ParityWL.Complexity.minimizeList line 117
  19. lemma OAI.ParityWL.Complexity.listCNF_minimize line 121
  20. def OAI.ParityWL.Complexity.pruneList line 139
  21. lemma OAI.ParityWL.Complexity.listCNF_prune line 142