OAI/Combinatorics/MatchingCount/Tapes/FixedAlphabetCompiler.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.FixedAlphabetCompiler.bitsWord line 17
2. def OAI.MatchingFPRAS.FixedAlphabetCompiler.word line 18
3. lemma OAI.MatchingFPRAS.FixedAlphabetCompiler.initial_block line 20
4. lemma OAI.MatchingFPRAS.FixedAlphabetCompiler.output_block line 28
5. def OAI.MatchingFPRAS.FixedAlphabetCompiler.support line 33
6. lemma OAI.MatchingFPRAS.FixedAlphabetCompiler.block_support line 36
7. def OAI.MatchingFPRAS.FixedAlphabetCompiler.compiled line 38
8. def OAI.MatchingFPRAS.FixedAlphabetCompiler.cost line 42
9. theorem OAI.MatchingFPRAS.FixedAlphabetCompiler.compiled_words line 47