OAI/Combinatorics/EditApproximation/Binary/BinaryFractionWork.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Unreduced fractions stored as Boolean words. Every numerator operation below runs the literal signed ripple/shift-add code; denominator products run the literal Boolean multiplication routine.

  1. theorem OAI.EditApproximation.BinaryFraction.representation_value line 22
  2. theorem OAI.EditApproximation.BinaryFraction.denominatorInteger_value line 28
  3. theorem OAI.EditApproximation.BinaryFraction.addWithWork_value line 35
  4. theorem OAI.EditApproximation.BinaryFraction.mulWithWork_value line 44
  5. theorem OAI.EditApproximation.BinaryFraction.addWithWork_representation line 50
  6. theorem OAI.EditApproximation.BinaryFraction.mulWithWork_representation line 57
  7. theorem OAI.EditApproximation.BinaryFraction.addWithWork_cost line 63
  8. theorem OAI.EditApproximation.BinaryFraction.mulWithWork_cost line 89
  9. theorem OAI.EditApproximation.BinaryFraction.neg_value line 109
  10. theorem OAI.EditApproximation.BinaryFraction.invWithWork_value line 112
  11. theorem OAI.EditApproximation.BinaryFraction.invWithWork_cost line 125
  12. theorem OAI.EditApproximation.BinaryFraction.zero_representation line 134
  13. theorem OAI.EditApproximation.BinaryFraction.neg_representation line 137
  14. theorem OAI.EditApproximation.BinaryFraction.invWithWork_representation line 143
  15. theorem OAI.EditApproximation.BinaryFraction.ltWithWork_representation line 166
  16. theorem OAI.EditApproximation.BinaryFraction.ltWithWork_value line 179
  17. theorem OAI.EditApproximation.BinaryFraction.ltWithWork_cost line 184