fact: Fixpoint size_of_pb'_productions {valid pats} (p : generic_pb'_productions G transform_valid valid pats) : nat := match p with | PBNil _ => 0 | PBCons _ _ _ p0 p1 => S (size_of_pb'_production p0 + size_of_pb'_productions p1) end with size_of_pb'_production {valid n pat} (p : generic_pb'_production G transform_valid valid n pat) : nat := match p with | PBProductionNil _ => 0 | PBProductionConsNonTerminal _ _ _ _ _ p0 p1 => S (size_of_pb'_productions p0 + size_of_pb'_production p1) | PBProductionConsTerminal _ _ _ _ _ _ _ p' => S (size_of_pb'_production p') end.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.BaseTypes