OAI/Combinatorics/EditApproximation/Binary/BitQueryOn.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Simulation along a fixed reachable oracle. This allows a checked normalization at the end of a local query: its denominator invariant is required only for the values that the ranked execution actually reaches.

  1. inductive OAI.EditApproximation.BitQuery.RefinesOn line 11
  2. theorem OAI.EditApproximation.BitQuery.Refines.onOracle line 22
  3. theorem OAI.EditApproximation.BitQuery.RefinesOn.value_keys line 31
  4. theorem OAI.EditApproximation.BitQuery.RefinesOn.finish line 41