OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedStreamAllowance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.BudgetedStreamStep.allowance line 11

   Source documentation

   Proof-only allowance for one comparison or one complete tie group.

   def allowance (base front fill outer inner copy : ℕ)
       (read₁ : σ₁ → Option (α × σ₁) × ℕ) (key₁ : α → ℤ × ℕ)
       (read₂ : σ₂ → Option (β × σ₂) × ℕ) (key₂ : β → ℤ × ℕ)
       (cells : β → ℕ) (report : α → β → τ → (τ × Bool) × ℕ)
       (clone : σ₂ → σ₂ × ℕ) (B fuel₁ fuel₂ : ℕ) (st : StreamJoin.State σ₁ σ₂ τ) : ℕ :=
   …

   Mentions: OAI.LowSpaceSubsetSum.StreamJoin.State

2. theorem OAI.LowSpaceSubsetSum.BudgetedStreamStep.execute_complete line 27