OAI/Combinatorics/EditApproximation/Queries/QueryActionInputs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Once the selected group and online actions have been computed, the last adaptive gather lists exactly their child coordinates, sorted by the same injective encoding as the reference query.

  1. theorem OAI.EditApproximation.query_mem_action_cover line 14
  2. theorem OAI.EditApproximation.queryActionInputsWithWork_value line 28
  3. theorem OAI.EditApproximation.queryNeededInputsWithWork_value line 43