OAI/Combinatorics/MatchingCount/Graphs/Output.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.ZeroOutput.program line 9
2. abbrev OAI.MatchingFPRAS.ZeroOutput.cfg line 20
3. lemma OAI.MatchingFPRAS.ZeroOutput.zero_blank line 22
4. lemma OAI.MatchingFPRAS.ZeroOutput.start line 25
5. lemma OAI.MatchingFPRAS.ZeroOutput.erase_step line 28
6. lemma OAI.MatchingFPRAS.ZeroOutput.erase_run line 32
7. lemma OAI.MatchingFPRAS.ZeroOutput.switch line 42
8. lemma OAI.MatchingFPRAS.ZeroOutput.return_step line 45
9. lemma OAI.MatchingFPRAS.ZeroOutput.return_run line 49
10. lemma OAI.MatchingFPRAS.ZeroOutput.return_finish line 56
11. theorem OAI.MatchingFPRAS.ZeroOutput.run_zero line 63
12. lemma OAI.MatchingFPRAS.ZeroOutput.cost_bound line 72
13. theorem OAI.MatchingFPRAS.ZeroOutput.post_zero line 77
14. lemma OAI.MatchingFPRAS.ZeroOutput.encodeNat_nonblank line 89
15. lemma OAI.MatchingFPRAS.ZeroOutput.encodeInt_nonblank line 97
16. lemma OAI.MatchingFPRAS.ZeroOutput.encodeRat_nonblank line 102
17. lemma OAI.MatchingFPRAS.ZeroOutput.encodeInput_nonblank line 107
18. theorem OAI.MatchingFPRAS.ZeroOutput.post_zero_input line 121