OAI/Combinatorics/MatchingCount/Arithmetic/BinaryCopy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MatchingFPRAS.BinaryArithmetic.CopyPhase line 9
  2. def OAI.MatchingFPRAS.BinaryArithmetic.bitSymbol line 13
  3. def OAI.MatchingFPRAS.BinaryArithmetic.markSymbol line 14
  4. def OAI.MatchingFPRAS.BinaryArithmetic.unmarkSymbol line 15
  5. lemma OAI.MatchingFPRAS.BinaryArithmetic.bitSymbol_ne_zero line 16
  6. lemma OAI.MatchingFPRAS.BinaryArithmetic.markSymbol_ne_zero line 17
  7. lemma OAI.MatchingFPRAS.BinaryArithmetic.unmark_mark line 18
  8. lemma OAI.MatchingFPRAS.BinaryArithmetic.unmark_bit line 19
  9. lemma OAI.MatchingFPRAS.BinaryArithmetic.unmark_three line 20
  10. def OAI.MatchingFPRAS.BinaryArithmetic.copyProgram line 22
  11. abbrev OAI.MatchingFPRAS.BinaryArithmetic.copyCfg line 37
  12. lemma OAI.MatchingFPRAS.BinaryArithmetic.seek_marks line 39
  13. lemma OAI.MatchingFPRAS.BinaryArithmetic.seek_bit line 51
  14. lemma OAI.MatchingFPRAS.BinaryArithmetic.append_run line 55
  15. lemma OAI.MatchingFPRAS.BinaryArithmetic.rewind_run line 68
  16. lemma OAI.MatchingFPRAS.BinaryArithmetic.finish_run line 87
  17. lemma OAI.MatchingFPRAS.BinaryArithmetic.restore_run line 100
  18. def OAI.MatchingFPRAS.BinaryArithmetic.copyWord line 118
  19. lemma OAI.MatchingFPRAS.BinaryArithmetic.copy_cycle line 119
  20. lemma OAI.MatchingFPRAS.BinaryArithmetic.copy_finish line 163
  21. lemma OAI.MatchingFPRAS.BinaryArithmetic.copy_run line 200
  22. lemma OAI.MatchingFPRAS.BinaryArithmetic.copy_natural line 215
  23. lemma OAI.MatchingFPRAS.BinaryArithmetic.copyProgram_cost line 225
  24. theorem OAI.MatchingFPRAS.BinaryArithmetic.copy_post line 232