OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationJoinLedger.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual parent-join counters through the full prefix tree

The full tree is only an accounting view. The executable search is depth first and may return YES earlier. Invalid matching tuples remain charged.

  1. def OAI.LowSpaceSubsetSum.CompressionLedger.add line 18
  2. def OAI.LowSpaceSubsetSum.RepresentationParentData.localLedger line 28
  3. def OAI.LowSpaceSubsetSum.RepresentationParentData.prefixLedger line 32
  4. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.prefixLedger_queries line 41
  5. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.prefixLedger_bounds line 49