OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryTemporarySpace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedQueryTemporaryCells line 16

   Source documentation

   Cumulative concrete local allocations, address workspace, suspended reads, dictionary paths and evaluator frames, over the actual cache trace.

   def computedQueryTemporaryCells (source target : List ℕ) (N : ℕ)
       (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
       (input : ComputedFamilyInput source target N) : ℕ :=
   …

   Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.ComputedFamilyInput

2. theorem OAI.EditApproximation.computedQueryTemporaryCells_bound line 27
3. theorem OAI.EditApproximation.requestCells_factor line 64
4. theorem OAI.EditApproximation.computedQueryTemporaryCells_polynomial line 72