proposition: Lemma terminals_disjoint_search_for_not (str : @String Ascii.ascii HSLM) {nt its} (H_disjoint : disjoint ascii_beq (possible_terminals_of nt) (possible_first_terminals_of_production its)) {n} (pit : parse_of_item G (StringLike.take n str) (NonTerminal nt)) (pits : parse_of_production G (StringLike.drop n str) its) (H_reachable : production_is_reachable G (NonTerminal nt :: its)) : is_first_char_such_that (might_be_empty_of_production its) str n (fun ch => negb (list_bin ascii_beq ch (possible_terminals_of nt))).
proof: Proof. pose proof (terminals_disjoint_search_for_not' _ H_disjoint pit pits H_reachable) as H. split; [ destruct H as [H0 H1] | destruct H as [H0 [[H1 H2] | H1]]; solve [ left; eauto | right; eauto ] ]. revert H0. apply forall_chars__char_in__impl__forall_chars. intros ch H' H''. apply Bool.negb_true_iff, Bool.not_true_iff_false in H''. apply H''. apply list_in_lb; [ apply (@ascii_lb) | ]; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Init.Wf Coq.Arith.Wf_nat Coq.ZArith.ZArith Coq.Lists.List Coq.Strings.String Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Equality Coq.Program.Equality Coq.MSets.MSetPositive Fiat.Common Fiat.Common.Equality Fiat.Common.Wf Fiat.Common.Enumerable Fiat.Common.LogicFacts Fiat.Parsers.Splitters.RDPList Fiat.Parsers.Splitters.BruteForce Fiat.Parsers.ParserInterface Fiat.Parsers.BaseTypes Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BooleanRecognizerFull Fiat.Parsers.BooleanRecognizerCorrect Fiat.Common.List.Operations Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.ForallChars Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.StringLike.FirstCharSuchThat Fiat.Parsers.StringLike.LastChar Fiat.Parsers.StringLike.LastCharSuchThat Fiat.Parsers.StringLike.Properties Fiat.Parsers.MinimalParseOfParse Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.Fold Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidProperties Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.Refinement.DisjointLemmasEarlyDeclarations Fiat.Parsers.Refinement.PossibleTerminalsSets Fiat.Common.BoolFacts