OAI/Combinatorics/EditApproximation/Binary/SignedBinaryWork.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Signed integers represented by a sign bit and a Boolean magnitude word. Arithmetic uses Boolean ripple and shift-add routines.

  1. theorem OAI.EditApproximation.SignedBinary.value_ofInt line 28
  2. theorem OAI.EditApproximation.SignedBinary.value_neg line 35
  3. theorem OAI.EditApproximation.SignedBinary.subtract_signed_value line 39
  4. theorem OAI.EditApproximation.SignedBinary.addWithWork_value line 49
  5. theorem OAI.EditApproximation.SignedBinary.mulWithWork_value line 75
  6. theorem OAI.EditApproximation.SignedBinary.addWithWork_cost line 80
  7. theorem OAI.EditApproximation.SignedBinary.mulWithWork_cost line 93
  8. theorem OAI.EditApproximation.SignedBinary.addWithWork_length line 99
  9. theorem OAI.EditApproximation.SignedBinary.mulWithWork_length line 110