OAI/Combinatorics/EditApproximation/Binary/BitQueryNormalize.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Executed cache normalization charges the actual Boolean rescaling. Its exact-value premise is checked on the reachable local result.

  1. theorem OAI.EditApproximation.BitQuery.normalize_value line 15
  2. theorem OAI.EditApproximation.BitQuery.normalize_keys line 26
  3. theorem OAI.EditApproximation.BitQuery.normalize_work line 32
  4. theorem OAI.EditApproximation.BitQuery.RefinesOn.normalize line 40