OAI/Combinatorics/EditApproximation/Binary/BinarySubtractWork.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Ripple-borrow subtraction, used after the magnitude comparison in signed-integer addition. No unit-cost operation on unbounded integers is used by this Boolean routine.

  1. theorem OAI.EditApproximation.bitSubtractor_value line 17
  2. theorem OAI.EditApproximation.bitSubtractWithWork_length line 27

    Source documentation

    Ripple-borrow subtraction when the minuend has no remaining bits.

    theorem bitSubtractWithWork_length (left right : List Bool) (borrow : Bool) :
    (bitSubtractWithWork left right borrow).1.length = max left.length right.length := by
…

    Mentions: OAI.EditApproximation.bitSubtractWithWork

  3. theorem OAI.EditApproximation.bitSubtractionRippleEquation line 40
  4. theorem OAI.EditApproximation.bitSubtractWithWork_value line 47
  5. theorem OAI.EditApproximation.bitWordValue_lt_pow_length line 93
  6. theorem OAI.EditApproximation.bitSubtractWithWork_sub line 99
  7. theorem OAI.EditApproximation.bitSubtractWithWork_cost line 110
  8. theorem OAI.EditApproximation.binaryNaturalSubtractWithWork_value line 133
  9. theorem OAI.EditApproximation.binaryNaturalSubtractWithWork_cost line 138