OAI/Combinatorics/EditApproximation/Geometry/InitialSeedTable.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous initial accuracy on the actual labeled state domain

The source and target arguments are the stored substrings at each physical node and valid target interval. The entry-size and whole-domain cardinal premises of the coarse seed theorem are discharged here.

  1. theorem OAI.EditApproximation.initialSeedTable_width_bound line 18
  2. theorem OAI.EditApproximation.initialSeedTable_accuracy line 26