OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedBucketExecution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Executed separator families complete the representation history

  1. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.clog_le line 14

    Distinct definitions of this name: OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedHistoryExecution.lean:17 (same declaration text), OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedStructuralExecution.lean:43 (same statement text; different proof or body). Qualify references as OAI.LowSpaceSubsetSum.WordSeedMeasured.clog_le@path.

  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.separatorDraws line 17
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.bucketHistory line 24