OAI/Combinatorics/EditApproximation/Queries/QueryIndexedSlice.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A terminal source interval is accessed through its stored endpoint. Its substring is used only in the specification, never materialized.

  1. theorem OAI.EditApproximation.querySliceHeadWithWork_value line 15
  2. theorem OAI.EditApproximation.querySliceHeadWithWork_cost line 25
  3. theorem OAI.EditApproximation.queryIndexedSliceWithWork_value line 36
  4. theorem OAI.EditApproximation.queryIndexedSliceWithWork_cost line 50