OAI/Combinatorics/MatchingCount/Arithmetic/BinarySubtract.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.StackSubtract.borrow line 9
  2. lemma OAI.MatchingFPRAS.StackSubtract.digit_balance line 10
  3. def OAI.MatchingFPRAS.StackSubtract.subDigits line 14
  4. lemma OAI.MatchingFPRAS.StackSubtract.subDigits_length line 22
  5. lemma OAI.MatchingFPRAS.StackSubtract.subDigits_balance line 34
  6. lemma OAI.MatchingFPRAS.StackSubtract.value_lt line 63
  7. lemma OAI.MatchingFPRAS.StackSubtract.subDigits_correct line 71
  8. def OAI.MatchingFPRAS.StackSubtract.program line 80
  9. def OAI.MatchingFPRAS.StackSubtract.cfg line 86
  10. lemma OAI.MatchingFPRAS.StackSubtract.step_empty line 88
  11. lemma OAI.MatchingFPRAS.StackSubtract.step_digits line 91
  12. lemma OAI.MatchingFPRAS.StackSubtract.subDigits_step line 97
  13. theorem OAI.MatchingFPRAS.StackSubtract.run_subtraction line 102