OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSnapshotCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual mutable-reader cloning scratch

Only the tournament is copied. Both immutable arrays and bounded masks inside its records are shared. The trace retains the completed left subtree while copying the right subtree and includes the recursive stack.

  1. def OAI.LowSpaceSubsetSum.RepresentationSnapshotCells.copy line 16
  2. theorem OAI.LowSpaceSubsetSum.RepresentationSnapshotCells.copy_value line 24
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSnapshotCells.copy_cells line 30
  4. def OAI.LowSpaceSubsetSum.RepresentationSnapshotCells.snapshot line 44
  5. theorem OAI.LowSpaceSubsetSum.RepresentationSnapshotCells.snapshot_value line 52
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSnapshotCells.snapshot_cells line 57