OAI/Combinatorics/MatchingCount/Arithmetic/TreeNumberOps.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeBits.decodeForward line 11
  2. lemma OAI.MatchingFPRAS.TreeBits.decodeForward_exec line 12
  3. def OAI.MatchingFPRAS.TreeBits.encodeForward line 21
  4. lemma OAI.MatchingFPRAS.TreeBits.encodeForward_exec line 23
  5. def OAI.MatchingFPRAS.BinaryArithmeticProc.add line 42
  6. lemma OAI.MatchingFPRAS.BinaryArithmeticProc.add_exec line 43
  7. def OAI.MatchingFPRAS.BinaryArithmeticProc.compare line 49
  8. lemma OAI.MatchingFPRAS.BinaryArithmeticProc.compare_exec line 50
  9. def OAI.MatchingFPRAS.TreeArithmetic.decode line 64
  10. def OAI.MatchingFPRAS.TreeArithmetic.encode line 65
  11. def OAI.MatchingFPRAS.TreeArithmetic.normalize line 66
  12. def OAI.MatchingFPRAS.TreeArithmetic.add line 67
  13. def OAI.MatchingFPRAS.TreeArithmetic.rawPair line 72
  14. lemma OAI.MatchingFPRAS.TreeArithmetic.rawPair_scratch line 74
  15. lemma OAI.MatchingFPRAS.TreeArithmetic.rawPair_left line 76
  16. lemma OAI.MatchingFPRAS.TreeArithmetic.rawPair_right line 78
  17. lemma OAI.MatchingFPRAS.TreeArithmetic.rawPair_encode line 80
  18. lemma OAI.MatchingFPRAS.TreeArithmetic.rawPair_same line 86
  19. lemma OAI.MatchingFPRAS.TreeArithmetic.put3_raw_left line 92
  20. lemma OAI.MatchingFPRAS.TreeArithmetic.put3_raw_right line 98
  21. lemma OAI.MatchingFPRAS.TreeArithmetic.on_left line 104
  22. lemma OAI.MatchingFPRAS.TreeArithmetic.on_right line 111
  23. lemma OAI.MatchingFPRAS.TreeArithmetic.on_pair line 118
  24. theorem OAI.MatchingFPRAS.TreeArithmetic.add_exec line 131