fact: Fixpoint size_of_pbh'_productions {valid n pats} (p : generic_pbh'_productions G transform_valid valid n pats) : nat := match p with | PBHNil _ => 0 | PBHCons _ _ _ p0 p1 => S (size_of_pbh'_production p0 + size_of_pbh'_productions p1) end with size_of_pbh'_production {valid0 valid n pat} (p : generic_pbh'_production G transform_valid valid0 valid n pat) : nat := match p with | PBHProductionNil _ => 0 | PBHProductionConsNonTerminal0 _ _ _ _ p0 p1 => S (size_of_pbh'_productions p0 + size_of_pbh'_production p1) | PBHProductionConsNonTerminalS _ _ _ _ _ p1 => S (size_of_pbh'_production p1) | PBHProductionConsTerminal _ _ _ _ _ _ _ p' => S (size_of_pbh'_production p') end.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Reachable.ParenBalancedHiding.Core Fiat.Parsers.BaseTypes