JoinOne.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Reporting one item's matches against a buffered tie group

The immutable prefix buffer is reused. A generator suffix is restored only when the group was longer than the buffer. The callback may stop in either part; its work and stream queries are bounded on every outcome.

def OAI.LowSpaceSubsetSum.JoinOne.run line 20
theorem OAI.LowSpaceSubsetSum.JoinOne.reports_le line 32
theorem OAI.LowSpaceSubsetSum.JoinOne.queries_le line 47
theorem OAI.LowSpaceSubsetSum.JoinOne.halted_false line 65

theorem OAI.LowSpaceSubsetSum.JoinOne.state_complete line 78

Source documentation

Completed reporting is precisely prefix reporting followed by suffix reporting; a short group has no suffix to restore.

theorem state_complete (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (report : α → τ → τ × Bool) (hreport : ∀ x a, (report x a).2 = false)
    (view : σ → List α) (hread : RowMerge.IsReader read view)
    (buffer : Array α) (hkeys : ∀ x ∈ buffer.toList, key x = K)
    (saved : σ) (fuel : ℕ) (a : τ)
    (hfuel : (TieBuffer.groupView key K view saved).length ≤ fuel) :
    (run read key K report buffer saved (TieBuffer.hasKey read key K saved) fuel a).state =
      (buffer.toList ++ TieBuffer.groupView key K view saved).foldl
        (fun a x => (report x a).1) a := by
…

Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieBuffer.groupView, OAI.LowSpaceSubsetSum.JoinOne.run, OAI.LowSpaceSubsetSum.TieBuffer.hasKey

theorem OAI.LowSpaceSubsetSum.JoinOne.suffix_empty line 102
theorem OAI.LowSpaceSubsetSum.JoinOne.view_complete line 121
def OAI.LowSpaceSubsetSum.JoinOne.runFilled line 141
theorem OAI.LowSpaceSubsetSum.JoinOne.filled_reports_le line 147
theorem OAI.LowSpaceSubsetSum.JoinOne.filled_queries_le line 162
theorem OAI.LowSpaceSubsetSum.JoinOne.filled_state_complete line 177
theorem OAI.LowSpaceSubsetSum.JoinOne.filled_view_complete line 196