OAI/Combinatorics/EditApproximation/Geometry/IndexedTerminalWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.indexedLeafWithWork_value line 14

   Source documentation

   Empty and singleton terminal states use the already prepared occurrence index. Endpoints are read directly; no target substring is copied.

    theorem indexedLeafWithWork_value (table : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
       (symbol : Option ℕ) (lo hi : ℕ) :
       (indexedLeafWithWork table symbolBits positionBits symbol lo hi).1 =
         indexedLeafCost table symbolBits positionBits symbol lo hi := by
   …

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

2. theorem OAI.EditApproximation.indexedLeafWithWork_cost line 22
3. theorem OAI.EditApproximation.indexedLeafWithWork_exact line 30
4. theorem OAI.EditApproximation.integerIndexedLeafWithWork_cost line 40