OAI/Combinatorics/EditApproximation/Queries/QueryPhysicalInitial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete physical initial branch. It reads terminal symbols through the original array and uses a length descriptor for the nonterminal initial-cone computation. Seed reads remain adaptive ranked requests.

  1. theorem OAI.EditApproximation.queryPhysicalInitial_refines line 24