proposition: Lemma find_aggregate_state_max_exact k : PositiveMap.find k aggregate_state_max = if rdp_list_is_valid_nonterminal initial_nonterminals_data (positive_to_nonterminal k) then Some ⊥ else None.
proof: Proof. pose proof (find_aggregate_state_max_rdp_spec k) as H; unfold is_true in *; split_iff; break_match. { intuition eauto. } { edestruct PositiveMap.find; [ | reflexivity ]. specialize_all_ways; specialize_by (exact eq_refl). intuition congruence. } Qed.
imports: Coq.Init.Wf Coq.Numbers.BinNums Coq.Arith.Arith Coq.FSets.FMapPositive Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.Splitters.RDPList Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common.FMapExtensions.Wf Fiat.Common Fiat.Common.OptionFacts Fiat.Common.SetoidInstances