Confused about preservation of well-quasi-orders I don't understand preservation of well quasi-orders, here is what I have thought about:

Definition A binary relation $R$ on $X$ is a quasi-order when it is reflexive and transitive.
Definition A quasi-order $\le$ is a well quasi-order when it satisfies any of the following equivalent conditions:  


*

*(nowhere ascending chain condition) every sequence $x_1,x_2,x_3\ldots$ with $\lnot x_1 \le x_2$, $\lnot x_2 \le x_3$, $\ldots$ is finite.  

*(strictly descending chain condition) every strictly descending chain $\ldots \le x_2 \le x_1$ with $\lnot x_2 \le x_1$, $\lnot x_3 \le x_2$, $\ldots$ is finite.

*(finitely generated ideal condition) every ideal is finitely generated. An ideal $I$ is such that for all $x \in I$, $y \in X$ that $x \le y$ implies $y \in I$. To be finitely generated means $I$ is the smallest ideal containing some finite set of points.


Theorem Let $R,S$ be well quasi-orders on $X$ with $R \subseteq S$ (so $aRb$ implies $aSb$). Then $R$ W.Q.O. implies $S$ W.Q.O.
explanation I tried to prove the theorem using several different definitions I still didn't feel that I understand the relationship.
proof using nowhere ascending chain condition: any ascending chain in $S$ is an ascending chain in $R$, therefore finite.
strictly descending chain condition: I can't get this proof to work but here's what I tried:
(1) Let $\ldots R x_2 R x_1$ be an ascending chain in $R$, then it is also an ascending chain in $S$ because $R$ is stricter than $S$.
(2) Let $\lnot x_2 S x_1$, $\lnot x_3 S x_2$, $\lnot x_3 S x_2$ then this also holds for $R$ because there are less $R$-relations.
Now the proof could suppose a strictly descending chain in $S$, then either we have an strictly descending chain in $R$ hence it's finite - or the $S$ chain is infinite and gets broken up into infinitely many finite pieces in $R$: Then we have infinitely many relations of type $\lnot x_{b+1}Rx_b$, and also $x_i R x_{i+1}$ for all $i$.
I don't see the contradiction here though..
finitely generated ideal condition: Any $S$-ideal is an $R$-ideal too, so finitely generated.

so I tried proving the preservation for various different equivalent definition but I don't feel like I understand it any more and I couldn't make the proof work for one def. Also I defined a well-quasi order here and it became non-well-founded when dtldalek extended it to a total order - that seems to go directly against the theorem.
So I'm really confused about this, how should I understand the preservation intuitively? and what I do need to fix the middle proof? (although that middle proof might not lead to any insight in which case I don't care about it)
 A: This may not answer your immediate question but elaborates on why you need not worry about it.
Recall that many interesting definitions come (like here) from observations that certain conditions are equivalent:


*

*a subgroup is invariant under conjugation iff it is the kernel of some homomorphism iff left cosets are the same as right cosets - gives rise to the definition of normal subgroup;

*a family of vectors is maximal among linear independant families iff it is minmal among gereating families iff it is both linearaly independent and generating - gives rise to the definition of basis of a vector space. 


Such a - non-obvious - equivalence makes the concept comprised by (each/all of) the conditions interesting and therefore justifies coining a name for it by making a definition. And because the equivalence should at least be somewhat surprising and non-obvios, at least one step in proving the equivalence typically requires a bit of non-trivial work. As with all theorems, there is no need to reinvent the wheel later, but rather apply the theorem.
Therefore, there is no need to use all equivalent condiotions in a proof. In fact, you'd be allowed to assume that $S$ is w.q.o. by condition 2, say, and show that then $R$ is w.q.o. by condition 1, for example.
A: Part of the problem, as Marc van Leeuwen noted, is that your definitions of well-quasi-order aren’t quite right. Start with a quasi-order $\le$ (i.e., a reflexive, transitive relation) on $X$. Then $\langle X,\le\rangle$ is a well-quasi-order if it satisfies any of the following equivalent conditions:

*

*For any sequence $\langle x_k:k\in\Bbb N\rangle$ in $X$ there are $i,k\in\Bbb N$ such that $i<k$ and $x_i\le x_k$.

*$\langle X,\le\rangle$ is well-founded and has no infinite antichains. That is, there is neither an infinite strictly decreasing sequence nor an infinite set of pairwise incomparable elements.

*$\langle X,\le\rangle$ is well-founded, and every $A\subseteq X$ has only finitely many minimal elements.

*Every sequence $\langle x_k:k\in\Bbb N\rangle$ in $X$ has an infinite ascending subsequence.

Here (1)-(3) correspond more or less to your three conditions.

Theorem. Suppose that $\le$ and $\preceq$ are quasi-orders on $X$ such that $x\preceq y$ whenever $x\le y$. If $\le$ is a well-quasi-order, then so is $\preceq$.

A proof using (2) is entirely possible.

Proof. Any antichain in $\langle X,\preceq\rangle$ is an antichain in $\langle X,\le\rangle$, so it’s immediate that $\langle X,\preceq\rangle$ has no infinite antichains.
Now suppose that $\preceq$ is not well-founded, and let $\langle x_k:k\in\Bbb N\rangle$ be a such that $x_{k+1}\prec x_k$ for each $k\in\Bbb N$. Let $[\Bbb N]^2$ be the set of unordered pairs of non-negative integers. Define $$\varphi:[\Bbb N]^2\to\{0,1,2\}:\{i,k\}\mapsto\begin{cases}0,&\text{if }i<k\text{ and }x_i\le x_k\\1,&\text{if }i<k\text{ and }x_k<x_i\\2,&\text{if }x_i\not\le x_k\text{ and }x_k\not\le x_i\;;\end{cases}$$ by Ramsey’s theorem there is an infinite $H\subseteq\Bbb N$ such that $\varphi$ is constant on $[H]^2$. If the value of $\varphi$ on $[H]^2$ is $2$, the elements of $H$ are an infinite antichain in $\langle X,\le\rangle$, which is impossible. If the value of $\varphi$ on $[H]^2$ is $1$, $H$ is an infinite strictly decreasing sequence in $\langle X,\le\rangle$, which is also impossible. Thus, $x_i\le x_k$ whenever $i,k\in H$ with $i<k$, and it follows that $x_i\preceq x_k$ for all $i,k\in H$ with $i<k$, contradicting the choice of the sequence $\langle x_k:k\in\Bbb N\rangle$. Thus, $\preceq$ is well-founded. $\dashv$

A: I found answer here Gallier, Jean H. (1991), "What's so special about Kruskal's theorem and the ordinal Γ0? A survey of some results in proof theory", Ann. Pure Appl. Logic 53 (3):
