proposition: Lemma fold_nt_step_correct0 (valid0 : nonterminals_listT) (Hlen : nonterminals_length valid0 <= 0) (Hsub : sub_nonterminals_listT valid0 initial_nonterminals_data) : forall nt nt_idx, of_nonterminal nt = nt_idx -> Pnt valid0 nt (fold_nt_step (compiled_productions G) 0 fold_nt valid0 nt nt_idx).
proof: Proof. assert (Hlen' : nonterminals_length valid0 = 0) by omega; clear Hlen. simpl; intros nt nt_idx Hnt. apply Pnt_redundant; [ assumption | ]. destruct (is_valid_nonterminal valid0 (of_nonterminal nt)) eqn:Hvalid; trivial. assert (nonterminals_length (remove_nonterminal valid0 (of_nonterminal nt)) < nonterminals_length valid0) by (apply remove_nonterminal_dec; assumption). omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.OptionFacts