OAI/Combinatorics/EditApproximation/Geometry/ChargedDependencyExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The dependency expansion is built from the charged evaluator's executed requests. Its branching bounds therefore apply to actual lazy evaluation, with coarse leaves at their original physical depths.

  1. theorem OAI.EditApproximation.chargedRequest_index_le line 13
  2. theorem OAI.EditApproximation.chargedRequestList_progress line 45
  3. def OAI.EditApproximation.chargedDependencyTree line 59
  4. theorem OAI.EditApproximation.chargedDependencyTree_valid line 73
  5. theorem OAI.EditApproximation.chargedDependencyTree_widthWork_le line 100