OAI/Combinatorics/MatchingCount/Machines/TreeRefreshIndexed.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableRefresh.Key line 11
  2. def OAI.MatchingFPRAS.ExecutableRefresh.ordered line 13
  3. def OAI.MatchingFPRAS.ExecutableRefresh.orderedRealizer line 14
  4. lemma OAI.MatchingFPRAS.ExecutableRefresh.polynomial_ordered line 15
  5. lemma OAI.MatchingFPRAS.ExecutableRefresh.ordered_eq line 17
  6. def OAI.MatchingFPRAS.ExecutableRefresh.rowKey line 22
  7. def OAI.MatchingFPRAS.ExecutableRefresh.rowKeyRealizer line 24
  8. lemma OAI.MatchingFPRAS.ExecutableRefresh.polynomial_rowKey line 27
  9. def OAI.MatchingFPRAS.ExecutableRefresh.entryIndex line 33
  10. def OAI.MatchingFPRAS.ExecutableRefresh.entryIndexRealizer line 34
  11. lemma OAI.MatchingFPRAS.ExecutableRefresh.polynomial_entryIndex line 37
  12. def OAI.MatchingFPRAS.ExecutableRefresh.matching line 44
  13. def OAI.MatchingFPRAS.ExecutableRefresh.matchingRealizer line 46
  14. lemma OAI.MatchingFPRAS.ExecutableRefresh.polynomial_matching line 49
  15. def OAI.MatchingFPRAS.ExecutableRefresh.key line 64
  16. def OAI.MatchingFPRAS.ExecutableRefresh.catalog line 65
  17. lemma OAI.MatchingFPRAS.ExecutableRefresh.key_injective line 67
  18. lemma OAI.MatchingFPRAS.ExecutableRefresh.catalog_index line 78
  19. lemma OAI.MatchingFPRAS.ExecutableRefresh.rowKey_result line 89
  20. lemma OAI.MatchingFPRAS.ExecutableRefresh.matching_result line 94
  21. abbrev OAI.MatchingFPRAS.ExecutableRefresh.Input line 112
  22. def OAI.MatchingFPRAS.ExecutableRefresh.refresh line 113
  23. def OAI.MatchingFPRAS.ExecutableRefresh.refreshRealizer line 114
  24. lemma OAI.MatchingFPRAS.ExecutableRefresh.polynomial_refresh line 116
  25. lemma OAI.MatchingFPRAS.ExecutableRefresh.refresh_source line 124