OAI/Combinatorics/MatchingCount/Tapes/PackedExecution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.LiteralPacked.packCode line 9
2. def OAI.MatchingFPRAS.LiteralPacked.singletonBlock line 10
3. lemma OAI.MatchingFPRAS.LiteralPacked.singletonBlock_word line 11
4. lemma OAI.MatchingFPRAS.LiteralPacked.pack_exec line 12
5. def OAI.MatchingFPRAS.LiteralPacked.unpackCode line 28
6. lemma OAI.MatchingFPRAS.LiteralPacked.unpack_exec line 29
7. def OAI.MatchingFPRAS.LiteralTape.eraseRight line 54
8. lemma OAI.MatchingFPRAS.LiteralTape.eraseRight_step line 56
9. def OAI.MatchingFPRAS.LiteralTape.eraseCode line 65
10. lemma OAI.MatchingFPRAS.LiteralTape.erase_exec line 66