OAI/Computability/LoopMatching/BitAddRoutine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. lemma OAI.LoopMatching.BitAdd.boolList_code_length line 10
  2. lemma OAI.LoopMatching.BitAdd.state_code_length line 18
  3. theorem OAI.LoopMatching.BitAdd.xor_poly line 24
  4. theorem OAI.LoopMatching.BitAdd.digit_poly line 28
  5. theorem OAI.LoopMatching.BitAdd.carry_poly line 32
  6. theorem OAI.LoopMatching.BitAdd.step_poly line 36
  7. lemma OAI.LoopMatching.BitAdd.step_growth line 52
  8. theorem OAI.LoopMatching.BitAdd.run_poly line 60
  9. theorem OAI.LoopMatching.BitAdd.initial_poly line 63
  10. theorem OAI.LoopMatching.BitAdd.finish_poly line 67
  11. theorem OAI.LoopMatching.BitAdd.add_poly line 71