OAI/Combinatorics/EditApproximation/Queries/QueryFamilyScalarReads.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Counted pass/copy indexing for the independent scalar family. Both remainders and the complete family address are computed before lookup.

  1. theorem OAI.EditApproximation.queryFinOfNatWithWork_value line 14
  2. theorem OAI.EditApproximation.queryFinOfNatWithWork_cost line 19
  3. theorem OAI.EditApproximation.queryFamilyTagWithWork_value line 32
  4. theorem OAI.EditApproximation.queryFamilyGroupRead_refines line 40
  5. theorem OAI.EditApproximation.queryFamilyOnlineRead_refines line 51