OAI/Combinatorics/MatchingCount/Tapes/BlockMap.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.LiteralTape.scan_left line 11
2. lemma OAI.MatchingFPRAS.LiteralTape.scan_right line 25
3. inductive OAI.MatchingFPRAS.LiteralBlockMap.Label line 44
4. instance OAI.MatchingFPRAS.LiteralBlockMap.(instance at line 47) line 47
5. abbrev OAI.MatchingFPRAS.LiteralBlockMap.Block line 48
6. def OAI.MatchingFPRAS.LiteralBlockMap.code line 49
7. lemma OAI.MatchingFPRAS.LiteralBlockMap.seek_path line 72
8. lemma OAI.MatchingFPRAS.LiteralBlockMap.back_path line 75
9. lemma OAI.MatchingFPRAS.LiteralBlockMap.stopSep_path line 78
10. lemma OAI.MatchingFPRAS.LiteralBlockMap.stopOut_path line 81
11. def OAI.MatchingFPRAS.LiteralBlockMap.working line 85
12. lemma OAI.MatchingFPRAS.LiteralBlockMap.start_step line 87
13. lemma OAI.MatchingFPRAS.LiteralBlockMap.seek_write line 93
14. lemma OAI.MatchingFPRAS.LiteralBlockMap.stopOut_write line 103
15. lemma OAI.MatchingFPRAS.LiteralBlockMap.read_block line 112
16. lemma OAI.MatchingFPRAS.LiteralBlockMap.cycle line 137
17. lemma OAI.MatchingFPRAS.LiteralBlockMap.mk₂_blanks line 175
18. lemma OAI.MatchingFPRAS.LiteralBlockMap.mk₂_replicate line 178
19. lemma OAI.MatchingFPRAS.LiteralBlockMap.mk₂_zero_left line 181
20. lemma OAI.MatchingFPRAS.LiteralBlockMap.finish line 185
21. def OAI.MatchingFPRAS.LiteralBlockMap.budget line 225
22. lemma OAI.MatchingFPRAS.LiteralBlockMap.blocks line 226
23. lemma OAI.MatchingFPRAS.LiteralBlockMap.computes line 252