OAI/Combinatorics/MatchingCount/Machines/TreeRefreshCatalog.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.ExecutableRefresh.sharedKey line 10
2. def OAI.MatchingFPRAS.ExecutableRefresh.sharedKeyRealizer line 12
3. lemma OAI.MatchingFPRAS.ExecutableRefresh.polynomial_sharedKey line 16
4. def OAI.MatchingFPRAS.ExecutableRefresh.storedCatalog line 24
5. def OAI.MatchingFPRAS.ExecutableRefresh.storedCatalogRealizer line 26
6. lemma OAI.MatchingFPRAS.ExecutableRefresh.polynomial_storedCatalog line 29
7. lemma OAI.MatchingFPRAS.ExecutableRefresh.key_le line 51
8. lemma OAI.MatchingFPRAS.ExecutableRefresh.row_mem line 69
9. lemma OAI.MatchingFPRAS.ExecutableRefresh.sym_mk_inf_sup line 73
10. lemma OAI.MatchingFPRAS.ExecutableRefresh.sym_inf_mem line 75
11. lemma OAI.MatchingFPRAS.ExecutableRefresh.sym_sup_mem line 78
12. lemma OAI.MatchingFPRAS.ExecutableRefresh.storedCatalog_mem line 81
13. lemma OAI.MatchingFPRAS.ExecutableRefresh.storedCatalog_eq line 132