proposition: Theorem eval_TW2 A (f: A -> graph2): (forall a, exists T D, [/\ sdecomp T (sskeleton (f a)) D & width D <= 3]) -> forall u, exists T D, [/\ sdecomp T (sskeleton (eval f u)) D & width D <= 3].
proof: Proof. move => Hf. elim => [u IHu v IHv | u IHu v IHv | u IHu | u IHu | | | a]. - move: IHu IHv => [T1] [D1] [? ?] [T2] [D2] [? ?]. exact: (decomp_dot2 (D1 := D1) (D2 := D2)). - move: IHu IHv => [T1] [D1] [? ?] [T2] [D2] [? ?]. exact: (decomp_par2 (D1 := D1) (D2 := D2)). - move: IHu => [T] [D] [D1 D2]. exists T. exists D. split => //. exact: decomp_cnv. - move: IHu => [T] [D] [D1 D2]. exists T. exists D. split => //. exact: decomp_dom. - apply: decomp_small. by rewrite card_unit. - apply: decomp_small. by rewrite card_sum card_unit. - apply Hf. 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)