OAI/Combinatorics/EditApproximation/Queries/QueryIndexedSpace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.indexedLeafAllocation_le_work line 14

   Source documentation

   The occurrence key, two prefix traversals and scalar result cells. The occurrence trie itself is borrowed from preprocessing.

   theorem indexedLeafAllocation_le_work (table : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
       (symbol : Option ℕ) (lo hi : ℕ) :
       indexedLeafAllocation symbolBits positionBits symbol lo hi ≤
         (indexedLeafWithWork table symbolBits positionBits symbol lo hi).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.indexedLeafAllocation, OAI.EditApproximation.indexedLeafWithWork

2. theorem OAI.EditApproximation.binaryIndexedLeafAllocation_le_work line 26
3. theorem OAI.EditApproximation.queryIndexedSliceAllocation_le_work line 34