OAI/Combinatorics/EditApproximation/Queries/QueryCodeBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Key encoding uses only a fixed number of natural-word operations. Its word sizes and Boolean work are polynomial in the coordinate widths.

  1. theorem OAI.EditApproximation.queryNaturalAdd_size line 10
  2. theorem OAI.EditApproximation.queryNaturalMul_size line 18
  3. theorem OAI.EditApproximation.queryNaturalAdd_cost line 26
  4. theorem OAI.EditApproximation.queryNaturalMul_cost line 31
  5. theorem OAI.EditApproximation.queryChildCodeWithWork_bounds line 37
  6. theorem OAI.EditApproximation.queryChildOrderWithWork_cost line 84
  7. theorem OAI.EditApproximation.queryOrderedChildInputsWithWork_cost line 93