OAI/Combinatorics/ParityLifts/CodeErasure.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.PolyProgram.congr_code line 7
  2. lemma OAI.ParityWL.Complexity.PolyProgram.comp_code line 14
  3. lemma OAI.ParityWL.Complexity.PolyProgram.pair_code line 18
  4. lemma OAI.ParityWL.Complexity.PolyProgram.ite_code line 22
  5. lemma OAI.ParityWL.Complexity.PolyProgram.map_code_eq line 27
  6. lemma OAI.ParityWL.Complexity.PolyProgram.mapWith_code_eq line 35
  7. lemma OAI.ParityWL.Complexity.PolyProgram.any_code_eq line 44
  8. lemma OAI.ParityWL.Complexity.PolyProgram.all_code_eq line 51
  9. lemma OAI.ParityWL.Complexity.PolyProgram.filter_code_eq line 61
  10. lemma OAI.ParityWL.Complexity.FCode.cond_congr line 69
  11. lemma OAI.ParityWL.Complexity.PolyProgram.filterWith_code_eq line 85
  12. lemma OAI.ParityWL.Complexity.PolyProgram.dedupBy_code_eq line 100
  13. lemma OAI.ParityWL.Complexity.PolyProgram.mem_code_eq line 122
  14. lemma OAI.ParityWL.Complexity.PolyProgram.subset_code_eq line 128
  15. lemma OAI.ParityWL.Complexity.PolyProgram.reverse_code_eq line 137
  16. lemma OAI.ParityWL.Complexity.PolyProgram.append_code_eq line 143
  17. lemma OAI.ParityWL.Complexity.PolyProgram.flatten_code_eq line 150
  18. lemma OAI.ParityWL.Complexity.PolyProgram.length_code_eq line 157
  19. lemma OAI.ParityWL.Complexity.PolyProgram.clauseEqual_code_eq line 163
  20. lemma OAI.ParityWL.Complexity.PolyProgram.compactCNF_code_eq line 173
  21. lemma OAI.ParityWL.Complexity.PolyProgram.clauseSubset_code_eq line 178
  22. lemma OAI.ParityWL.Complexity.PolyProgram.minimalClause_code_eq line 194
  23. lemma OAI.ParityWL.Complexity.PolyProgram.minimizeList_code_eq line 207
  24. lemma OAI.ParityWL.Complexity.PolyProgram.keepClause_code_eq line 218
  25. lemma OAI.ParityWL.Complexity.PolyProgram.pruneList_code_eq line 224
  26. lemma OAI.ParityWL.Complexity.PolyProgram.prependAll_code_eq line 237
  27. lemma OAI.ParityWL.Complexity.PolyProgram.allTuples_code_eq line 242
  28. lemma OAI.ParityWL.Complexity.PolyProgram.clauseDiff_code_eq line 257
  29. lemma OAI.ParityWL.Complexity.PolyProgram.clauseDisjoint_code_eq line 265
  30. lemma OAI.ParityWL.Complexity.PolyProgram.allWith_code_eq line 271
  31. lemma OAI.ParityWL.Complexity.PolyProgram.card_code_eq line 278
  32. lemma OAI.ParityWL.Complexity.PolyProgram.cnfCard_code_eq line 287
  33. lemma OAI.ParityWL.Complexity.PolyProgram.cardEq_code_eq line 293
  34. lemma OAI.ParityWL.Complexity.PolyProgram.petalsApart_code_eq line 316
  35. lemma OAI.ParityWL.Complexity.PolyProgram.clauseMember_code_eq line 331
  36. lemma OAI.ParityWL.Complexity.PolyProgram.flowerCover_code_eq line 338
  37. lemma OAI.ParityWL.Complexity.PolyProgram.goodFlower_code_eq line 351
  38. lemma OAI.ParityWL.Complexity.PolyProgram.flowerCandidates_code_eq line 367
  39. lemma OAI.ParityWL.Complexity.PolyProgram.flowerList_code_eq line 385
  40. lemma OAI.ParityWL.Complexity.PolyProgram.sparseBranch_code line 398
  41. lemma OAI.ParityWL.Complexity.PolyProgram.sparseBranch_code_eq line 405
  42. lemma OAI.ParityWL.Complexity.PolyProgram.sparseStep_code_eq line 410