OAI/Combinatorics/EditApproximation/Queries/QueryPhysicalReaders.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual ranked physical reads for the charged local program. Table addresses are constructed before lookup, mass reads execute their mean, and the total history reader executes its natural-word guard.

  1. theorem OAI.EditApproximation.queryPhysicalTableRead_refines line 18
  2. theorem OAI.EditApproximation.queryPhysicalTableRead_work line 25
  3. theorem OAI.EditApproximation.queryPhysicalWarmupRead_refines line 38
  4. theorem OAI.EditApproximation.queryPhysicalMassRead_refines line 49
  5. theorem OAI.EditApproximation.queryPhysicalCurrentRead_refines line 60
  6. theorem OAI.EditApproximation.queryPhysicalEarlierRead_refines line 70