OAI/Combinatorics/LowSpaceSubsetSum/Streams/MergeCorrectness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Complete and stopped tournament merges

The multiset view counts every row occurrence, even when all item fields coincide. Each successful advance removes exactly the reported occurrence. A sufficiently long trace therefore enumerates the whole product stream; the potential also bounds every stopped execution's number of advances.

  1. def OAI.LowSpaceSubsetSum.RowMerge.bag line 23
  2. theorem OAI.LowSpaceSubsetSum.RowMerge.bag_card line 26
  3. theorem OAI.LowSpaceSubsetSum.RowMerge.replacement_bag line 29
  4. theorem OAI.LowSpaceSubsetSum.RowMerge.bag_eq_zero_of_winner_none line 57
  5. def OAI.LowSpaceSubsetSum.RowMerge.trace line 71

    Source documentation

    Analysis view of repeated advances. The program can stop between them.

    def trace (key : α → ℤ) (read : σ → Option (α × σ)) :
    ℕ → Tournament.Tree (Front d α σ) d → List α
  | 0, _ => []
  | k + 1, t => match advance key read t with
    | none => []
    | some (a, t') => a :: trace key read k t'

    Mentions: OAI.LowSpaceSubsetSum.Tournament.Tree, OAI.LowSpaceSubsetSum.RowMerge.Front, OAI.LowSpaceSubsetSum.RowMerge.advance

  6. theorem OAI.LowSpaceSubsetSum.RowMerge.trace_complete line 78
  7. theorem OAI.LowSpaceSubsetSum.RowMerge.trace_length_le line 107