OAI/Combinatorics/LowSpaceSubsetSum/Counting/CountedCeilLog.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Computing a bounded binary ceiling logarithm by doubling

The executable loop stores the current power of two. It performs no call to Nat.clog and never forms a power by repeated recomputation.

  1. def OAI.LowSpaceSubsetSum.CountedCeilLog.loop line 14
  2. theorem OAI.LowSpaceSubsetSum.CountedCeilLog.loop_value line 20
  3. theorem OAI.LowSpaceSubsetSum.CountedCeilLog.loop_work line 41
  4. def OAI.LowSpaceSubsetSum.CountedCeilLog.run line 52
  5. theorem OAI.LowSpaceSubsetSum.CountedCeilLog.run_value line 54
  6. theorem OAI.LowSpaceSubsetSum.CountedCeilLog.run_work line 59