OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedTieGroupCompletion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LowSpaceSubsetSum.BudgetedTieGroup.allowance line 12

    Source documentation

    Proof-only allowance for the operations performed by this tie group.

    def allowance (frontCharge fillCharge outerCharge charge copyCharge : ℕ)
    (read₁ : σ₁ → Option (α × σ₁) × ℕ) (key₁ : α → ℤ × ℕ)
    (read₂ : σ₂ → Option (β × σ₂) × ℕ) (key₂ : β → ℤ × ℕ)
    (cells : β → ℕ) (K : ℤ) (report : α → β → τ → (τ × Bool) × ℕ)
    (clone : σ₂ → σ₂ × ℕ) (B fuel₁ fuel₂ : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ) : ℕ :=
…
  2. theorem OAI.LowSpaceSubsetSum.BudgetedTieGroup.execute_complete line 26
  3. theorem OAI.LowSpaceSubsetSum.BudgetedTieGroup.execute_spent line 80
  4. theorem OAI.LowSpaceSubsetSum.BudgetedTieGroup.execute_remaining line 145
  5. theorem OAI.LowSpaceSubsetSum.BudgetedTieGroup.allowance_le line 204

    Source documentation

    The prepaid allowance is linear in the exact group's query/copy ledger.

    theorem allowance_le (frontCharge fillCharge outerCharge charge copyCharge : ℕ)
    (read₁ : σ₁ → Option (α × σ₁) × ℕ) (key₁ : α → ℤ × ℕ)
    (read₂ : σ₂ → Option (β × σ₂) × ℕ) (key₂ : β → ℤ × ℕ)
    (cells : β → ℕ) (K : ℤ) (report : α → β → τ → (τ × Bool) × ℕ)
    (clone : σ₂ → σ₂ × ℕ) (B fuel₁ fuel₂ : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ) :
    let out := (CountedTieGroup.run read₁ key₁ read₂ key₂ cells K report clone B fuel₁ fuel₂ s₁ s₂ a).1
…

    Mentions: OAI.LowSpaceSubsetSum.CountedTieGroup.run