OAI/Combinatorics/EditApproximation/Queries/QueryChargedFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

All physical table branches run Boolean arithmetic and issue address-charged adaptive requests. Coarse entries are supplied by the separately executed coarse initializer.

  1. def OAI.EditApproximation.queryChargedFamilyTable line 24
  2. theorem OAI.EditApproximation.queryChargedFamilyTable_refines line 56
  3. def OAI.EditApproximation.queryChargedFamilyGlobal line 106
  4. theorem OAI.EditApproximation.queryChargedFamilyGlobal_refines line 115