proposition: Lemma decomp_quot (T1 T2 : forest) D1 D2 (e : equiv_rel (union G1 G2)): sdecomp T1 (sskeleton G1) D1 -> sdecomp T2 (sskeleton G2) D2 -> width D1 <= 3 -> width D2 <= 3 -> admissible e -> #|[set pi e x | x in P]| <= 3 -> exists T D, [/\ sdecomp T (skeleton (merge _ e)) D, width D <= 3 & exists t, D t = [set \pi x | x in P]].
proof: Proof. Proof using. move => /sdecomp_sskel [dec1 comp1] /sdecomp_sskel [dec2 comp2] W1 W2 adm_e collapse_P. move: comp1 comp2 => [t1 /andP[t1_in t1_out]] [t2 /andP[t2_in t2_out]]. pose T := tjoin T1 T2. pose D : tjoin T1 T2 -> {set sjoin G1 G2}:= decompU D1 D2. have dec_D: sdecomp T (sjoin G1 G2) D by exact: join_decomp. have dis_t1_t2 : ~~ connect (@sedge T)(inl t1) (inr t2) by rewrite join_disc. have dis_T12 : {in [set inl t1;inr t2] &, forall x y, x != y -> ~~ connect (@sedge T) x y}. { move => [?|?] [?|?] /setUP[] /set1P-> /setUP[]/set1P ->. all: by rewrite ?eqxx // => _; rewrite sconnect_sym. } pose T' := @tlink T _ dis_T12. pose D' := decompL D P : _ -> {set sjoin G1 G2}. have dec_D' : sdecomp T' (sjoin G1 G2) D'. { apply: decomp_link => //. apply/subsetP => x. rewrite !inE -!orbA => /or4P [] /eqP->. all: apply/bigcupP; solve [ by exists (inl t1) => //; rewrite ?inE ?imset_f ?eqxx | by exists (inr t2) => //; rewrite ?inE ?imset_f ?eqxx]. } pose h := pi e : skeleton (union G1 G2) -> skeleton (merge _ e). exists T'. exists (rename D' h); split; last by exists None. - apply: rename_decomp => //. + apply: hom_eqL (pi_hom (e := e)). exact: skel_union_join. + exact: pi_surj. + move => x y. move/sk_rel_mergeE => [? [x0] [y0] /= [? ? ?]]. exists x0;exists y0. split => //. by rewrite /edge_rel/= -skel_union_join. + move => x y. move/eqquotP => /=. case/adm_e => [<-|A]. * case: (sbag_cover dec_D' x) => t Ht. left. exists t. by rewrite Ht. * left. exists None. by rewrite /= -!sub1set -subUset. - rewrite /width (bigop.bigID (pred1 None)). rewrite bigop.big_pred1_eq. rewrite geq_max. apply/andP;split => //. + rewrite (bigop.reindex Some) /=. * apply: (@leq_trans (maxn (width D1) (width D2))); last by rewrite geq_max W1 W2. apply: leq_trans (join_width _ _). apply: bigmax_leq_pointwise => t _. exact: leq_imset_card. * apply: subon_bij; last by (apply bij_on_codom => //; exact: (inl t1)). by move => [x|]; rewrite !in_simpl // codom_f. Qed.
imports: Coq(RelationClasses Setoid) mathcomp(all_ssreflect) GraphTheory(edone set_tac finite_quotient preliminaries) GraphTheory(digraph sgraph treewidth minor equiv setoid_bigop) GraphTheory(structures mgraph pttdom ptt mgraph2 skeleton)