OAI/Combinatorics/LowSpaceSubsetSum/Storage/ScalarJoinCells.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Tail-recursive scalar join lifetime

The stopped loop retains only its current two cursors and user state. No previously completed group remains reachable from its successor.

  1. def OAI.LowSpaceSubsetSum.ScalarJoinCells.run line 18
  2. theorem OAI.LowSpaceSubsetSum.ScalarJoinCells.run_value line 29
  3. theorem OAI.LowSpaceSubsetSum.ScalarJoinCells.run_cells line 52