proposition: Lemma prod_combine_production_nondep_correct (precombine_production0 : T0 -> T0 -> lattice_for T0) (precombine_production1 : T1 -> T1 -> lattice_for T1) (combine_production0_correct : forall P1 st1, lattice_for_related prerelated0 P1 st1 -> forall P2 st2, lattice_for_related prerelated0 P2 st2 -> lattice_for_related prerelated0 (ensemble_combine_production P1 P2) (lattice_for_combine_production precombine_production0 st1 st2)) (combine_production1_correct : forall P1 st1, lattice_for_related prerelated1 P1 st1 -> forall P2 st2, lattice_for_related prerelated1 P2 st2 -> lattice_for_related prerelated1 (ensemble_combine_production P1 P2) (lattice_for_combine_production precombine_production1 st1 st2)) : forall P1 st1, lattice_for_related prod_prerelated P1 st1 -> forall P2 st2, lattice_for_related prod_prerelated P2 st2 -> lattice_for_related prod_prerelated (ensemble_combine_production P1 P2) (lattice_for_combine_production (prod_precombine_production_nondep precombine_production0 precombine_production1) st1 st2).
proof: Proof. t. Qed.
imports: Coq.Sets.Ensembles Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Parsers.ContextFreeGrammar.Fix.Prod Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretationDefinitions Fiat.Common Fiat.Common.Instances Fiat.Common.BoolFacts