proposition: Lemma prod_lub_correct (lub0_correct : forall P1 st1, lattice_for_related prerelated0 P1 st1 -> forall P2 st2, lattice_for_related prerelated0 P2 st2 -> lattice_for_related prerelated0 (ensemble_least_upper_bound P1 P2) (st1 ⊔ st2)%fixedpoint) (lub1_correct : forall P1 st1, lattice_for_related prerelated1 P1 st1 -> forall P2 st2, lattice_for_related prerelated1 P2 st2 -> lattice_for_related prerelated1 (ensemble_least_upper_bound P1 P2) (st1 ⊔ st2)%fixedpoint) : 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_least_upper_bound P1 P2) (st1 ⊔ st2)%fixedpoint.
proof: Proof. pose proof (fun P1 H1 P2 st2 => lub0_correct P1 ⊥%fixedpoint H1 P2 (constant st2)). pose proof (fun P1 H1 P2 st2 => lub1_correct P1 ⊥%fixedpoint H1 P2 (constant st2)). pose proof (fun P1 st1 H1 P2 => lub0_correct P1 (constant st1) H1 P2 ⊥%fixedpoint). pose proof (fun P1 st1 H1 P2 => lub1_correct P1 (constant st1) H1 P2 ⊥%fixedpoint). 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