OAI/Combinatorics/EditApproximation/Queries/QueryDependencyExpansion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The dependency tree here is obtained from the requests made by the finite adaptive program at its actual answers. Local depth/index progress therefore bounds execution, rather than an independently supplied tree.

  1. def OAI.EditApproximation.queryRequestList line 20
  2. def OAI.EditApproximation.querySameRequests line 24
  3. def OAI.EditApproximation.queryEarlierRequests line 27
  4. theorem OAI.EditApproximation.queryRequestList_cost line 30
  5. theorem OAI.EditApproximation.sum_map_partition line 38
  6. theorem OAI.EditApproximation.querySameRequests_progress line 54
  7. theorem OAI.EditApproximation.queryEarlierRequests_progress line 65
  8. def OAI.EditApproximation.queryDependencyExpansion line 77
  9. theorem OAI.EditApproximation.queryDependencyExpansion_depth line 86
  10. theorem OAI.EditApproximation.queryDependencyExpansion_index line 90
  11. theorem OAI.EditApproximation.queryDependencyExpansion_valid line 94
  12. theorem OAI.EditApproximation.queryDependencyExpansion_nodes line 100
  13. theorem OAI.EditApproximation.rankedMemoEvaluate_dependency_bound line 162