OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedJoinExecution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LowSpaceSubsetSum.BudgetedJoinExecution.step line 11
2. abbrev OAI.LowSpaceSubsetSum.BudgetedJoinExecution.run line 18
3. theorem OAI.LowSpaceSubsetSum.BudgetedJoinExecution.reference_eq line 26
4. theorem OAI.LowSpaceSubsetSum.BudgetedJoinExecution.run_value line 39
5. theorem OAI.LowSpaceSubsetSum.BudgetedJoinExecution.run_work line 58
6. theorem OAI.LowSpaceSubsetSum.BudgetedJoinExecution.run_complete line 85
7. theorem OAI.LowSpaceSubsetSum.BudgetedJoinExecution.run_complete_queries line 116

   Source documentation

   From fresh cursors, every control iteration performs at least one query.

   theorem run_complete_queries (base front fill outer inner copy : ℕ)
       (read₁ : σ₁ → Option (α × σ₁) × ℕ) (key₁ : α → ℤ × ℕ)
       (read₂ : σ₂ → Option (β × σ₂) × ℕ) (key₂ : β → ℤ × ℕ)
       (cells : β → ℕ) (report : α → β → τ → (τ × Bool) × ℕ)
       (clone : σ₂ → σ₂ × ℕ) (hclone : ∀ s, (clone s).1 = s)
       (B fuel₁ fuel₂ fuel : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ) (budget : ℕ)
       (hb : let out := (CountedStreamJoin.runAcc read₁ key₁ read₂ key₂ cells report clone B fuel₁ fuel₂ fuel
   …

   Mentions: OAI.LowSpaceSubsetSum.CountedStreamJoin.runAcc