Question on inductive {definitions, proof} Consider the following inductive definition:
Define the set $\Lambda$ as follows (where the $\langle x, y, z\rangle$ denote ordered triples):


*

*if $n \in \mathbb{N},$ then $\langle 0, n, n\rangle \in \Lambda \;$;

*if $n \in \mathbb{N}$ and $x \in \Lambda$ then $\langle 1, n, x \rangle \in \Lambda \;$;

*if $x, y \in \Lambda$, then $\langle 2, x, y \rangle \in \Lambda$.


Now define the function $\ell:\Lambda \to \mathbb{N}$ recursively as follows:


*

*$\ell(\langle 0, n, n \rangle) = 1, \forall \; n \in \mathbb{N}$;

*$\ell(\langle 1, n, x \rangle) = 1 + \ell(x), \forall \; n \in \mathbb{N}$ and $x \in \Lambda$;

*$\ell(\langle 2, x, y \rangle) = \ell(x) + \ell(y), \forall \; x, y \in \Lambda$.


It is obvious that $\ell(x) > 0, \forall \; x \in \Lambda$, but I don't know how to prove it.  It looks like a case for proof by induction, but induction on what?
Thanks!
 A: What you want is known as structural induction, or more vaguely as "the induction principle implied by the inductive definition".
The crucial point is that every element of $\Lambda$ is there by virtue of one of your three rules -- this is sometimes hinted at by a fourth rule reading: "Nothing else is in $\Lambda$". Your inductive definition is really shorthand for the following set-theoretic construction:


*

*Given any set $A$, define $$\Phi(A) = \{\langle 0,n,n\rangle\mid n\in \mathbb N\} \cup (\{1\}\times \mathbb N \times A) \cup (\{2\}\times A\times A)$$

*Let $A_0=\varnothing$ and $A_{n+1}=\Phi(A_n)$ for all $n\ge 0$.

*Let $\Lambda$ be the union of all $A_n$. In other words $\Lambda=\bigcup_{n\in \mathbb N}A_n$.


Now, the structural induction principle says: In order to prove that some property holds for all $x\in\Lambda$ it suffices to prove for an arbitrary $A$ that if all $x\in A$ has the property, then the property holds for all $a\in\Phi(A)$.
This can principle can be justified by ordinary mathematical induction on $n$ for the statement that the property holds for every $x\in A_n$. When this is true for all $n$, then since every $x\in\Lambda$ is in some $A_n$, the property holds for every such $x$.
