fact: Fixpoint size_of_reachable_from_productions {pats} (p : reachable_from_productions G ch valid pats) : nat := match p with | ReachableHead _ _ p' => S (size_of_reachable_from_production p') | ReachableTail _ _ p' => S (size_of_reachable_from_productions p') end with size_of_reachable_from_production {pat} (p : reachable_from_production G ch valid pat) : nat := match p with | ReachableProductionHead _ _ _ p' => S (size_of_reachable_from_item' (@size_of_reachable_from_productions) p') | ReachableProductionTail _ _ p' => S (size_of_reachable_from_production p') end.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.Reachable.OnlyLast.Reachable Fiat.Parsers.BaseTypes