OAI/Combinatorics/MatchingCount/Tapes/CoinStack.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.CoinStack.safe line 12
2. def OAI.MatchingFPRAS.CoinStack.coins line 16
3. lemma OAI.MatchingFPRAS.CoinStack.go_path line 21
4. lemma OAI.MatchingFPRAS.CoinStack.return_path line 34
5. theorem OAI.MatchingFPRAS.CoinStack.statement_path line 52
6. lemma OAI.MatchingFPRAS.CoinStack.one_step_path line 113
7. lemma OAI.MatchingFPRAS.CoinStack.coins_none line 132