OAI/Combinatorics/MatchingCount/Machines/TreeStart.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableSource.evenTest line 12
  2. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_evenTest line 14
  3. def OAI.MatchingFPRAS.ExecutableSource.mateIndex line 19
  4. def OAI.MatchingFPRAS.ExecutableSource.mateIndexRealizer line 20
  5. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_mateIndex line 23
  6. lemma OAI.MatchingFPRAS.ExecutableSource.mateIndex_source line 28
  7. def OAI.MatchingFPRAS.ExecutableSource.startSelected line 33
  8. def OAI.MatchingFPRAS.ExecutableSource.startSelectedRealizer line 35
  9. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_startSelected line 40
  10. lemma OAI.MatchingFPRAS.ExecutableSource.startSelected_source line 47
  11. def OAI.MatchingFPRAS.ExecutableSource.exactStart line 57
  12. def OAI.MatchingFPRAS.ExecutableSource.exactStartRealizer line 60
  13. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_exactStart line 64
  14. lemma OAI.MatchingFPRAS.ExecutableSource.numbered_map_image line 74
  15. lemma OAI.MatchingFPRAS.ExecutableSource.startMatching_set line 80
  16. lemma OAI.MatchingFPRAS.ExecutableSource.exactStart_source line 86
  17. theorem OAI.MatchingFPRAS.ExecutableSource.exactStart_post line 114