OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedStreamPotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.BudgetedStreamStep.allowance_potential line 11

   Source documentation

   All nested prepaid charges are covered by the actual query and copy ledger.

   theorem allowance_potential (base front fill outer inner copy : ℕ)
       (read₁ : σ₁ → Option (α × σ₁) × ℕ) (key₁ : α → ℤ × ℕ)
       (read₂ : σ₂ → Option (β × σ₂) × ℕ) (key₂ : β → ℤ × ℕ)
       (cells : β → ℕ) (report : α → β → τ → (τ × Bool) × ℕ)
       (clone : σ₂ → σ₂ × ℕ) (B fuel₁ fuel₂ : ℕ) (st : StreamJoin.State σ₁ σ₂ τ) :
       let M := base + front + fill + outer + 2 * inner + 12
   …

   Mentions: OAI.LowSpaceSubsetSum.StreamJoin.State