If I naively generalize the homeomorphic embedding relation for labeled finite trees in this way, do I still have a wqo?

Question

The homeomorphic embedding relation for trees as I understand it is a well-quasi-order (wqo) on trees when the label of a node determines the number of children of that node, and there are a finite number of such labels. A description of what (I hope) I'm referring to is in section 5.1 of this article.

I want to naively generalize this wqo to trees wherein the labels do not determine the number of children, for the purpose of runtime termination checking with states being said ill-behaved trees.

Assuming that I'm testing the homeomorphic embedding relation $\leq$ according to the rules (if something looks wrong here, then trust the linked the paper and correct me instead):

$l \leq r = \begin{array}\\ c(s_1 \ldots s_n) \leq c(t_1 \ldots t_n) & \text{if} & l = c(s_1 \ldots s_n) \text{ and } r = c(t_1 \ldots t_n) \text{ and } s_1 \leq t_1 \ldots s_1 \leq t_n \\ s \leq c(t_1 \ldots t_n) & \text{if} & l = x(s_1 \ldots s_n) \text{ and } r = c(t_1 \ldots t_n) \text{ and } \exists i.s\leq t_i \\ false && \text{otherwise} \end{array}$

where $c$ is a label, $x$ is some other label, and $s_i$ and $t_i$ are subtrees (and the $c(\ldots)$ notation is a tree construction with $c$ as the root of a (sub)tree and $\ldots$ that (sub)tree's children).

Would I still have a wqo if I simply said the relation holds if I ever encounter (in the course of checking membership in the relation) a scenario where I'm checking $c(\ldots s_m) \leq c(\ldots t_n)$ and $m \neq n$?

My gut says that I still would have a wqo (the 'dives in' rule should force me to make the arity check and blow the whistle whenever the vanilla homeomorphic embedding would be too lenient on labels-with-inconsistent-children-counts, and catch the case of an infinite sequence of widening trees), but as with any procedural hack on a mathematical relation I feel a bit too dumb to be sure.

Answer 1

Here's a nice property of WQOs:

If $R$ is a WQO on terms, and $S$ is another transitive relation such that $$ R\ \subseteq\ S$$ Then $S$ is a WQO

Proof: Let $t_1,\ldots, t_n,\ldots$ be an infinite sequence of terms. Because $R$ is a WQO, there are $i, j$ with $i<j$ such that $t_i\ R\ t_j$. But this implies $t_i\ S\ t_j$, so $S$ is a WQO as well.

This (somewhat counter-intuitive) result means you can always make your relation more permissive while preserving the WQO property.