OAI/Combinatorics/MatchingCount/Tapes/TreeBits.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeData.bits line 8
  2. lemma OAI.MatchingFPRAS.TreeData.bits_nil line 9
  3. lemma OAI.MatchingFPRAS.TreeData.bits_cons line 10
  4. lemma OAI.MatchingFPRAS.TreeData.bits_length line 11
  5. def OAI.MatchingFPRAS.TreeBits.decodeProgram line 21
  6. lemma OAI.MatchingFPRAS.TreeBits.decode_nil line 27
  7. lemma OAI.MatchingFPRAS.TreeBits.decode_cons line 30
  8. lemma OAI.MatchingFPRAS.TreeBits.run_decode line 34
  9. def OAI.MatchingFPRAS.TreeBits.decodeRaw line 42
  10. lemma OAI.MatchingFPRAS.TreeBits.decodeRaw_exec line 43
  11. def OAI.MatchingFPRAS.TreeBits.encodeProgram line 47
  12. lemma OAI.MatchingFPRAS.TreeBits.encode_nil line 52
  13. lemma OAI.MatchingFPRAS.TreeBits.encode_cons line 55
  14. def OAI.MatchingFPRAS.TreeBits.prepend line 59
  15. lemma OAI.MatchingFPRAS.TreeBits.prepend_append line 60
  16. lemma OAI.MatchingFPRAS.TreeBits.run_encode line 62
  17. lemma OAI.MatchingFPRAS.TreeBits.prepend_bits line 70
  18. def OAI.MatchingFPRAS.TreeBits.encodeRaw line 72
  19. lemma OAI.MatchingFPRAS.TreeBits.encodeRaw_exec line 73