YES (VAR va vb ta vc vy vg vh) (RULES c_union(c_insert(va,vb,ta),vc,ta) -> c_insert(va,c_union(vb,vc,ta),ta) c_union(c_emptyset(),vy,ta) -> vy c_union(c_Message_Oparts(vg),c_Message_Oparts(vh),tc_Message_Omsg()) -> c_Message_Oparts(c_union(vg,vh,tc_Message_Omsg())) ) (COMMENT Termination is shown by LPO with precedence: c_emptyset > c_union > c_Message_Oparts > tc_Message_Omsg > c_insert )