OAI/Combinatorics/MatchingCount/Machines/TreeCanonical.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.contains line 11
  2. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_contains line 20
  3. def OAI.MatchingFPRAS.TreeTyped.dedupStep line 25
  4. def OAI.MatchingFPRAS.TreeTyped.dedupStepRealizer line 26
  5. lemma OAI.MatchingFPRAS.TreeTyped.dedup_fold line 30
  6. def OAI.MatchingFPRAS.TreeTyped.dedup line 37
  7. lemma OAI.MatchingFPRAS.TreeTyped.weight_dedupFold line 39
  8. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_dedup line 53
  9. def OAI.MatchingFPRAS.TreeTyped.insertStep line 66
  10. def OAI.MatchingFPRAS.TreeTyped.insertStepRealizer line 68
  11. lemma OAI.MatchingFPRAS.TreeTyped.insert_fold line 74
  12. def OAI.MatchingFPRAS.TreeTyped.orderedInsert line 82
  13. lemma OAI.MatchingFPRAS.TreeTyped.weight_perm line 91
  14. lemma OAI.MatchingFPRAS.TreeTyped.weight_orderedInsert line 93
  15. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_insertStep line 96
  16. lemma OAI.MatchingFPRAS.TreeTyped.insert_fold_bound line 106
  17. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_orderedInsert line 133
  18. def OAI.MatchingFPRAS.TreeTyped.insertionSort line 155
  19. lemma OAI.MatchingFPRAS.TreeTyped.weight_insertFold line 162
  20. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_insertionSort line 172
  21. def OAI.MatchingFPRAS.TreeTyped.canonical line 185
  22. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_canonical line 188
  23. lemma OAI.MatchingFPRAS.TreeTyped.canonical_eq_sort line 193