OAI/Combinatorics/MatchingCount/Sampling/TreeDPCounts.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.filterWith line 8
  2. abbrev OAI.MatchingFPRAS.ExecutableDP.Bag line 19
  3. abbrev OAI.MatchingFPRAS.ExecutableDP.Bags line 20
  4. abbrev OAI.MatchingFPRAS.ExecutableDP.Parents line 21
  5. def OAI.MatchingFPRAS.ExecutableDP.privateFlag line 23
  6. def OAI.MatchingFPRAS.ExecutableDP.sharedFlag line 24
  7. def OAI.MatchingFPRAS.ExecutableDP.totalFlag line 25
  8. def OAI.MatchingFPRAS.ExecutableDP.privateNumber line 26
  9. def OAI.MatchingFPRAS.ExecutableDP.sharedNumber line 27
  10. def OAI.MatchingFPRAS.ExecutableDP.totalNumber line 28
  11. def OAI.MatchingFPRAS.ExecutableDP.trim line 29
  12. def OAI.MatchingFPRAS.ExecutableDP.totalFlagRealizer line 31
  13. def OAI.MatchingFPRAS.ExecutableDP.privateFlagRealizer line 32
  14. def OAI.MatchingFPRAS.ExecutableDP.sharedFlagRealizer line 34
  15. def OAI.MatchingFPRAS.ExecutableDP.privateNumberRealizer line 37
  16. def OAI.MatchingFPRAS.ExecutableDP.sharedNumberRealizer line 39
  17. def OAI.MatchingFPRAS.ExecutableDP.totalNumberRealizer line 41
  18. def OAI.MatchingFPRAS.ExecutableDP.trimRealizer line 43
  19. def OAI.MatchingFPRAS.ExecutableDP.context line 46
  20. def OAI.MatchingFPRAS.ExecutableDP.contextRealizer line 50
  21. def OAI.MatchingFPRAS.ExecutableDP.bagRep line 59
  22. def OAI.MatchingFPRAS.ExecutableDP.activeRep line 61
  23. lemma OAI.MatchingFPRAS.ExecutableDP.mem_bagRep line 63
  24. lemma OAI.MatchingFPRAS.ExecutableDP.length_bagRep line 65
  25. lemma OAI.MatchingFPRAS.ExecutableDP.card_one_mem line 67
  26. lemma OAI.MatchingFPRAS.ExecutableDP.privateFlag_bagRep line 74
  27. lemma OAI.MatchingFPRAS.ExecutableDP.sharedFlag_bagRep line 78
  28. lemma OAI.MatchingFPRAS.ExecutableDP.totalFlag_bagRep line 82
  29. lemma OAI.MatchingFPRAS.ExecutableDP.filter_length_toList line 86
  30. lemma OAI.MatchingFPRAS.ExecutableDP.privateNumber_activeRep line 92
  31. lemma OAI.MatchingFPRAS.ExecutableDP.sharedNumber_activeRep line 96
  32. lemma OAI.MatchingFPRAS.ExecutableDP.totalNumber_activeRep line 100
  33. lemma OAI.MatchingFPRAS.ExecutableDP.trim_activeRep line 106