OAI/Combinatorics/EditApproximation/Probability/FiniteQueryRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Restriction of adaptive read programs to a proved finite request domain. The restriction visits the same reads whenever the original execution stays in that domain. It does not enumerate the domain.

  1. theorem OAI.EditApproximation.FiniteQuery.mapKeys_id line 15
  2. theorem OAI.EditApproximation.FiniteQuery.mapKeys_value line 25
  3. theorem OAI.EditApproximation.FiniteQuery.mapKeys_cost line 31
  4. theorem OAI.EditApproximation.FiniteQuery.mapKeys_keys line 38
  5. theorem OAI.EditApproximation.FiniteQuery.restrict_value line 46
  6. theorem OAI.EditApproximation.FiniteQuery.restrict_cost line 59
  7. theorem OAI.EditApproximation.FiniteQuery.restrict_keys line 74