proposition: Lemma decomp_dot2 (T1 T2 : forest) D1 D2 : sdecomp T1 (sskeleton G1) D1 -> sdecomp T2 (sskeleton G2) D2 -> width D1 <= 3 -> width D2 <= 3 -> exists T D, [/\ sdecomp T (sskeleton (G1 · G2)) D & width D <= 3].
proof: Proof. Proof using. move => dec1 dec2 W1 W2. case: (decomp_quot (e:=eqv_clot [:: (unl output, unr input)]) dec1 dec2 W1 W2 _ _). - apply admissible_eqv_clot. case => u v. rewrite !inE /= !xpair_eqE => /andP [/eqP -> /eqP->]; by rewrite !eqxx. - pose P' : {set union G1 G2} := [set unl input; unl output; unr output]. apply: (@leq_trans #|P'|); last apply cards3. apply: (@leq_trans #|[set (\pi x : G1 · G2) | x in P']|); last exact: leq_imset_card. apply: subset_leq_card. apply/subsetP => ? /imsetP [x H1 ->]. move: H1. rewrite /P -!setUA [[set _;_]]setUC !setUA. case/setUP => H1. * by rewrite imset_f. * move/set1P : H1 => ->. apply/imsetP. exists (unl output); first by rewrite !inE eqxx ?orbT. apply/eqquotP. eqv. - move => T [D] [A B [t C]]. exists T. exists D. split => //. apply/sdecomp_sskel. split => //. exists t. by rewrite C !imset_f // !inE ?eqxx ?orbT. 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)