OAI/Combinatorics/EditApproximation/Refinement/PhysicalBinaryStep.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Boolean refinement kernel at a physical node uses cached words for its child and table requests.

  1. def OAI.EditApproximation.physicalPreparedStepWithWork line 27
  2. theorem OAI.EditApproximation.physicalPreparedStepWithWork_bounds line 34
  3. theorem OAI.EditApproximation.physicalPreparedStepWithWork_value line 67
  4. theorem OAI.EditApproximation.physicalPreparedStep_input_ranges line 98
  5. def OAI.EditApproximation.physicalCachedStepWithWork line 112
  6. theorem OAI.EditApproximation.physicalCachedStepWithWork_cost line 120
  7. theorem OAI.EditApproximation.physicalCachedStepWithWork_value_width line 143