proposition: Lemma pre_Fix_grammar_fixedpoint_correct (P : default_nonterminal_carrierT -> state gdata -> Type) (Pbot : forall nt, is_true (is_valid_nonterminal initial_nonterminals_data nt) -> P nt ⊥) (Ptop : forall nt, is_valid_nonterminal initial_nonterminals_data nt = false -> P nt ⊤) (IH : forall nt st v, st nt = v -> is_true (is_valid_nonterminal initial_nonterminals_data nt) -> P nt v -> P nt (v ⊔ step_constraints gdata st nt v)) : forall nt, P nt (lookup_state (pre_Fix_grammar gdata initial_nonterminals_data) nt).
proof: Proof. intro nt. destruct (is_valid_nonterminal (@initial_nonterminals_data _ (@rdp_list_predata _ G)) nt) eqn:Hvalid. { apply pre_Fix_grammar_fixedpoint_correct_valid; eauto with nocore. } { simpl rewrite lookup_state_invalid_pre_Fix_grammar; [ | assumption ]. eauto with nocore. } Qed.
imports: Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common