OAI/Combinatorics/EditApproximation/Queries/QueryScopedOrder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Sorting costs only require bounded comparisons between keys actually present in the input. This is needed for the natural-valued history time.

  1. theorem OAI.EditApproximation.memberByWithWork_cost_on line 10
  2. theorem OAI.EditApproximation.queryEraseLoopWithWork_cost_on line 24
  3. theorem OAI.EditApproximation.queryEraseWithWork_cost_on line 57
  4. theorem OAI.EditApproximation.queryInsertWithWork_cost_on line 65
  5. theorem OAI.EditApproximation.querySortWithWork_cost_on line 80
  6. theorem OAI.EditApproximation.queryOrderedInputsWithWork_cost_on line 103