proposition: Lemma join_decomp (G1 G2 : sgraph) (D1 : T1 -> {set G1}) (D2 : T2 -> {set G2}) : sdecomp T1 G1 D1 -> sdecomp T2 G2 D2 -> sdecomp tjoin (sjoin G1 G2) (decompU D1 D2).
proof: Proof. Proof using. move => dec1 dec2. split. - move => [x|x]. + case: (sbag_cover dec1 x) => t Ht. exists (inl t) => /=. by rewrite imset_f. + case: (sbag_cover dec2 x) => t Ht. exists (inr t) => /=. by rewrite imset_f. - move => [x|x] [y|y] // xy. + case: (sbag_edge dec1 xy) => t /andP [H1 H2]. exists (inl t) => /=. by rewrite !imset_f. + case: (sbag_edge dec2 xy) => t /andP [H1 H2]. exists (inr t) => /=. by rewrite !imset_f. - have inl_inr x t : inl x \in decompU D1 D2 (inr t) = false. { rewrite /decompU /=. apply/negbTE/negP. by case/imsetP. } have inr_inl x t : inr x \in decompU D1 D2 (inl t) = false. { rewrite /decompU /=. apply/negbTE/negP. by case/imsetP. } move => [x|x] [t1|t1] [t2|t2] /= ; rewrite ?inl_inr ?inr_inl // => A B. + pose e := restrict [pred t | x \in D1 t] sedge. apply: (homo_connect (e:= e) (f := inl)). * move => a b. rewrite /e /= !in_simpl -andbA => /and3P[? ? ?]. by rewrite !imset_f. * apply: sbag_conn => //. move: A. by case/imsetP => ? ? [->]. move: B. by case/imsetP => ? ? [->]. + pose e := restrict [pred t | x \in D2 t] sedge. apply: (homo_connect (e:= e) (f := inr)). * move => a b. rewrite /e /= !in_simpl -andbA => /and3P[? ? ?]. by rewrite !imset_f. * apply: sbag_conn => //. move: A. by case/imsetP => ? ? [->]. move: B. by case/imsetP => ? ? [->]. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)