OAI/Computability/LoopMatching/BitAdd.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.BitAdd.value line 9
  2. def OAI.LoopMatching.BitAdd.xor line 13
  3. def OAI.LoopMatching.BitAdd.digit line 14
  4. def OAI.LoopMatching.BitAdd.carry line 15
  5. lemma OAI.LoopMatching.BitAdd.fullAdder line 17
  6. lemma OAI.LoopMatching.BitAdd.value_append line 21
  7. lemma OAI.LoopMatching.BitAdd.value_head_tail line 27
  8. abbrev OAI.LoopMatching.BitAdd.State line 31
  9. def OAI.LoopMatching.BitAdd.step line 33
  10. def OAI.LoopMatching.BitAdd.initial line 38
  11. def OAI.LoopMatching.BitAdd.finish line 39
  12. def OAI.LoopMatching.BitAdd.run line 41
  13. def OAI.LoopMatching.BitAdd.add line 43
  14. def OAI.LoopMatching.BitAdd.potential line 46
  15. lemma OAI.LoopMatching.BitAdd.potential_step line 49
  16. lemma OAI.LoopMatching.BitAdd.potential_run line 65
  17. lemma OAI.LoopMatching.BitAdd.run_inputs line 72
  18. lemma OAI.LoopMatching.BitAdd.run_length line 82
  19. lemma OAI.LoopMatching.BitAdd.value_finish line 91
  20. theorem OAI.LoopMatching.BitAdd.value_add line 96
  21. theorem OAI.LoopMatching.BitAdd.length_add line 104
  22. lemma OAI.LoopMatching.BitAdd.value_bits line 111
  23. theorem OAI.LoopMatching.BitAdd.value_add_bits line 118