OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedPrefixAllowance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.BudgetedPrefixController.allowance line 10

   Source documentation

   Full-tree analysis allowance; the executable never evaluates it.

   def allowance (collect : StoredRestriction n → StoredEntry.Dictionary I C)
       (collectBill : StoredRestriction n → ℕ) (checkBill : Array (StoredEntry n) → ℕ) :
       List (Fin n) → StoredRestriction n → ℕ
     | order, P =>
       StoredPrefixController.header n + collectBill P +
       if (collect P).val.keys.overflow then
         match order with
         | [] => 0
         | i :: rest => allowance collect collectBill checkBill rest (P.force i false).1 +
             allowance collect collectBill checkBill rest (P.force i true).1
       else checkBill (collect P).val.records

   Mentions: OAI.collect, OAI.LowSpaceSubsetSum.StoredRestriction, OAI.LowSpaceSubsetSum.StoredEntry.Dictionary, OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.StoredPrefixController.header

2. theorem OAI.LowSpaceSubsetSum.BudgetedPrefixController.run_remaining line 22