proposition: Lemma decomp_par2 (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 input, unr input); (unl output, unr output)]) dec1 dec2 W1 W2 _ _). - apply admissible_eqv_clot. case => u v. rewrite !inE /= !xpair_eqE => /orP [] /andP [/eqP -> /eqP->]; by rewrite !eqxx. - pose P' : {set union G1 G2} := [set unl input; unl output]. apply: (@leq_trans #|P'|); last by rewrite cards2; by case (_ != _). 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 ->]. case/setUP : H1 => H1; first case/setUP : H1 => H1. * by rewrite imset_f. * move/set1P : H1 => ->. apply/imsetP. exists (unl input); first by rewrite !inE eqxx ?orbT. apply/eqquotP. eqv. * 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)