OAI/Combinatorics/MatchingCount/Tapes/PackedInverse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.LiteralPacked.symbol_encode_injective line 11
2. lemma OAI.MatchingFPRAS.LiteralPacked.symbolBits_injective line 19
3. lemma OAI.MatchingFPRAS.LiteralPacked.encoding_injective line 23
4. lemma OAI.MatchingFPRAS.LiteralPacked.block_injective line 29
5. lemma OAI.MatchingFPRAS.LiteralPacked.flatMap_injective_fixed line 30
6. lemma OAI.MatchingFPRAS.LiteralPacked.width_pos line 47
7. lemma OAI.MatchingFPRAS.LiteralPacked.letter_injective line 48
8. lemma OAI.MatchingFPRAS.LiteralPacked.chunk_injective line 52
9. lemma OAI.MatchingFPRAS.LiteralPacked.encoding_blank line 61
10. lemma OAI.MatchingFPRAS.LiteralPacked.block_blank line 68
11. lemma OAI.MatchingFPRAS.LiteralPacked.block_ne_zero line 69
12. lemma OAI.MatchingFPRAS.LiteralPacked.chunk_nonzero line 72
13. def OAI.MatchingFPRAS.LiteralPacked.chunkFn line 87
14. lemma OAI.MatchingFPRAS.LiteralPacked.chunkFn_word line 89
15. def OAI.MatchingFPRAS.LiteralPacked.unchunk line 93
16. lemma OAI.MatchingFPRAS.LiteralPacked.unchunk_chunkFn line 95
17. lemma OAI.MatchingFPRAS.LiteralPacked.chunkFn_nonzero line 97