My foremost problem is on which ordinal should I do induction?
If I do induction on
, which seems the most natural choice, I face the problem that ordinal addition is defined "on the right", and is moreover not commutative.
(for example, the base case would be that
, but the definition of addition with 0 is
. This could be circumvented, but I think it will prove more difficult to do so in the later cases).
On the other hand, if I do induction on
, then sooner or later I would get
, and then what?
Could you at least give me this hint?