proposition: Lemma forest_TW1 (G : sgraph) : is_forest [set: G] -> exists T B, sdecomp T G B /\ width B <= 2.
proof: Proof. elim/(size_ind (fun G : sgraph => #|G|)) : G => G Hind forest_G. have:= forest_vseparator forest_G. case: leqP => [Glt2 _|Ggt2 /(_ isT) [S sepS Slt2]]; first exact: decomp_small. have [V1 [V2 [[sep [x0 [y0 [Hx0 Hy0]]]] SV12]]] := vseparator_separation sepS. have V1properG: #|induced V1| < #|G|. { rewrite card_sig. eapply card_ltnT. simpl. eauto. } have {x0 Hx0 y0 Hy0} V2properG: #|induced V2| < #|G|. { rewrite card_sig. eapply card_ltnT. simpl. eauto. } have C: clique (V1 :&: V2) by rewrite -SV12; exact: small_clique. case: (Hind (induced V1)) => // [|T1 [B1 [sd1 w1]]]. { apply: induced_forest. exact: sub_forest forest_G. } case: (Hind (induced V2)) => // [|T2 [B2 [sd2 w2]]]. { apply: induced_forest. exact: sub_forest forest_G. } case separation_decomp with G V1 V2 T1 T2 B1 B2 => // T [B [sd w]]. exists T. exists B. split => //. apply leq_trans with (maxn (width B1) (width B2)) => //. by rewrite geq_max w1 w2. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)