OAI/Combinatorics/MatchingCount/Arithmetic/BinaryIncrement.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.BinaryArithmetic.incrementBits line 9
  2. lemma OAI.MatchingFPRAS.BinaryArithmetic.incrementBits_bits line 13
  3. def OAI.MatchingFPRAS.BinaryArithmetic.numeral line 28
  4. def OAI.MatchingFPRAS.BinaryArithmetic.incrementProgram line 30
  5. abbrev OAI.MatchingFPRAS.BinaryArithmetic.cfg line 37
  6. lemma OAI.MatchingFPRAS.BinaryArithmetic.back_step line 39
  7. lemma OAI.MatchingFPRAS.BinaryArithmetic.back_run line 44
  8. lemma OAI.MatchingFPRAS.BinaryArithmetic.carry_false line 63
  9. lemma OAI.MatchingFPRAS.BinaryArithmetic.carry_true line 67
  10. lemma OAI.MatchingFPRAS.BinaryArithmetic.carry_nil line 71
  11. lemma OAI.MatchingFPRAS.BinaryArithmetic.increment_run line 75
  12. theorem OAI.MatchingFPRAS.BinaryArithmetic.increment_natural line 100
  13. lemma OAI.MatchingFPRAS.BinaryArithmetic.incrementProgram_cost line 108
  14. theorem OAI.MatchingFPRAS.BinaryArithmetic.increment_post line 113