OAI/Combinatorics/MatchingCount/Machines/CoinTM1.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingFPRAS.CoinTM1.Node line 12
2. abbrev OAI.MatchingFPRAS.CoinTM1.State line 13
3. abbrev OAI.MatchingFPRAS.CoinTM1.Coins line 14
4. def OAI.MatchingFPRAS.CoinTM1.aux line 16
5. def OAI.MatchingFPRAS.CoinTM1.table line 24
6. def OAI.MatchingFPRAS.CoinTM1.pending line 30
7. def OAI.MatchingFPRAS.CoinTM1.trCfg line 33
8. lemma OAI.MatchingFPRAS.CoinTM1.execute_first_eq line 36
9. theorem OAI.MatchingFPRAS.CoinTM1.statement_ticks line 43
10. lemma OAI.MatchingFPRAS.CoinTM1.entry_ticks line 82
11. lemma OAI.MatchingFPRAS.CoinTM1.coin_tick line 93