OAI/Combinatorics/MatchingCount/Tapes/RandomWord.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingFPRAS.RandomWord.machine line 10
2. abbrev OAI.MatchingFPRAS.RandomWord.cfg line 19
3. def OAI.MatchingFPRAS.RandomWord.execute line 21
4. lemma OAI.MatchingFPRAS.RandomWord.execute_append line 23
5. lemma OAI.MatchingFPRAS.RandomWord.execute_cons line 25
6. lemma OAI.MatchingFPRAS.RandomWord.execute_halted line 27
7. lemma OAI.MatchingFPRAS.RandomWord.draw_two line 32
8. def OAI.MatchingFPRAS.RandomWord.pairCoins line 35
9. def OAI.MatchingFPRAS.RandomWord.drawnWord line 36
10. lemma OAI.MatchingFPRAS.RandomWord.draw_forward line 37
11. lemma OAI.MatchingFPRAS.RandomWord.reset_tick line 48
12. lemma OAI.MatchingFPRAS.RandomWord.reset_run line 52
13. lemma OAI.MatchingFPRAS.RandomWord.finish_run line 75
14. theorem OAI.MatchingFPRAS.RandomWord.execute_word line 99