OAI/Combinatorics/EditApproximation/Queries/QueryBandGather.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The band-data stage constructs its keys by counted Boolean routines, then gathers mass and initial words in the reference order.

  1. theorem OAI.EditApproximation.queryBandGather_refines line 15
  2. theorem OAI.EditApproximation.queryBandGather_work line 47