OAI/Combinatorics/EditApproximation/Binary/BitControlSpace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Invocation counts for literal Boolean routines. An active call stack is a subset of these invocations. Each frame has a fixed number of bit/word/pointer fields, so these bounds complement (rather than replace) fresh-array storage.

  1. def OAI.EditApproximation.bitAddInvocations line 11
  2. theorem OAI.EditApproximation.bitAddInvocations_le_work line 17
  3. def OAI.EditApproximation.bitSubtractInvocations line 39
  4. theorem OAI.EditApproximation.bitSubtractInvocations_le_work line 45
  5. def OAI.EditApproximation.bitCompareInvocations line 67
  6. theorem OAI.EditApproximation.bitCompareInvocations_le_work line 69
  7. def OAI.EditApproximation.bitMulInvocations line 73
  8. theorem OAI.EditApproximation.bitMulInvocations_le_work line 79
  9. def OAI.EditApproximation.trimBitWordInvocations line 87
  10. theorem OAI.EditApproximation.trimBitWordInvocations_le_work line 89
  11. def OAI.EditApproximation.bitDivModInvocations line 95
  12. theorem OAI.EditApproximation.bitDivModInvocations_le_work line 103
  13. def OAI.EditApproximation.bitPowerInvocations line 113
  14. theorem OAI.EditApproximation.bitPowerInvocations_le_work line 120