BudgetedPrefixCompletion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LowSpaceSubsetSum.BudgetedPrefixController.run_complete line 11

Source documentation

Paying the full source-prefix ledger guarantees that early-YES execution finishes; the allowance does not have to be computed at runtime.

theorem run_complete
    (collect : StoredRestriction n → ℕ → Option (StoredEntry.Dictionary I C × ℕ) × ℕ)
    (pureCollect : StoredRestriction n → StoredEntry.Dictionary I C)
    (check : Array (StoredEntry n) → ℕ → Option (Bool × ℕ) × ℕ)
    (collectBill : StoredRestriction n → ℕ) (checkBill : Array (StoredEntry n) → ℕ)
    (hc : ∀ P b, collectBill P ≤ b → ∃ left, (collect P b).1 = some (pureCollect P, left))
    (hcr : ∀ P b d left, (collect P b).1 = some (d, left) → d = pureCollect P ∧ b ≤ left + collectBill P)
    (hk : ∀ a b, checkBill a ≤ b → ∃ v left, (check a b).1 = some (v, left))
    (hkr : ∀ a b v left, (check a b).1 = some (v, left) → b ≤ left + checkBill a)
    (order : List (Fin n)) (P : StoredRestriction n) (budget : ℕ)
    (hb : allowance pureCollect collectBill checkBill order P ≤ budget) :
    ∃ v left, (run collect check order P budget).1 = some (v, left) := by
…

Mentions: OAI.collect, OAI.LowSpaceSubsetSum.StoredRestriction, OAI.LowSpaceSubsetSum.StoredEntry.Dictionary, OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.BudgetedPrefixController.allowance, OAI.LowSpaceSubsetSum.BudgetedPrefixController.run