OAI/Combinatorics/LowSpaceSubsetSum/Streams/StreamJoinCorrectness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.StreamJoin.semanticAccount line 14
2. theorem OAI.LowSpaceSubsetSum.StreamJoin.step_semantics line 18
3. theorem OAI.LowSpaceSubsetSum.StreamJoin.runAcc_semantics line 101
4. def OAI.LowSpaceSubsetSum.StreamJoin.DoneEmpty line 118
5. theorem OAI.LowSpaceSubsetSum.StreamJoin.step_doneEmpty line 121
6. theorem OAI.LowSpaceSubsetSum.StreamJoin.runAcc_doneEmpty line 157
7. theorem OAI.LowSpaceSubsetSum.StreamJoin.run_complete line 172

   Source documentation

   Enough control fuel gives the exact Cartesian-match fold. Occurrences with identical fields are still processed separately in this equation.

   theorem run_complete (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
       (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ)
       (report : α → β → τ → τ × Bool) (hreport : ∀ x y a, (report x y a).2 = false)
       (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
       (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
       (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ)
       (hsort₁ : (view₁ s₁).Pairwise (fun x y => key₁ x ≤ key₁ y))
       (hsort₂ : (view₂ s₂).Pairwise (fun x y => key₂ x ≤ key₂ y))
       (hcap₁ : (view₁ s₁).length ≤ fuel₁) (hcap₂ : (view₂ s₂).length ≤ fuel₂)
       (hfuel : (view₁ s₁).length + (view₂ s₂).length < controlFuel) :
       (run read₁ key₁ read₂ key₂ report B fuel₁ fuel₂ controlFuel s₁ s₂ a).user =
         MatchFold.run key₁ key₂ report (view₁ s₁) (view₂ s₂) a := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.StreamJoin.run, OAI.LowSpaceSubsetSum.MatchFold.run