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.