OAI/Combinatorics/LowSpaceSubsetSum/Streams/CountedTieGroup.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.CountedTieGroup.potential line 15
2. def OAI.LowSpaceSubsetSum.CountedTieGroup.step line 18
3. theorem OAI.LowSpaceSubsetSum.CountedTieGroup.step_value line 26
4. theorem OAI.LowSpaceSubsetSum.CountedTieGroup.step_work_potential line 35
5. def OAI.LowSpaceSubsetSum.CountedTieGroup.run line 50
6. theorem OAI.LowSpaceSubsetSum.CountedTieGroup.run_value line 64
7. theorem OAI.LowSpaceSubsetSum.CountedTieGroup.run_work line 80

   Source documentation

   The group cost follows its exact query, report and copy ledger. In particular, suffix fuel is not multiplied by the number of outer records.

   theorem run_work
       (read₁ : σ₁ → Option (α × σ₁) × ℕ) (key₁ : α → ℤ × ℕ)
       (read₂ : σ₂ → Option (β × σ₂) × ℕ) (key₂ : β → ℤ × ℕ) (cells : β → ℕ) (K : ℤ)
       (report : α → β → τ → (τ × Bool) × ℕ) (clone : σ₂ → σ₂ × ℕ)
       (R₁ R₂ L₁ L₂ S C D : ℕ)
       (hr₁ : ∀ s, (read₁ s).2 ≤ R₁) (hr₂ : ∀ s, (read₂ s).2 ≤ R₂)
       (hk₁ : ∀ x, (key₁ x).2 ≤ L₁) (hk₂ : ∀ y, (key₂ y).2 ≤ L₂)
       (hs : ∀ y, cells y ≤ S) (hc : ∀ x y a, (report x y a).2 ≤ C)
       (hcopy : ∀ s, (clone s).2 ≤ D)
       (B fuel₁ fuel₂ : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ) :
       (run read₁ key₁ read₂ key₂ cells K report clone B fuel₁ fuel₂ s₁ s₂ a).2 ≤
         (R₁ + R₂ + L₁ + L₂ + S + 50) *
   …

   Mentions: OAI.LowSpaceSubsetSum.CountedTieGroup.run