OAI/Combinatorics/EditApproximation/Binary/BinaryCanonicalWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing only leading zero bits of an integer word. This is unrelated to rational reduction: no common divisor is computed.

  1. theorem OAI.EditApproximation.trimBitWordWithWork_value line 14
  2. theorem OAI.EditApproximation.trimBitWordWithWork_canonical line 25
  3. theorem OAI.EditApproximation.trimBitWordWithWork_length line 43
  4. theorem OAI.EditApproximation.trimBitWordWithWork_cost line 47