Values in an inductively defined sequence of sets Consider the following sequence of sets:
\begin{align}
T_0 &= \{(0,0)\} \\
T_{n+1} &= \{(1+x_1+x_2,y_1+y_2):(x_1,y_1)\in T_n, (x_2,y_2)\in T_k \text{ for some } k\leq n\} \\
 &\quad \cup \{(x_1,1+y_1):(x_1,y_1)\in T_n\}.
\end{align}
What values of $(a,b)$ are in $T_n$ for a given $n$?
For reference, here are the first couple values of $T_n$:
$T_1 = \{(1,0),(0,1)\}$
$T_2 = \{(1,2),(2,0),(3,0),(1,1),(2,1),(0,2)\}$ 
$T_3$ is pretty big. 
So far, I have that the first coordinate can take any value from $n$ to $2^n-1$, but I am having trouble finding a systematic way of describing corresponding possible values for the second coordinate. 
If it helps, this question is derived from trying to determine the possible lengths of a propositional formula of height $n$.
 A: As mentioned in the comment, it is probably better to ask the actual problem you wanted to solve. The current question has a rather messy and lengthy solution and might not be too useful. For that reason I only give here the main results and the main steps required in a proof.
The set of points $T_n$ is a convex set of lattice points $(x,y)$ in the 2D plane. It is relatively easy to show that $0 \leq x \leq 2^n-1$ and $0 \leq y \leq 2^{n-1}$. For the actual boundaries of the set, you will find that the set is bounded from below by two lines $x+y \geq n$ and $y \geq 0$. The upper limit is more complicated and consists of inequalities, the number of which increases with the value of $n$. One can show that for given $n$ and $x \in [0,2^n-1]$ that all points are found by
$$
\max (n-x,0) \leq y \leq 2^{k+1} + (n-k-2)(x+1) \qquad \qquad \qquad (*)
$$
where $k$ is an integer dependent on $x$ and given by
$$
2^k \leq x + 1 < 2^{k+1}.
$$

For proving this result a number of steps are required.
1) The range of $x$ and $y$. From the transformation it is immediately clear that $x,y \geq 0$. With the help of induction you can prove that the domain is restricted by $T_n \subset [0,2^n-1] \times [0,2^{n-1}]$ for $n\geq1$ using the maximum growth possible in either direction.
2) With induction you can also show that 
$$
(x,0) \in T_n \qquad\text{for}\qquad n\leq x\leq2^n-1
$$
$$
(x,n-x)\in T_n \qquad\text{for}\qquad 0 \leq x \leq n
$$
You can also use this to show that $x+y\geq n$ which establishes the lower bounds in $(*)$
3) If you would represent the sets graphically and consider the transformation for low values of $n$, it will be clear that the set $T_n$ is convex and that the boundary is a polygon.
4) The vertices of the polygon-boundary of $T_n$ are given by $(2^k-1,[n-k]2^k)$ for $0\leq k \leq n$. Note that each vertex under the first transformation rule maps on to the boundary of $T_{n+1}$, i.e., $(x,y) \rightarrow (2x+1,2y)$ gives that $(2^k-1,[n-k]2^k) \rightarrow (2^{k+1}-1,[(n+1)-(k+1)]2^{k+1})$ complemented with applying the second transformation on $(0,n) \rightarrow (0,n+1)$. The only other vertex to be added to make the boundary complete is the point $(n,0)$.
5) The rest of the boundary are straight lines connecting the vertices, giving rise to the upper limit in $(*)$. 
A full prove along these lines is possible but quite a bit of writing. 
The derivation can be simplified and made more intuitive, if we consider the sets $S_n=\cup_{i=0}^n T_n$. With the innitial condition $T_0=\{(0,0)\}$, we then find that
\begin{eqnarray}
S_{n+1}
 & = & \left[ \bigcup_{k=1}^{n+1} T_n \right] \cup T_0\\
 & = & \left[ \bigcup_{k=0}^{n} \{p+q+(1,0)|p \in T_{k}; q \in T_i \text{ with } 0 \leq i \leq k\} \cup \{p+(0,1)|p\in T_{k}\} \right] \cup T_0\\
 & = & \left[ \bigcup_{k=0}^{n} \{p+q+(1,0)|p \in T_{k}; q \in S_k\} \right] \cup \left[ \bigcup_{k=0}^{n} \{p+(0,1)|p\in T_{k}\} \right] \cup S_0\\
 & = & \{p+q+(1,0)|p,q \in S_n\} \cup \{p+(0,1)|p\in S_{n}\} \cup S_0
\end{eqnarray}
Effectively, this means that $S_n$ is obtained by adding the grid-points $(x,y)$ in the triange $x,y\geq$ and $x+y<n$ to $T_n$.
By considering $q=(0,1)$ in the first set, it is obvious that almost all points generated by the second set in the prescription for $S_{n+1}$ are already included by the first set. The only exception are the points $(0,y)$ with $1 \leq y \leq n+1$. Including the point $(0,0)$, we can therefore summarize the sets $S_n$ by
\begin{eqnarray}
S_0 & = & \{(0,0)\} \\
S_{n+1} & = & \{p+q+(1,0)|p,q \in S_n\} \cup \{(0,k) |0 \leq k \leq n+1 \}
\end{eqnarray}

We now apply a particular translation of the points in each set $S_n$, that will depend explicitly on $n$. This does of course not affect their number or the shape of the set in a graphical representation, and obtain the sets $R_n$
$$
R_n = \{p-(2^{n-2}-1,0) | p \in S_n\}
$$
This results in $R_0=\{(\frac{3}{4},0)\}$ and $R_1=\{(\frac{1}{2},0),(\frac{1}{2},1),(\frac{3}{2},0)\}$, but for $n \geq 2$ the set $R_n$ will only contain integer grid-points.
Applying this translation to the transformation for $T_n$, we find that this results in
\begin{eqnarray}
R_0 & = & \{(\frac{3}{4},0)\} \\
R_{n+1} & = & \{p+q|p,q \in R_n\} \cup \{(1-2^{n-1},k) |0 \leq k \leq n+1 \}
\end{eqnarray}

This means that in each iteration the domain is mainly scaled by a factor 2 in both $x$ and $y$ direction with respect to the origin (this is the reason for the particular choice or translation) and a single vertical line of points is added on the extreme left side. With this in mind, it is then easy to check and prove by induction that for $n \geq 2$, the set $R_n$ contains all integer grid-points that are bounded by the inequalities $y \geq 0$, $x \geq 1-2^{n-2}$, and $ y \leq (k-1) (x+2^{n-2}) + 2^{k+1}$ for $0 \leq k < n$, as well as that the corresponding vertices of the polygon are given by $\{(2^{n-k}-2^{n-2}, k 2^{n-k})| 0 \leq k \leq n\} \cup \{(1-2^{n-2},0)\}$. 
Transforming this result back to the set $S_n$ and $T_n$ gives the results as mentioned above.
