OAI/Combinatorics/MatchingCount/Tapes/Packed.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.LiteralPacked.Row line 11
  2. def OAI.MatchingFPRAS.LiteralPacked.baseRow line 12
  3. def OAI.MatchingFPRAS.LiteralPacked.bitRow line 15
  4. def OAI.MatchingFPRAS.LiteralPacked.bottom line 16
  5. def OAI.MatchingFPRAS.LiteralPacked.letter line 17
  6. lemma OAI.MatchingFPRAS.LiteralPacked.rows_eq line 18
  7. lemma OAI.MatchingFPRAS.LiteralPacked.word_eq line 40
  8. def OAI.MatchingFPRAS.LiteralPacked.symbolBits line 49
  9. lemma OAI.MatchingFPRAS.LiteralPacked.symbolBits_length line 50
  10. lemma OAI.MatchingFPRAS.LiteralPacked.list_bits line 54
  11. def OAI.MatchingFPRAS.LiteralPacked.block line 63
  12. def OAI.MatchingFPRAS.LiteralPacked.header line 65
  13. def OAI.MatchingFPRAS.LiteralPacked.chunk line 66
  14. def OAI.MatchingFPRAS.LiteralPacked.width line 67
  15. lemma OAI.MatchingFPRAS.LiteralPacked.map_enc_length line 68
  16. lemma OAI.MatchingFPRAS.LiteralPacked.block_length line 72
  17. lemma OAI.MatchingFPRAS.LiteralPacked.flatMap_uniform_length line 75
  18. lemma OAI.MatchingFPRAS.LiteralPacked.chunk_length line 80
  19. lemma OAI.MatchingFPRAS.LiteralPacked.packed_eq line 84
  20. lemma OAI.MatchingFPRAS.LiteralPacked.block_alphabet line 90
  21. lemma OAI.MatchingFPRAS.LiteralPacked.chunk_alphabet line 93