OAI/Combinatorics/EditApproximation/Binary/BinaryOrderWork.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Most-significant comparison performed directly on little-endian Boolean words, allowing leading zero bits.

  1. theorem OAI.EditApproximation.bitOrdering_matches line 16
  2. theorem OAI.EditApproximation.bitCompareWithWork_matches line 29
  3. theorem OAI.EditApproximation.bitCompareWithWork_lt line 48
  4. theorem OAI.EditApproximation.bitCompareWithWork_eq line 54
  5. theorem OAI.EditApproximation.bitCompareWithWork_cost line 60
  6. theorem OAI.EditApproximation.binaryNaturalCompareWithWork_lt line 83
  7. theorem OAI.EditApproximation.binaryNaturalCompareWithWork_eq line 87
  8. theorem OAI.EditApproximation.binaryNaturalCompareWithWork_cost line 91