proposition: Lemma guarded_bij_disjointed_union: forall PV1 PE1 PV2 PE2 vmap emap (G: PreGraph V E) (G': PreGraph V' E'), disjointed_guard (image_set PV1 vmap) (image_set PV2 vmap) (image_set PE1 emap) (image_set PE2 emap) -> guarded_bij PV1 PE1 vmap emap G G' -> guarded_bij PV2 PE2 vmap emap G G' -> boundary_consistent PV1 PV2 PE1 PE2 vmap emap G G' -> guarded_bij (Union _ PV1 PV2) (Union _ PE1 PE2) vmap emap G G'.
proof: Proof. intros. destruct H as [vDISJ eDISJ]. split; intros. + pose proof image_Disjoint_rev _ _ _ vDISJ. apply Disjoint_Union_Prop_join in H. eapply is_guarded_inj_disjoint_union; eauto. - apply (vmap_inj H0); auto. - apply (vmap_inj H1); auto. - rewrite Disjoint_spec in vDISJ. intros v1 v2 ? ? ?. apply (vDISJ (vmap v1)). * constructor; auto. * rewrite H5; constructor; auto. + pose proof image_Disjoint_rev _ _ _ eDISJ. apply Disjoint_Union_Prop_join in H. eapply is_guarded_inj_disjoint_union; eauto. - apply (emap_inj H0); auto. - apply (emap_inj H1); auto. - rewrite Disjoint_spec in eDISJ. intros e1 e2 ? ? ?. apply (eDISJ (emap e1)). * constructor; auto. * rewrite H5; constructor; auto. + apply guarded_morphism_disjointed_union; auto; apply bij_is_morphism; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation