OAI/Combinatorics/LowSpaceSubsetSum/Search/StoppedStreamJoin.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LowSpaceSubsetSum.StreamJoin.StoppedResult line 12
2. def OAI.LowSpaceSubsetSum.StreamJoin.stoppedAcc line 18

   Source documentation

   Return immediately at exhaustion or callback halt. The fuel counter is only a bound; its unused suffix is never traversed.

   def stoppedAcc (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
       (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ)
       (report : α → β → τ → τ × Bool) (B fuel₁ fuel₂ : ℕ) :
       ℕ → State σ₁ σ₂ τ → StoppedResult σ₁ σ₂ τ
     | 0, st => ⟨st, 0⟩
     | fuel + 1, st =>
       if st.done then ⟨st, 0⟩ else
         let out := stoppedAcc read₁ key₁ read₂ key₂ report B fuel₁ fuel₂ fuel
   …

   Mentions: OAI.LowSpaceSubsetSum.StreamJoin.State, OAI.LowSpaceSubsetSum.StreamJoin.StoppedResult

3. def OAI.LowSpaceSubsetSum.StreamJoin.stopped line 29
4. theorem OAI.LowSpaceSubsetSum.StreamJoin.stoppedAcc_eq line 35
5. theorem OAI.LowSpaceSubsetSum.StreamJoin.stopped_eq line 49
6. theorem OAI.LowSpaceSubsetSum.StreamJoin.step_query_growth line 57
7. theorem OAI.LowSpaceSubsetSum.StreamJoin.stoppedAcc_steps_le line 72

   Source documentation

   Each actual control iteration performs a charged reader query.

   theorem stoppedAcc_steps_le (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
       (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ)
       (report : α → β → τ → τ × Bool) (B fuel₁ fuel₂ fuel : ℕ) (st : State σ₁ σ₂ τ) :
       st.queries + (stoppedAcc read₁ key₁ read₂ key₂ report B fuel₁ fuel₂ fuel st).steps ≤
         (stoppedAcc read₁ key₁ read₂ key₂ report B fuel₁ fuel₂ fuel st).state.queries := by
   …

   Mentions: OAI.LowSpaceSubsetSum.StreamJoin.State, OAI.LowSpaceSubsetSum.StreamJoin.stoppedAcc

8. theorem OAI.LowSpaceSubsetSum.StreamJoin.stopped_steps_le_queries line 88