OAI/Combinatorics/MatchingCount/Machines/TreeMarkTable.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableSource.MarkRowInput line 13
  2. def OAI.MatchingFPRAS.ExecutableSource.phantomPart line 14
  3. def OAI.MatchingFPRAS.ExecutableSource.phantomPartRealizer line 16
  4. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_phantomPart line 18
  5. def OAI.MatchingFPRAS.ExecutableSource.markPortions line 26
  6. def OAI.MatchingFPRAS.ExecutableSource.markPortionsRealizer line 28
  7. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_markPortions line 31
  8. lemma OAI.MatchingFPRAS.ExecutableSource.markPortions_source line 41
  9. def OAI.MatchingFPRAS.ExecutableSource.threeOptions line 62
  10. def OAI.MatchingFPRAS.ExecutableSource.threeOptionsRealizer line 64
  11. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_threeOptions line 68
  12. def OAI.MatchingFPRAS.ExecutableSource.sourceMarkRow line 75
  13. def OAI.MatchingFPRAS.ExecutableSource.sourceMarkRowRealizer line 77
  14. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sourceMarkRow line 80
  15. lemma OAI.MatchingFPRAS.ExecutableSource.sourceMarkRow_source line 89
  16. def OAI.MatchingFPRAS.ExecutableSource.sourceMarks line 102
  17. def OAI.MatchingFPRAS.ExecutableSource.sourceMarksRealizer line 104
  18. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sourceMarks line 106
  19. lemma OAI.MatchingFPRAS.ExecutableSource.sourceMarks_source line 109
  20. theorem OAI.MatchingFPRAS.ExecutableSource.sourceMarks_post line 124