I’ve written the first draft of the proof on conservative extension of the term order, but I plan to let it sit for a week so I can refine it and make sure there are no gaps before sharing it on this forum.
T_\omega is the set of finite branching trees such that for any node x, the length of the path from the root to x is finite. H is the well known set of finite terms, which is viewed as finite tree in the proof. R is the set of cyclic terms also viewed as rational trees, which has only finite number of its subtrees modulo isomorphism.
H\subset R \subset T_\omega.
There is already given a total ordering < on H, that is, (H, <) is total transitive order.
Proposition. There is a natural extension <' on T_\omega of <.
- <\; \subset\; <'.
- <' is total on T_\omega. (EDIT)
- <' is transitive.
Ín summary, (T_\omega, <') is total transitive order which extends the standard (H, <)
in a natural way. As R is a subset of T_\omega, it follows that restriction <' to R is also total and transitive.