proposition: Lemma rename_decomp (T : forest) (G H : sgraph) D (dec_D : sdecomp T G D) (h : G -> H) : hom_s h -> surjective h -> (forall x y : H, x -- y -> exists x0 y0, [/\ h x0 = x, h y0 = y & x0 -- y0]) -> (forall x y, h x = h y -> (exists t, (x \in D t) && (y \in D t)) \/ (exists t1 t2, [/\ t1 -- t2, x \in D t1 & y \in D t2])) -> @sdecomp T _ (rename D h).
proof: Proof. move => hom_h sur_h sur_e comp_h. split. - move => x. pose x0 := iinv (sur_h x). case: (sbag_cover dec_D x0) => t Ht. exists t. apply/imsetP. by exists x0; rewrite // f_iinv. - move => x y xy. case: (sur_e _ _ xy) => x0 [y0] [hx0 hy0 e0]. case: (sbag_edge dec_D e0) => t /andP [t1 t2]. exists t. apply/andP;split;apply/imsetP;by [exists x0|exists y0]. - move => x t0 t1 bg1 bg2. case/imsetP : bg1 bg2 => x0 A B /imsetP [x1 C E]. subst. have connT x t t' : x \in D t -> x \in D t' -> connect (restrict [pred t | h x \in (rename D h) t] sedge) t t'. { move => Ht Ht'. apply: connect_mono (sbag_conn dec_D Ht Ht') => u v /= /andP [/andP [X Y] Z]. rewrite Z andbT. apply/andP;split; by apply/imsetP;exists x. } case: (comp_h _ _ E). + case => t /andP [F I]. apply: (connect_trans (y := t)); [exact: connT|rewrite E;exact:connT]. + move => [t0'] [t1'] [t0t1 H0 H1]. apply: connect_trans (connT _ _ _ A H0) _. rewrite E. apply: connect_trans (connect1 _) (connT _ _ _ H1 C). by rewrite /= t0t1 !inE -{1}E !imset_f. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)