OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationTieOuterCells.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Live cells of the complete outer traversal of one tie group

The buffer and saved second reader form a shared callback context. Each outer iteration releases its old reader and user state before the tail call; inner buffer/suffix replay uses the concrete bounded-list callbacks.

  1. def OAI.LowSpaceSubsetSum.RepresentationTieOuterCells.run line 18
  2. theorem OAI.LowSpaceSubsetSum.RepresentationTieOuterCells.run_value line 32
  3. theorem OAI.LowSpaceSubsetSum.RepresentationTieOuterCells.outer_bound line 67
  4. theorem OAI.LowSpaceSubsetSum.RepresentationTieOuterCells.run_cells line 94