OAI/Combinatorics/EditApproximation/Binary/BinaryArithmeticWork.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal Boolean ripple addition. The counter counts Boolean gates and bit writes, not unit-cost arithmetic on unbounded integers.

  1. theorem OAI.EditApproximation.bitAdder_value line 19
  2. theorem OAI.EditApproximation.bitAddWithWork_value line 28
  3. theorem OAI.EditApproximation.bitAddWithWork_cost line 53
  4. theorem OAI.EditApproximation.bitAddWithWork_length line 77
  5. theorem OAI.EditApproximation.bitWordValue_bits line 101
  6. theorem OAI.EditApproximation.binaryNaturalAddWithWork_value line 110
  7. theorem OAI.EditApproximation.binaryNaturalAddWithWork_cost line 114
  8. theorem OAI.EditApproximation.bitMulWithWork_value line 121
  9. theorem OAI.EditApproximation.bitMulWithWork_length line 128
  10. theorem OAI.EditApproximation.bitMulWithWork_cost line 141
  11. theorem OAI.EditApproximation.binaryNaturalMulWithWork_value line 157
  12. theorem OAI.EditApproximation.binaryNaturalMulWithWork_cost line 161