OAI/Combinatorics/MatchingCount/Arithmetic/BinaryAddition.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.StackAddition.Stacks line 9
  2. abbrev OAI.MatchingFPRAS.StackAddition.Store line 10
  3. def OAI.MatchingFPRAS.StackAddition.value line 11
  4. def OAI.MatchingFPRAS.StackAddition.digit line 14
  5. def OAI.MatchingFPRAS.StackAddition.carry line 15
  6. lemma OAI.MatchingFPRAS.StackAddition.digit_identity line 16
  7. def OAI.MatchingFPRAS.StackAddition.addDigits line 20
  8. lemma OAI.MatchingFPRAS.StackAddition.addDigits_value line 28
  9. lemma OAI.MatchingFPRAS.StackAddition.addDigits_length line 58
  10. def OAI.MatchingFPRAS.StackAddition.program line 82
  11. def OAI.MatchingFPRAS.StackAddition.stackData line 89
  12. lemma OAI.MatchingFPRAS.StackAddition.stackData_zero line 90
  13. lemma OAI.MatchingFPRAS.StackAddition.stackData_one line 91
  14. lemma OAI.MatchingFPRAS.StackAddition.stackData_two line 92
  15. def OAI.MatchingFPRAS.StackAddition.cfg line 93
  16. lemma OAI.MatchingFPRAS.StackAddition.update_zero line 95
  17. lemma OAI.MatchingFPRAS.StackAddition.update_one line 99
  18. lemma OAI.MatchingFPRAS.StackAddition.update_two line 103
  19. lemma OAI.MatchingFPRAS.StackAddition.step_empty line 107
  20. lemma OAI.MatchingFPRAS.StackAddition.step_digits line 112
  21. lemma OAI.MatchingFPRAS.StackAddition.addDigits_step line 119
  22. theorem OAI.MatchingFPRAS.StackAddition.run_addition line 124
  23. lemma OAI.MatchingFPRAS.StackAddition.accesses_bound line 151
  24. lemma OAI.MatchingFPRAS.StackAddition.finite_support line 153
  25. lemma OAI.MatchingFPRAS.StackAddition.value_bits line 155
  26. lemma OAI.MatchingFPRAS.StackAddition.addition_numerals line 164