OAI/Combinatorics/EditApproximation/Queries/QueryListWork.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

First-occurrence duplicate removal for the literal adaptive query lists. The equality tests, accumulated list, and final reversal are charged.

  1. theorem OAI.EditApproximation.queryEraseLoopWithWork_value line 16
  2. theorem OAI.EditApproximation.queryEraseWithWork_value line 30
  3. theorem OAI.EditApproximation.queryEraseLoopWithWork_nodup line 35
  4. theorem OAI.EditApproximation.queryEraseWithWork_nodup line 51
  5. theorem OAI.EditApproximation.queryEraseLoopWithWork_cost line 56
  6. theorem OAI.EditApproximation.queryEraseWithWork_cost line 80
  7. theorem OAI.EditApproximation.queryIntervalEqualWithWork_value line 88
  8. theorem OAI.EditApproximation.queryIntervalEqualWithWork_cost line 102