OAI/Combinatorics/EditApproximation/Queries/QueryHistoryCodeBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Word and comparison bounds for the actual finite history-key lists.

  1. theorem OAI.EditApproximation.queryPairWithWork_bounds line 10
  2. theorem OAI.EditApproximation.queryHistoryCodeWithWork_bounds line 47
  3. theorem OAI.EditApproximation.queryHistoryEqualWithWork_cost line 61
  4. theorem OAI.EditApproximation.queryHistoryOrderWithWork_cost line 70
  5. theorem OAI.EditApproximation.queryOrderedHistoryInputsWithWork_cost line 80