OAI/Combinatorics/MatchingCount/Arithmetic/BinaryCompare.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.StackCompare.updateOrder line 9
  2. def OAI.MatchingFPRAS.StackCompare.compareDigits line 12
  3. def OAI.MatchingFPRAS.StackCompare.result line 20
  4. lemma OAI.MatchingFPRAS.StackCompare.result_digits line 21
  5. lemma OAI.MatchingFPRAS.StackCompare.compareDigits_result line 36
  6. lemma OAI.MatchingFPRAS.StackCompare.compares_values line 53
  7. def OAI.MatchingFPRAS.StackCompare.flags line 60
  8. def OAI.MatchingFPRAS.StackCompare.program line 61
  9. def OAI.MatchingFPRAS.StackCompare.cfg line 67
  10. lemma OAI.MatchingFPRAS.StackCompare.step_empty line 69
  11. lemma OAI.MatchingFPRAS.StackCompare.step_digits line 74
  12. lemma OAI.MatchingFPRAS.StackCompare.compareDigits_step line 80
  13. theorem OAI.MatchingFPRAS.StackCompare.run_comparison line 84
  14. lemma OAI.MatchingFPRAS.StackCompare.accesses_bound line 110
  15. lemma OAI.MatchingFPRAS.StackCompare.finite_support line 112
  16. lemma OAI.MatchingFPRAS.StackCompare.numerical_comparison line 114