OAI/Combinatorics/EditApproximation/Queries/QueryHistoryInputs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The earlier-history cover is materialized from its small coordinate lists, then sorted by the original history encoding. It never enumerates the much larger Cartesian set of complete wide actions.

  1. theorem OAI.EditApproximation.BinaryFraction.queryRawHistoryInputsWithWork_value line 17
  2. theorem OAI.EditApproximation.BinaryFraction.queryRawHistoryInputsWithWork_cover line 27
  3. theorem OAI.EditApproximation.BinaryFraction.queryEarlierInputsWithWork_value line 40