OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredPrefixController.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Prefix control executing bounded-list restriction updates

The collector receives the actual stored one/zero lists. Finite restrictions appear only in the semantic refinement. The full traversal remains an accounting object, while execution stops after the first accepting child.

  1. def OAI.LowSpaceSubsetSum.StoredPrefixController.header line 17
  2. def OAI.LowSpaceSubsetSum.StoredPrefixController.run line 19
  3. def OAI.LowSpaceSubsetSum.StoredPrefixController.fullCost line 38
  4. theorem OAI.LowSpaceSubsetSum.StoredPrefixController.run_work line 50
  5. theorem OAI.LowSpaceSubsetSum.StoredPrefixController.run_value line 67
  6. theorem OAI.LowSpaceSubsetSum.StoredPrefixController.fullCost_le_ledger line 91