text:
\begin{document}

\begin{abstract} In \cite{S3} I solved the Thom's conjecture that a proper Thom map is triangulable. In this paper I drop the properness condition in the semialgebraic case and, moreover, in the definable case in an o-minimal structure.
\end{abstract}

\maketitle

\section{Introduction}
Let $r$ be always a positive integer or $\infty$, $X$ and $Y$ subsets of $\R^m$ and $\R^n$, respectively, and $f:X\to Y$ a $C^r$ map (i.e., $f$ is extended to a $C^r$ map from an open neighborhood of $X$ in $\R^m$ to one of $Y$ in $\R^n$).
A {\it $C^r$ stratification} of $f$ is a pair of $C^r$ stratifications $\{X_i\}$ of $X$ and $\{Y_j\}$ of $Y$ such that for each $i$, the image $f(X_i)$ is included in some $Y_j$ and the restriction map $f|_{X_i}:X_i\to Y_j$ is a $C^r$ submersion.
We call also $f:\{X_i\}\to\{Y_j\}$ a {\it $C^r$ stratification} of $f:X\to Y$.
We call $f:X\to Y$ a {\it Thom $C^r$ map} if there exists a Whitney $C^r$ stratification $f:\{X_i\}\to\{Y_j\}$ such that the following condition is satisfied.
Let $X_i$ and $X_{i'}$ be strata with $X_{i'}\cap(\overline X_i-X_i)=\emptyset$.
If $\{a_k\}$ is a sequence of points in $X_i$ converging to a point $b$ of $X_{i'}$ and if the sequence of the tangent spaces $\{T_{a_k}(f|_{X_i})^{-1}(f(a_k))\}$ converges to a space $T\subset\R^m$ in the Grassmannien space $G_{m,m'},\ m'=\dim (f|_{X_i})^{-1}(f(a_k))$, then $T_b(f|_{X_{i'}})^{-1}(f(b))\subset T$.
We call then $f:\{X_i\}\to\{Y_j\}$ a {\it Thom $C^r$ stratification} of $f:X\to Y$.
In \cite{S3} I solved the following Thom's conjecture.

\begin{thm}
Assume $X$ and $Y$ are closed in $\R^m$ and $\R^n$, respectively, and $f:X\to Y$ is a proper Thom $C^\infty$ map.
Then there exist homeomorphisms $\tau$ and $\pi$ from $X$ and $Y$ to polyhedra $P$ and $Q$, respectively, such that $\pi\circ f\circ\tau^{-1}:P\to Q$ is piecewise-linear.
\end{thm}

Here a natural question arises.
Whether can we drop the properness condition?
Indeed, the condition is too strong for some applications.
For example, the natural map from a $G$-manifold $M$ to its orbit space is a Thom map but not necessarily proper provided the action $G\times M\ni(g,x)\to(g x,x)\in M^2$ is proper (see \cite{MS}).
In the present paper we give a positive answer in the semialgebraic or definable case.
A $C^r$ stratification $f:\{X_i\}\to\{Y_j\}$ of $f:X\to Y$ is called {\it semialgebraic} ({\it definable}) if $X,\,Y,\,f,\,X_i$ and $Y_j$ are all semialgebraic (definable, respectively,) and $\{X_i\}$ and $\{Y_j\}$ are finite stratifications.

\begin{thm}\label{thmA}
Assume $X$ and $Y$ are closed and semialgebraic (definable in an o-minimal structure) in $\R^m$ and $\R^n$, respectively, and $f:X\to Y$ is a semialgebraic (definable, respectively,) Thom $C^1$ map.
Then there exist finite simplicial complexes $K$ and $L$ and semialgebraic (definable, respectively,) $C^0$ imbeddings $\tau:X\to|K|$ and $\pi:Y\to|L|$ such that $\tau(X)$ and $\pi(Y)$ are unions of some open simplexes of $K$ and $L$, respectively, and $\pi\circ f\circ\tau^{-1}:\tau(X)\to\pi(Y)$ is extended to a simplicial map from $K$ to $L$, where $|K|$ denotes the underlying polyhedron to $K$.
\end{thm}

The theorem does not necessarily hold without the condition that $X$ is closed in $\R^m$.
A counter-example is given by $X=\R^2-\{(x,y)\in\R^2:x=0,\ y\not=0\},\ Y=\R^2$ and $f(x,y)=(x,x y)$.
Such $f$ is not triangulable in the weak sense that there exist $C^0$ imbeddings $\tau$ of $X$ and $\pi$ of $Y$ into some Euclidean space $\R^n$ such that $\overline{\tau(X)}$ is a polyhedron and $\pi\circ f\circ\tau^{-1}:\tau(Y)\to\pi(X)$ is extended to a piecewise-linear map $\theta:\overline{\tau(X)}\to\R^n$ for the following reason.
Assume there exist $\tau$ and $\pi$ as required.
Then $\overline{\tau(X)}$ is of dimension two and $\theta^{-1}(y)$ is of dimension 0 for each $y\in\overline{\pi(Y)}$ because $\theta$ is piecewise-linear and $\theta|_{\tau(X)}$ is injective.
Hence a small compact neighborhood $U$ of $\tau(0)$ in $\overline{\tau(X)}$ does not intersect with $\theta^{-1}(\pi(0))$ except at $\tau(0)$.
Choose a point $(x_1,x_2)$ in $X$ with $x_2\not=0$ so close to 0 that the half-open segment $L$ with ends $(0,x_2)$ and $(x_1,x_2)$ in $X$ is included in $\tau^{-1}(U)$.
Then $\overline{f(L)}-f(L)=\{0\}$ and $\overline{\pi\circ f(L)}-\pi\circ f(L)=\{\pi(0)\}$.
Hence $(\overline{\tau(L)}-\tau(L))\cap U=\{\tau(0)\}$ or $(\overline{\tau(L)}-\tau(L))\cap U=\emptyset$ since $\theta^{-1}(\pi(0))=\{\tau(0)\}$ in $U$.
The former case contradicts the definition of $L$ and the fact that $\tau$ is a $C^0$ imbedding, and the latter does the fact that $U$ is compact. \par
  An open problem is whether a Thom $C^1$ map $f:X\to Y$ is triangulable in this weak sense under the condition that $X$ is closed in $\R^n$ or, equivalently, $X$ is locally compact.

\section{Tube systems}
If $r$ is larger than one, $C^r$ {\it tube} at a $C^r$ submanifold $M$ of $\R^n$ is a triple $T=(|T|,\pi,\rho)$, where $|T|$ is an open neighborhood of $M$ in $\R^n$, $\pi:|T|\to M$ is a submersive $C^r$ retraction and $\rho$ is a non-negative $C^r$ function on $|T|$ such that $\rho^{-1}(0)=M$ and each point $x$ on $M$ is a unique and non-degenerate critical point of $\rho|_{\pi^{-1}(x)}$.
We will need to consider a $C^1$ tube.
Assume $M$ is a $C^1$ submanifold of $\R^n$.
Let $|T|$ be an open neighborhood of $M$ in $\R^n$, $\pi:|T|\to M$ a $C^1$ map and $\rho$ a $C^1$ function on $|T|$.
We call $T=(|T|,\pi,\rho)$ a $C^1$ {\it tube} at $M$ if there exists a $C^1$ imbedding $\tau$ of $|T|$ into $\R^n$ such that $\tau(M)$ is a $C^2$ submanifold of $\R^n$ and $\tau_*T=(\tau(|T|),\tau\circ\pi\circ\tau^{-1},\rho\circ\tau^{-1})$ is a $C^2$ tube at $\tau(M)$.
(See pages 33--40 in \cite{S2}, which says the arguments on tube systems in \cite{G} work in the $C^1$ category.)
A $C^r$ {\it tube system} $\{T_j\}$ for a $C^r$ stratification $\{Y_j\}$ of a set $Y\subset\R^n$ consists of one tube $T_j$ at each $Y_j$.
We define a $C^r$ {\it weak tube system} $\{T_j=(|T_j|,\pi_j,\rho_j)\}$ for the same $\{Y_j\}$ weakening the conditions on $\rho_j$ as follows.
Each $\rho_j$ is a non-negative $C^0$ function on $|T_j|$ with zero set $Y_j$, of class $C^r$ on $|T_j|-Y_j$ and regular on $Y_{j'}\cap\pi^{-1}_j(y)-Y_j$ for each $y\in Y_j$ and $Y_{j'}$.
Note a $C^r$ tube system is a $C^r$ weak tube system if $\{Y_j\}$ is a Whitney stratification by Lemma I.1.1, \cite{S2}.
In the following arguments we shrink $|T_j|$ many times without mention. \par
  We call a $C^r$ (weak) tube system $\{T_j\}$ for $\{Y_j\}$ {\it controlled} if for each pair $j$ and $j'$ with $(\overline{Y_{j'}}-Y_{j'})\cap Y_j\not=\emptyset$,
$$
\pi_j\circ\pi_{j'}=\pi_j\quad\text{and}\quad \rho_j\circ\pi_{j'}=\rho_j\quad\text{on}\ |T_j|\cap|T_{j'}|.
$$
Remember there exists a controlled $C^r$ tube system for a Whitney stratification (see \cite{G} and \cite{S2}), note if $\{T_j\}$ is such a $C^r$ tube system then the map $(\pi_j,\rho_j)|_{Y_{j'}\cap|T_j|}$ is a $C^r$ submersion into $Y_j\times\R$ because
$$
(\pi_j,\rho_j)|_{Y_{j'}\cap|T_j|}\circ\pi_{j'}=(\pi_j,\rho_j)\quad\text{on}\ |T_j|\cap|T_{j'}|,
$$
and if we assume only $\pi_j\circ\pi_{j'}=\pi_j$ on $|T_j|\cap|T_{j'}|$ then $\pi_j|_{Y_{j'}\cap|T_j|}$ is a $C^r$ submersion into $Y_j$.
In the case of a $C^r$ weak tube system $(\pi_j,\rho_j)|_{Y_{j'}\cap|T_j|-Y_j}$ is a $C^1$ submersion into $Y_j\times\R$.
Let $f:\{X_i\}\to\{Y_j\}$ be a $C^r$ stratification of a $C^r$ map $f:X\to Y$ between subsets of $\R^m$ and $\R^n$, respectively, $\{T_j^Y=(|Y_j^Y|,\pi_j^Y,\rho_j^Y)\}$ a controlled $C^r$ (weak) tube system for $\{Y_j\}$ and $\{T_i^X=(|T_i^X|,\pi_i^X,\rho_i^X)\}$ a $C^r$ (weak) tube system for $\{X_i\}$.
We call $\{T_i^X\}$ {\it controlled over} $\{T_j^Y\}$ if the following four conditions are satisfied.
Let $f$ be extended to a $C^r$ map $\tilde f:\cup_i|T_i^X|\to\R^n$. \par\noindent
(1) For each $(i,j)$ with $f(X_i)\subset Y_j$,
$$
f\circ\pi_i^X=\pi_j^Y\circ\tilde f\quad\text{on}\ |T_j^X|\cap\tilde f^{-1}(|T_j^Y|).
$$\par\noindent
(2) For each $j$, $\{T_i^X:f(X_i)\subset Y_j\}$ is a controlled $C^r$ (weak) tube system for $\{X_i:f(X_i)\subset Y_j\}$. \par\noindent
(3) For each pair $i$ and $i'$ with $(\overline{X_{i'}}-X_{i'})\cap X_i\not=\emptyset$,
$$
\pi_i^X\circ\pi_{i'}^X=\pi_i^X\quad\text{on}\ |T_i^X|\cap|T_{i'}^X|.
$$\par\noindent
(4) For each $(i,j)$ with $f(X_i)\subset Y_j$ and $(i',j')$ with $(\overline{X_{i'}}-X_{i'})\cap X_i\not=\emptyset$ and $f(X_{i'})\subset Y_{j'}$, $(\pi_i^X,f)|_{X_{i'}\cap|T_i^X|}$ is a $C^r$ submersion into the fiber product $X_i\times_{(f,\pi_j^Y)}(Y_{j'}\cap|T_j^Y|)$---the $C^r$ manifold $\{(x,y)\in X_i\times(Y_{j'}\cap|T_j^Y|):f(x)=\pi_j^Y(y)\}$. \par
  Note (4) is equivalent to the next condition. \par\noindent
(4)$'$ For $(i,j),\ (i',j')$ as in (4) and for each $x\in X_{i'}\cap|T_i^X|$, the germ of $\pi_i^X|_{X_{i'}\cap f^{-1}(f(x))}$ at $x$ is a $C^r$ submersion onto the germ of $X_i\cap f^{-1}(\pi_j^Y\circ f(x))$ at $\pi_i^X(x)$. \par
  This definition of controlledness is stronger than that in \cite{G}.
In \cite{G}, (4) is not assumed.
However, if $f:\{X_i\}\to\{Y_j\}$ is a Thom map then (4) immediately follows from (1), (2) and (3), and existence of a $C^r$ tube system $\{T_i^X\}$ for $\{X_i\}$ controlled over a given controlled $C^r$ tube system $\{T_j^Y\}$ for $\{Y_j\}$ is known (see \cite{G} and \cite{S2}).
We shall treat a $C^1$ stratification $f:\{X_i\}\to\{Y_j\}$ of $f$ which is not necessarily a Thom $C^1$ stratification but admits a controlled $C^1$ tube system $\{T_j^Y\}$ for $\{Y_j\}$ and a $C^1$ weak tube system $\{T_i^X\}$ for $\{X_i\}$ controlled over $\{T_j^Y\}$. \par
  In \cite{S3} theorem 1.1 is proved in the following more general form.

\begin{thm}
Let $f:\{X_i\}\to\{Y_j\}$ be a $C^\infty$ stratification of a $C^\infty$ proper map $f:X\to Y$ between closed subsets of Euclidean spaces.
Assume there exist a controlled $C^\infty$ tube system $\{T_j^Y\}$ for $\{Y_j\}$ and a $C^\infty$ tube system $\{T_i^X\}$ for $\{X_i\}$ controlled over $\{T_j^Y\}$.
Then there exist homeomorphisms $\tau$ and $\pi$ from $X$ and $Y$ to polyhedra $P$ and $Q$, respectively, closed in some Euclidean spaces such that $\pi\circ f\circ\tau^{-1}:P\to Q$ is piecewise linear and $\tau(\overline{X_i})$ and $\pi(\overline{Y_j})$ are all polyhedra.
If $f:\{X_i\}\to\{Y_j\},\,\{T_i^X\}$ and $\{T_j^Y\}$ are semialgebraic or, more generally, definable in an o-minimal structure, then we can choose semialgebraic or definable $\tau,\,\pi,\,P$ and $Q$.
\end{thm}

(Note a semialgebraic closed polyhedron in a Euclidean space is semilinear, i.e., is defined by a finite number of equalities and inequalities of linear functions.)
Moreover, the proof in \cite{S3} shows the following generalization though we do not repeat its proof.

\begin{thm}
Let $f:\{X_i\}\to\{Y_j\}$ be a $C^1$ stratification of a $C^1$ proper map $f:X\to Y$ between closed subsets of Euclidean spaces.
Let $I$ denote the set of indexes $i$ of $X_i$ such that $f|_{X_i}$ is not injective.
Assume there exist a controlled $C^1$ tube system $\{T_j^Y\}$ for $\{Y_j\}$ and a $C^1$ weak tube system $\{T_i^X\}$ for $\{X_i\}$ controlled over $\{T_j^Y\}$ such that $\{T_i^X:i\in I\}$ is a $C^1$ tube system for $\{X_i:i\in I\}$.
Then the result in theorem 2.1 holds.
\end{thm}

We will prove theorem 1.2 by compactifying $f:X\to Y$ in theorem 1.2 and applying theorem 2.2 to the compctification.
There are two unusual problems which we encounter.
First the arguments do not work in the $C^2$ category and apply the $C^1$ category.
Secondly we construct $\{T_j^Y:Y_j\subset\overline Y\}$ and $\{T_i^X:X_i\subset X\}$ by induction on $\dim Y_j$ and $\dim X_i$ but the induction of construction of $\{T_i^X:X_i\subset\overline X-X\}$ is downward.
The two inductions are not independent and we need special conditions (iv) and (ix) for tube systems in the proof below.
It is natural to ask whether we can extend $f$ to a Thom map $\overline f$.
The answer is negative.
To keep the property that $f$ is a Thom map also we use (iv) and (ix).

\section{Proof theorem \ref{thmA}}
{\it Proof of theorem \ref{thmA}.}
We assume $X$ is non-compact and $X$ and $Y$ are bounded in $\R^m$ and $\R^n$, respectively, by replacing $\R^m$ and $\R^n$ with $(0,\,1)^m$ and $(0,\,1)^n$ respectively.
Then $\overline X-X$ and $\overline Y-Y$ are compact.
Let $f:\{X_i\}\to\{Y_j\}$ be a semialgebraic Thom $C^1$ stratification of $f:X\to Y$.
Then we can assume $f$ is extendable to $\overline X$.
Apply Theorem II.4.1, \cite{S1} to the function on $\R^m$ measuring distance from the compact set $\overline X-X$.
Then we have a non-negative semialgebraic $C^0$ function $\phi$ on $\R^m$ such that $\phi^{-1}(0)=\overline X-X$ and $\phi|_{\R^m-(\overline X-X)}$ is of class $C^1$.
Choose $\epsilon>0\in\R$ so that $\phi$ is $C^1$ regular on $\phi^{-1}((0,\,\epsilon])$ and let $\phi'$ be a semialgebraic $C^1$ function on $\R$ such that $\phi'(0)=0$, $\phi'$ is regular on $(0,\,\epsilon)$ and $\phi'=1$ on $[\epsilon,\,\infty)$.
Set
$$
\Phi(x)=(\phi'\circ\phi(x),\phi'\circ\phi(x)x)\quad\text{for}\ x\in X. $$
Then $\Phi$ is a semialgebraic $C^1$ imbedding of $X$ into $\R^{m+1}$ such that $\Phi(X)$ is bounded and $\overline{\Phi(X)}-\Phi(X)=\{0\}$.
Hence replacing $X$ with $\Phi(X)$ we assume $\overline X-X=\{0\}$ from the beginning.
Moreover, replace $X$ with the graph of $f$.
Then we suppose $X$ is contained and bounded in $\R^m\times\R^n$, $\overline X-X\subset\{0\}\times\overline Y$, $f:X\to Y$ is the restriction of the projection $p:\R^m\times\R^n\to\R^n$ and hence $f$ is extended to a semialgebraic $C^1$ map $\overline f:\overline X\to\overline Y$. \par
  By the same reason we assume $\overline Y-\{0\}$.
Note then $\{Y_j,0\}$ is a semialgebraic Whitney $C^1$ stratification of $\overline Y$.
Let $\{T_j^Y\}$ be a controlled semialgebraic $C^1$ tube system for $\{Y_j\}$ and $\{T_i^X\}$ a semialgebraic $C^1$ tube system for $\{X_i\}$ controlled over $\{T_j^Y\}$.
Assume the set of indexes of $Y_j$ does not contain 0, set $Y_0=\{0\}$ and add $Y_0$ to $\{Y_j\}$.
Then we can assume there is a semialgebraic $C^1$ tube $T_0^Y=(|T_0^Y|,\pi_0^Y,\rho_0^Y)$ at $Y_0$ such that $\{T_j^Y,T_0^Y:j\not=0\}$ is controlled for the following reason. \par
  Let $|T_0^Y|$ be the closed ball $B(\epsilon)$ with center 0 in $\R^n$ and with small radius $\epsilon>0$ (we treat closed balls in place of open balls for simplicity of notation), and set $\pi_0^Y(y)=0$ and, tentatively, $\rho_0^Y(y)=|y|^2$ for $y\in|T_0^Y|$.
Then the condition $\rho_0^Y\circ\pi_j^Y=\rho_0^Y$ on $|T_0^Y|\cap|T_j^Y|$ for $j\not=0$ does not necessarily hold.
For that condition it suffices to find a semialgebraic homeomorphism $\tau$ of $\R^n$ of class $C^1$ outside of 0 and such that $\tau(0)=0$, $\tau=\id$ outside of $B(\epsilon)$ and $\rho_0^Y\circ\pi_j^Y\circ\tau^{-1}=\rho_0^Y$ on $B(\epsilon')\cap\tau(|T_j^Y|)$ for $j\not=0$, shrunk $|T_j^Y|$ and some $\epsilon'>0$. \par
  Let $Y_j$ be such that $\dim Y_j$ is the smallest in $\{Y_j:0\in\overline{Y_j},\,j\not=0\}$, and choose $\epsilon$ so small that $\rho_0^Y|_{Y_j\cap|T_0^Y|}$ is $C^1$ regular, which implies that $\rho_0^{Y-1}(\epsilon'^2)$ is transversal to $Y_j$ for any $0<\epsilon'\le\epsilon$.
Set $Y_j(\epsilon')=Y_j\cap\rho_0^{Y-1}(\epsilon'^2)$.
We will define a semialgebraic homeomorphism $\tau_j$ of $\R^n$ of class $C^1$ outside of 0 such that $\tau_j(0)=0$, $\tau_j=\id$ outside of $B(\epsilon)$ and $\rho_0^Y\circ\pi_j^Y\circ\tau_j^{-1}=\rho_0^Y$ on $B(\epsilon/2)\cap\tau_j(|T_j^Y|)$ for shrunk $|T_j^Y|$.
Since the problem is local at $Y_j$, we can assume by Thom's first isotopy lemma (see Theorem II.6.1 and it complement, [4]) that
$$
|T_0^Y|\cap Y_j=Y_j(\epsilon)\times(0,\,\epsilon^2],\ \text{after then,}\ |T_0^Y|\cap|T_j^Y|=\cup\{y+L_y:y\in Y_j(\epsilon)\}\times(0,\,\epsilon^2]
$$
and $\pi_j^Y(y+z,t)$ and $\rho_0^Y(y+z,t)$ are of the form $(y,\pi_j^{Y\prime}(y+z,t))$ and $t$, respectively, for $y\in Y_j(\epsilon)$ and $(z,t)\in L_y\times(0,\,\epsilon^2]$, where $L_y$ is a linear subspace of the tangent space $T_y\rho_0^{Y-1}(\epsilon^2)$ of codimension\,=\,$\codim Y_j$ in $\R^n$ such that the correspondence $Y_j(\epsilon)\ni y\to L_y\in G_{n,\codim Y_j}$ is semialgebraic and of class $C^1$ and $\pi_j^{Y\prime}$ is a semialgebraic $C^1$ function defined on $\cup\{y+L_y\}\times(0,\,\epsilon^2]$.
For simplicity of notation we write $\cup_{y\in Y_j(\epsilon)}\{y\}\times L_y$ as $Y_j(\epsilon)\times L$.
Transform $Y_j(\epsilon)\times L\times(0,\,\epsilon^2]$ by a semialgebraic $C^1$ diffeomorphism $(y,z,t)\to(y,z/kt^k,t)$ for sufficiently large integer $k$.
Then we can assume
$$|\pi_j^{Y\prime}(y+z,t)-t|\le\epsilon^2/28\ \ \text{and}\ \ |\frac{\partial\pi_j^{Y\prime}}{\partial t}(y+z,t)-1|<1/4\ \ \text{for}\ |z|\le 1\leqno{(0)}
$$
$$
\pi_j^{Y\prime}(y,t)=t. \leqno{\text{since}}
$$
Let $\xi$ be a semialgebraic $C^1$ function on $\R$ such that $0\le\xi\le 1,\ \xi=1$ on $(-\infty,\,1/2),\ \xi=0$ on $(2/3,\,\infty)$ and $|\frac{d\xi}{d t}|\le 7$.
Set
$$
\tau_j(y+z,t)=(y+z,(1-\xi(2t/\epsilon^2)\xi(|z|))t+\xi(2t/\epsilon^2)\xi(|z|)\pi_j^{Y\prime}(y+z,t))\qquad
$$
$$
\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\text{for}\ (y,z,t)\in Y_j(\epsilon)\times L\times(0,\,\epsilon^2].
$$
Then $\tau_j=\pi_j^Y$ if $t\le\epsilon^2/4$ and $|z|\le 1/2$, $\tau_j=\id$ if $t\ge\epsilon^2/3$ or $|z|\ge2/3$ and, moreover, $\tau_j$ is a diffeomorphism because
$$
|\frac{\partial}{\partial t}\big((1-\xi(t/\epsilon^2)\xi(|z|))t+\xi(t/\epsilon^2)\xi(|z|)\pi_j^{Y\prime}(y+z,t)\big)-1|\qquad\qquad\qquad\quad
$$
$$
\le\xi(t/\epsilon^2)\xi(|z|)|1-\frac{\partial\pi_j^{Y\prime}}{\partial t}(y+z,t)|+|\frac{d\xi}{d t}(t/\epsilon^2)\xi(|z|)|t-\pi_j^{Y\prime}(y+z,t)|/\epsilon^2
$$
$$
\qquad\qquad\qquad\qquad\qquad\qquad\le 1/4+1/4=1/2\quad\text{for}\ |z|\le 1.
$$
Thus we can assume $\rho_0^Y\circ\pi_j^Y=\rho_0^Y$ on $|T_0^Y|\cap|T_j^Y|$. \par
  Repeating the same arguments by induction on $\dim Y_{j'}$ for all $Y_{j'}$ with $0\in\overline{Y_{j'}}$ we obtain the required $\tau$.
Here we note only that for $j'$ with $\overline{Y_{j'}}-Y_{j'}\supset Y_j$, though $Y_{j'}(\epsilon)$ is not compact, $(0)$ can holds.
Indeed
$$
\rho_0^Y=\rho_0^Y\circ\pi_j^Y\circ\pi_{j'}^Y=\rho_0^Y\circ\pi_{j'}^Y\quad\text{on}\ |T_0^Y|\cap|T_j^Y|\cap|T_{j'}^Y|.
$$
Hence when we describe $\pi_{j'}^Y$ as above there is a semialgebraic neighborhood $U$ of $Y_j(\epsilon)\times(0,\,\epsilon^2]$ in $\overline{Y_{j'}(\epsilon)}\times(0,\,\epsilon^2]$ such that
$$
\pi_{j'}^{Y\prime}(y+z,t)=t\quad\text{for}\ (y,z,t)\in Y_{j'}(\epsilon)\times L_y\times(0,\,\epsilon^2]\ \text{with}\ (y,t)\in U.
$$
In conclusion we assume $Y$ is compact. \par
  If $f:\{X_i\}\to\{Y_j\}$ is extended to a Thom $C^1$ stratification of $\overline f:\overline X\to Y$, then theorem 1.2 follows from theorem 1.1 in the $C^1$ case.
However, such extension does not always exist.
Instead we will find a semialgebraic $C^1$ stratification $\overline f:\{X'_{i'}\}\to\{Y'_{j'}\}$ of $\overline f$, a controlled semialgebraic $C^1$ tube system $\{T_{j'}^{Y\prime}\}$ for $\{Y'_{j'}\}$ and a semialgebraic $C^1$ weak tube system $\{T_{i'}^{X\prime}\}$ for $\{X'_{i'}\}$ controlled over $\{T_{j'}^{Y\prime}\}$ such that $\{X'_{i'}\}|_X$ and $\{Y'_{j'}\}|_Y$ are substratifications of $\{X_i\}$ and $\{Y_j\}$.
Here $\{Y'_{j'}\}$ is a Whitney stratification but $\{X'_{i'}\}$ is not necessarily so. \par
  Set $Z=\overline X-X$, which is compact.
Note $Z=\{0\}\times\overline f(Z)$ and $\overline f|_Z$ is a homeomorphism onto $\overline f(Z)$.
Let $\{Y'_{j'}\}$ be a semialgebraic Whitney $C^1$ substratification of $\{Y_j\}$ such that each stratum is connected, $\overline f(Z)$ is a union of some $Y'_{j'}$'s and $\{X_i,\{0\}\times(Y'_{j'}\cap\overline f(Z))\}$ is a Whitney $C^1$ stratification of $\overline X$, which is constructed in the same way as the canonical semialgebraic $C^\omega$ stratification of a semialgebraic set since $\overline f(Z)$ is closed in $Y$.
Note $\{Y'_{j'}\}$ satisfies the frontier condition.
Set
$$
\{X'_{i'}\}=\{X_i\cap\overline f^{-1}(Y'_{j'}),Z\cap\{0\}\times Y'_{j'}\}.
$$
Then $\{X'_{i'}\}$ is a semialgebraic (not necessarily Whitney) $C^1$ stratification of $\overline X$; $\{X'_{i'}\cap X\}$ is a substratification of $\{X_i\}$; $\overline f:\{X'_{i'}\}\to\{Y'_{j'}\}$ is a $C^1$ stratification of $\overline f$; we can choose $\{Y'_{j'}\}$ so that for each $Y'_{j'}$, $\{X'_{i'}:\overline f(X'_{i'})=Y'_{j'}\}$ is a Whitney $C^1$ stratification for the following reason. \par
  Assume $Y'_{j'}\not\subset\overline f(Z)$.
Then $Y'_{j'}\cap\overline f(Z)=\emptyset$ and there is $Y_j$ including $Y'_{j'}$.
By definition of $\{X'_{i'}\}$,
$$
\{X'_{i'}:\overline f(X'_{i'})=Y'_{j'}\}=\{X_i\cap f^{-1}(Y'_{j'})\}.
$$
Therefore the assertion follows from the fact that given a Whitney $C^r$ stratification $\{M_1,M_2\}$, a $C^r$ map $g$ from $M_1\cup M_2$ to a $C^r$ manifold $N$ such that $g|_{M_1}$ and $g|_{M_2}$ are $C^r$ submersions into $N$ and a $C^r$ submanifold $N_1$ of $N$ then $\{M_1\cap g^{-1}(N_1),M_2\cap g^{-1}(N_1)\}$ is a Whitney $C^r$ stratification. \par
  Next assume $Y'_{j'}\subset\overline f(Z)$, and let $X'_{i'_1}$ and $X'_{i'_2}$ be such that $\overline f(X'_{i'_k})=Y'_{j'},\ k=1,2$, and $(\overline{X'_{i'_1}}-X'_{i'_1})\cap X'_{i'_2}\not=\emptyset$.
Then we need to see $(X'_{i'_1},X'_{i'_2})$ can satisfy the Whitney condition.
Since $\overline f|_Z$ is injective, there are only two possible cases to consider: $X'_{i'_k}=X_{i_k}\cap\overline f^{-1}(Y'_{j'}),\ k=1,2$, for some $i_1$ and $i_2$ or $X'_{i'_1}=X_{i_1}\cap\overline f^{-1}(Y'_{j'})$ and $X'_{i'_2}=\{0\}\times Y'_{j'}$.
In the former case there is $j$ such that $Y'_{j'}\subset Y_j$.
Hence the Whitney condition is satisfied by the same reason as in the case of $Y'_{j'}\not\subset\overline f(Z)$.
Consider the latter case.
If $\{X'_{i'_1},\{0\}\times Y'_{j'}\}$ is not a Whitney stratification, let $Y''_{j'}$ denote the subset of $Y'_{j'}$ consisting of $y$ such that $(X'_{i_1},\{0\}\times Y'_{j'})$ does not satisfy the Whitney condition at $(0,y)$.
Then $Y''_{j'}$ and hence $\overline{Y''_{j'}}$ are semialgebraic and of dimension smaller that $\dim Y'_{j'}$.
Divide $Y'_{j'}$ to $\{Y'_{j'}-\overline{Y''_{j'}},\overline{Y''_{j'}}\}$ and substratify $\{Y'_{j'}\cap\overline f(Z)\}$ by downward induction on dimension of $Y'_{j'}$ so that the above conditions on $\{Y'_{j'}\}$ are kept and $Y''_{j'}=\emptyset$.
Then $\{X'_{i'_1},\{0\}\times Y'_{j'}\}$ becomes a Whitney stratification. \par
  Now we define a controlled semialgebraic $C^1$ tube system $\{T_{j'}^{Y\prime}=(|T_{j'}^{Y\prime}|,\pi_{j'}^{Y\prime},\rho_{j'}^{Y\prime})\}$ for $\{Y'_{j'}\}$.
For simplicity of notation, assume $\dim Y_j=j$ gathering strata of the same dimension.
For each $j$, set
$$
J_j=\left\{
\begin{array}{ll}
\{j':Y'_{j'}\subset Y_j,\}\quad&\text{if}\ j\ge0,\\
\emptyset\quad&\text{if}\ j=-1. \\
\end{array}
\right.
$$
We define $\{T_{j'}^{Y\prime}:j'\in J_j\}$ by induction on $j$.
Fix a non-negative integer $j_0$, and assume we have constructed a controlled semialgebraic $C^1$ tube system $\{T_{j'}^{Y\prime}:j'\in J_j,j<j_0\}$ so that $T_{j'}^{Y\prime}=T_{j_1}^Y|_{|T_{j'}^{Y\prime}|}$ for $j'\in J_{j_1},\ j_1<j_0$, with $\dim Y'_{j'}=j_1$,
$$
\pi_{j'}^{Y\prime}\circ\pi_j^Y=\pi_{j'}^{Y\prime}\quad\text{on}\ |T_{j'}^{Y\prime}|\cap|T_j^Y|\ \text{for}\ j'\ \text{and}\ j\ \text{with}\ Y'_{j'}\subset\overline{Y_j},\leqno{(*)_Y}
$$
$$
\rho_{j'}^{Y\prime}\circ\pi_j^Y=\rho_{j'}^{Y\prime}\quad\text{on}\ |T_{j'}^{Y\prime}|\cap|T_j^Y|\ \text{for}\ j'\in J_{j_1}\ \text{and}\ j\ \text{with}\ j_1<j,\leqno{(**)_Y}
$$
$\pi_{j'}^{Y\prime}$ are of class $C^1$ and $\rho_{j'}^{Y\prime}$ are of class $C^1$ on $|T_{j'}^{Y\prime}|-Y'_{j'}$.
For the conditions of the first and $(**)_Y$ we need to proceed in the $C^1$ category because there does not necessarily exist such $\{T_{j'}^{Y\prime}\}$ of class $C^2$ even if $\{T_j^Y\}$ is of class $C^2$. \par
  We wil define a semialgebraic $C^1$ tube system $\{T_{j'}^{Y\prime}:j'\in J_{j_0}\}$ for $\{Y'_{j'}:j'\in J_{j_0}\}$.
For the time being, let $\{T_{j'}^{Y\prime}:j'\in J_{j_0}\}$ be a semialgebraic $C^1$ tube system for $\{Y'_{j'}:j'\in J_{j_0}\}$ such that $\{T_{j'}^{Y\prime}:j'\in J_j,j\le j_0\}$ is controlled (Lemma II.6.10, \cite{S2} states only the case where $\cup_{j'\in J_{j_0}}Y'_{j'}$ is compact but its proof works in the general case.
We omit the details.)
We modify $\{T_{j'}^{Y\prime}:j'\in J_{j_0}\}$ so that the conditions are satisfied.
Let $j'\in J_{j_0}$. \par
  Restrict $\pi_{j'}^{Y\prime}$ and $\rho_{j'}^{Y\prime}$ to $Y_{j_0}$ for $j'\in J_{j_0}$ and define afresh them outside of $Y_{j_0}$ as follows.
Let $\pi_{j'}^{Y\prime}$ and $\rho_{j'}^{Y\prime}$, $j'\in J_{j_0}$, now denote the restrictions.
If $\dim Y'_{j'}=j_0$, we should set $T_{j'}^{Y\prime}=T_{j_0}^Y|_{|T_{j'}^{Y\prime}|}$.
Then $(*)_Y$ and $(**)_Y$ are satisfied because $\{Y_j^Y\}$ is controlled.
Assume $\dim Y'_{j'}<j_0$ and hence $j_0>0$.
In this case, define the extension of $\pi_{j'}^{Y\prime}$ to $|T_{j'}^{Y\prime}|$ to be $\pi_{j'}^{Y\prime}\circ\pi_{j_0}^Y$, and keep the same notation $\pi_{j'}^{Y\prime}$ for the extension.
Then by controlledness of $\{T_j^Y\}$, $(*)_Y$ holds for any $j$ with $Y'_{j'}\subset\overline{Y_J}$.
The problem is how to extend $\rho_{j'}^{Y\prime}$. \par
  As the problem is local at $Y'_{j'}$ (see II.1.1, [4]), considering semialgebraic tubular neighborhoods of $Y'_{j'}$ and $Y_{j_0}$ we can assume for each $y\in Y'_{j'}$, $\pi_{j'}^{Y\prime-1}(y),\ \pi_{j'}^{Y\prime-1}(y)\cap Y_{j_0}$ and $\pi_{j_0}^{Y-1}(y)$ are of the form $y+L_y,\ y+L_{0,y}$ and $y+L_{0,y}^\perp$, where $L_y$ and $L_{0,y}$ are linear subspaces of $\R^n$ with $L_y\supset L_{0,y}$ and $L_{0,y}^\perp$ is the orthocomplement of $L_{0,y}$ with respect to $L_y$, and $\pi_{j_0}^Y|_{\pi_{j'}^{Y\prime-1}(y)}:\pi_{j'}^{Y\prime-1}(y)\longrightarrow\pi_{j'}^{Y\prime-1}(y)\cap Y_{j_0}$ is induced by the orthogonal projection of $L_y$ to $L_{0,y}$ and
$$
  \rho_{j_0}^Y(y+z_1+z_2)=|z_2|^2\ \text{for}\ (y,z_1,z_2)\in Y'_{j'}\times L_{0,y}\times L_{0,y}^\perp,
$$
where $Y'_{j'}\times L_{0,y}\times L_{0,y}^\perp$ denotes $\cup_{y\in Y'_{j'}}\{y\}\times L_{0,y}\times L_{0,y}^\perp$.
$$
\rho_{j'}^{Y\prime\prime}(y+z_1+z_2)=|z_1|^2+|z_2|^2\quad\text{for}\ (y,z_1,z_2)\in Y'_{j'}\times L_{0,y}\times L_{0,y}^\perp. \leqno{\text{Set}}
$$
Then $(|T_{j'}^{Y\prime}|,\pi_{j'}^{Y\prime},\rho_{j'}^{Y\prime\prime})$ is a semialgebraic $C^1$ tube at $Y'_{j'}$ but not always satisfy the condition $\rho_{j'}^{Y\prime\prime}\circ\pi_{j_0}^Y=\rho_{j'}^{Y\prime\prime}$.
We need to modify $\rho_{j'}^{Y\prime\prime}$ so that the equality holds on a neighborhood of $Y_{j_0}-Y'_{j'}$.
Let $\xi$ be a semialgebraic $C^1$ function on $\R$ such that $\xi=1$ on $(-\infty,\,1],\ \xi=0$ on $[2,\infty)$ and $d\xi/d t\le0$.
Set
$$
\eta_{j'}(z_1,z_2)=\left\{
\begin{array}{ll}
\xi(\frac{|z_2|}{|z_1|^2})\frac{|z_1|}{(|z_1|^2+|z_2|^2)^{1/2}}+1-\xi(\frac{|z_2|}{|z_1|^2})\, &\text{for}\ (z_1,z_2)\in(L_{0,y}-\{0\})\times L_{0,y}^\perp,\\
1\ &\text{for}\ (z_1,z_2)\in\{0\}\times L_{0,y}^\perp,\\
\end{array}
\right.
$$
and define a semialgebraic map $\tau_{j'}$ between $|T_{j'}^{Y\prime}|$ by
$$
\tau_{j'}(y+z_1+z_2)=y+\eta_{j'}(z_1,z_2)z_1+\eta_{j'}(z_1,z_2)z_2\quad\text{for}\ (y,z_1,z_2)\in Y'_{j'}\times L_{0,y}\times L_{0,y}^\perp.
$$\par
  Then $\pi_{j'}^{Y\prime}\circ\tau_{j'}=\pi_{j'}^{Y\prime}$;
$$
\tau_{j'}=\id\quad\text{on}\ \{y+z_1+z_2:|z_2|\ge2|z_1|^2\};
$$
$$
\tau_{j'}(y+z_1+z_2)=y+\frac{|z_1|}{(|z_1|^2+|z_2|^2)^{1/2}}z_1+\frac{|z_1|}{(|z_1|^2+|z_2|^2)^{1/2}}z_2\qquad\qquad\qquad
$$
$$\qquad\qquad\qquad\qquad\quad\text{for}\ (y,z_1,z_2)\in Y'_{j'}\times L_{0,y}\times L_{0,y}^\perp\ \text{with}\ |z_2|\le|z_1|^2;
$$
$$
\rho_{j'}^{Y\prime\prime}\circ\tau_{j'}(y+z_1+z_2)=|z_1|^2\quad\text{for the same}\ (y,z_1,z_2); \leqno{(***)_Y}
$$
for each line $l$ in $\{y\}\times L_{0,y}\times L_{0,y}^\perp$ passing through 0 parameterized by $t\in\R$ as $z_1=z_1(t)$ and $z_2=z_2(t)$ so that $|z_1(t)|=|t|$ and $|z_2(t)|=a|t|$ for $a\ge 0\in\R$,
$$
\tau_{j'}(l)=l,
$$
$$
|\tau_{j'}(y+z_1(t)+z_2(t))-y|=\eta_{j'}(z_1(t),z_2(t))(|z_1(t)|^2+|z_2(t)|^2)^{1/2}\quad\qquad\qquad
$$
$$
\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad=\xi(\frac{a}{|t|})|t|+(1-\xi(\frac{a}{|t|}))(1+a^2)^{1/2}|t|,
$$
hence by easy calculations we see if $a$ is sufficiently small then $\tau_{j'}|_l$ is a $C^1$ diffeomorphism of $l$ and, therefore by the above equality $\tau_{j'}=\id$ on $\{|z_2|\ge 2|z_1|^2\}$ shrinking $|T_{j'}^{Y\prime}|$ we can assume $\tau_{j'}$ is a homeomorphism and its restriction to $|T_{j'}^{Y\prime}|-Y'_{j'}$ is a $C^1$ diffeomorphism;
moreover, if we set $\rho_{j'}^{Y\prime}=\rho_{j'}^{Y\prime\prime}\circ\tau_{j'}$ and $T_{j'}^{Y\prime}=(|T_{j'}^{Y\prime}|,\pi_{j'}^{Y\prime},\rho_{j'}^{Y\prime})$ for all $j'\in J_{j_0}$ with $\dim Y'_{j'}<j_0$ then $\{T_{j'_1}^{Y\prime}:j'_1\in J_{j_1},j_1\le j_0\}$ is a controlled semialgebraic $C^1$ tube system.
Indeed, for $j'_1\in J_{j_0}$ and $j'_2$ with $(\overline{Y'_{j'_1}}-Y'_{j'_1})\cap Y'_{j'_2}\not=\emptyset$, the following equalities folds on $|T_{j'_1}^{Y\prime}|\cap|T_{j'_2}^{Y\prime}|$
$$
\pi_{j'_2}^{Y\prime}\circ\pi_{j'_1}^{Y\prime}=\pi_{j'_2}^{Y\prime}\circ\pi_{j'_1}^{Y\prime}\circ\pi_{j_0}^Y\quad\text{by definition of}\ \pi_{j'_1}^{Y\prime}\qquad\qquad\quad
$$
$$
=\pi_{j'_2}^{Y\prime}\circ\pi_{j_0}^Y\quad\text{by controlledness of}\ \{T_{j'}^{Y\prime}|_{Y_{j_0}}:j'\in J_j,\,j\le j_0\}
$$
$$
=\pi_{j'_2}^{Y\prime}\ \text{by definition of}\ \pi_{j'_2}^{Y\prime}\ \text{in the case of }j'_2\in J_{j_0}\text{ and by }(*)_Y\text{ in the other case}.
$$
In the same way we see by $(**)_Y$ and $(***)_Y$
$$
\rho_{j'_2}^{Y\prime}\circ\pi_{j'_1}^{Y\prime}=\rho_{j'_2}^{Y\prime}\quad\text{on}\ |T_{j'_1}^{Y\prime}|\cap|T_{j'_2}^{Y\prime}|.
$$
Hence it remains to show $\tau_{j'}$ is a $C^1$ diffeomorphism. \par
  It is easy to show $\tau_{j'}$ is differentiable at $Y'_{j'}$ and its differential $d\tau_{j'a}$ at each point $a$ of $Y'_{j'}$ is equal to the identity map.
Hence we only need to show the map $|T_{j'}^{Y\prime}|\ni a\to d\tau_{j'a}\in GL(\R^n)$ is of class $C^0$.
As the problem is local at each point of $Y'_{j'}$ we suppose
$$
Y'_{j'}=\R^{n'}\times\{0\}\times\{0\},\ Y_{j_0}=\R^{n'}\times\R^{n_1}\times\{0\},\ |T_{j'}^{Y\prime}|=|T_{j_0}^Y|=\R^{n'}\times\R^{n_1}\times\R^{n_2}
$$
and $\pi_{j_0}^Y$ and $\pi_{j'}^{Y\prime}$ are the projections of $\R^{n'}\times\R^{n_1}\times\R^{n_2}$ to $\R^{n'}\times\R^{n_1}\times\{0\}$ and $\R^{n'}\times\{0\}\times\{0\}$ respectively.
Then it suffices to see the differential at $(z_{01},z_{02})$ of the map $\R^{n_1}\times\R^{n_2}\ni(z_1,z_2)\to(\eta_{j'}(z_1,z_2)z_1,\eta_{j'}(z_1,z_2)z_2)\in\R^{n_1}\times\R^{n_2}$ converges to the identity map as $(z_{01},z_{02})\to(0,0)$.
That is,
$$
\aligned
&d\left(\frac{\xi(\frac{|z_2|}{|z_1|^2})((|z_1|^2+|z_2|^2)^{1/2}-|z_1|)z_i}{(|z_1|^2+|z_2|^2)^{1/2}}\right)_{(z_{01},z_{02})}=\\
&d\left(\frac{\xi(\frac{|z_2|}{|z_1|^2})|z_2|^2z_i}{(|z_1|^2+|z_2|^2)^{1/2}((|z_1|^2+|z_2|^2)^{1/2}+|z_1|)}\right)_{(z_{01},z_{02})}\longrightarrow 0
\endaligned
$$
as $(z_{01},z_{02})\to(0,0)$ with $|z_2|\le2|z_1|^2,\ i=1,2,$ since $\eta_{j'}(z_1,z_2)=1$ for $(z_1,z_2)$ with $|z_2|\ge2|z_1|^2$.
That is easy to check.
We omit the details. \par
  Thus we obtain semialgebraic $C^1$ tubes $T_{j'}^{Y\prime}$ for all $j'\in J_{j_0}$.
The other requirements in the induction hypothesis are satisfied as follows.
By definition of $T_{j'}^{Y\prime}$,
$$
T_{j'}^{Y\prime}=T_{j_0}^Y|_{|T_{j'}^{Y\prime}|}\quad\text{for}\ j'\in J_{j_0}\ \text{with}\ \dim Y'_{j'}=j_0;
$$ by controlledness of $\{T_j^Y\}$ and by definition of $T_{j'}^{Y\prime}$, for $j'$ and $j$ with $Y'_{j'}\subset\overline{Y_j},\ j'\in J_{j_0}$ and $j\ge j_0$,
$$
\pi_{j'}^{Y\prime}\circ\pi_j^Y=\pi_{j'}^{Y\prime}\circ\pi_{j_0}^Y\circ\pi_j^Y=\pi_{j'}^{Y\prime}\circ\pi_{j_0}^Y=\pi_{j'}^{Y\prime}\quad\text{on}\ |T_{j'}^{Y\prime}|\cap|T_j^Y|;\leqno{(*)_Y}
$$
$(**)_Y$ holds for $j'$ and $j$ with $j'\in J_{j_0}$ and $j>j_0$ for the following reason. \par
  That is clear if $\dim Y'_{j'}=j_0$.
Hence assume $\dim Y'_{j'}<j_0$ and use the above coordinate system $Y'_{j'}\times L_{0,y}\times L_{0,y}^\perp$.
Then
$$
\rho_{j'}^{Y\prime}(y+z_1+z_2)\!=\!\rho_{j'}^{Y\prime\prime}\circ\tau_{j'}(y+z_1+z_2)\!=\!\eta_{j'}^2(z_1,z_2)(|z_1|^2+|z_2|^2)\qquad
$$
$$
\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\text{for }(y,z_1,z_2)\in Y'_{j'}\times L_{0,y}\times L_{0,y}^\perp
$$
and $\eta_{j'}(z_1,z_2)$ depends on only $|z_1|$ and $|z_2|$.
Hence if we set
$$
\pi_j^Y(y+z_1+z_2)=\pi_{j1}^Y(y+z_1+z_2)+\pi_{j2}^Y(y+z_1+z_2)+\pi_{j3}^Y(y+z_1+z_2),
$$
$$
\pi_{j1}^Y(y+z_1+z_2)\in Y'_{j'},\ \pi_{j2}^Y(y+z_1+z_2)\in L_{0,y},\ \pi_{j3}^Y(y+z_1+z_2)\in L_{0,y}^\perp.
$$
then it suffices to see
$$
\pi_{j2}^Y(y+z_1+z_2)=z_1\quad\text{and}\quad|\pi_{j3}^Y(y+z_1+z_2)|=|z_2|.
$$
By controlledness of $\{T_j^Y\}$ we have $\pi_{j_0}^Y\circ\pi_j^Y=\pi_{j_0}^Y$.
Hence by the equation $\pi_{j_0}^Y(y+z_1+z_2)=y+z_1$, the former equality holds.
The latter also follows from the equations $\rho_{j_0}^Y\circ\pi_j^Y=\rho_{j_0}^Y$ and $\rho_{j_0}^Y(y+z_1+z_2)=|z_2|^2$. \par
  Hence by induction we have a controlled semialgebraic $C^1$ tube system $\{T_{j'}^{Y\prime}\}$ for $\{Y'_{j'}\}$ such that $T_{j'}^{Y\prime}=T_j^Y|_{|T_{j'}^{Y\prime}|}$ for $j'\in J_j$ with $\dim Y'_{j'}=j$, $(*)_Y$ for $j'$ and $j$ with $Y'_{j'}\subset\overline{Y_j}$ and $(**)_Y$ for $j'\in J_{j_1}$ and $j$ with $j_1<j$. \par
  Next we define $\{T_{i'}^{X\prime}\}$ by induction as $\{T_{j'}^{Y\prime}\}$.
Consider all $X'_{i'}$ included in $X$ and forget $X'_{i'}$ outside of $X$.
We change the set of indexes of $X_i$.
For non-negative integers $i_0$ and $j_0$, let $X_{i_0,j_0}$ denote the union of $X_i$'s such that $\dim X_i=i_0$ and $f(X_i)\subset Y_{j_0}$, i.e., $\dim f(X_i)=j_0$, naturally define $T_{i,j}^X=(|T_{i,j}^X|,\pi_{i,j}^X,\rho_{i,j}^X)$ and continue to define $\{X'_{i'}\}$ to be $\{X_{i,j}\cap p^{-1}(Y'_{j'}),Z\cap\{0\}\times Y'_{j'}\}$.
Then $\dim X_{i,j}=i$ and $f|_{X_{i,j}}$ is a map to $Y_j$.
Let $I_i$ denote the set of indexes of $X'_{i'}$ such that $X'_{i'}$ is included in $X_{i,j}$ for some $j$.
Note $X=\cup\{X'_{i'}:i'\in I_i$ for some $i\}$.
Fix a non-negative integer $i_0$, and assume there exists a semialgebraic $C^1$ tube system $\{T_{i'}^{X\prime}=(|T_{i'}^{X\prime}|,\pi_{i'}^{X\prime},\rho_{i'}^{X\prime}):i'\in I_i,\ i<i_0\}$ for $\{X'_{i'}:i'\in I_i,\ i<i_0\}$ such that the following four conditions are satisfied, which are, except (iv), similar to the conditions (1), (2) and (3) in section 2. \par\noindent
(i) For $i,\ i'$ and $j'$ with $i<i_0,\ i'\in I_i$ and $f(X'_{i'})=Y'_{j'}$,
$$
f\circ\pi_{i'}^{X\prime}=\pi_{j'}^{Y\prime}\circ p\quad\text{on}\ |T_{i'}^{X\prime}|\cap p^{-1}(|T_{j'}^{Y\prime}|).
$$
(ii) For each $j'$, $\{T_{i'}^{X\prime}:f(X'_{i'})=Y'_{j'},\ i'\in I_i,\ i<i_0\}$ is a controlled semialgebraic $C^1$ tube system for $\{X'_{i'}:f(X'_{i'})=Y'_{j'},\ i'\in I_i,\ i<i_0\}$. \par\noindent
(iii) For $i_k,\,i'_k,\ k=1,2,3,\ i_4$ and $j_4$ with $i_k<i_0,\ i'_k\in I_{i_k},\ k=1,2,3$, $X'_{i'_1}\cap(\overline{X'_{i'_2}}-X'_{i'_2})\not=\emptyset$ and $X'_{i'_3}\subset\overline{X_{i_4,j_4}}$,
$$
\pi_{i'_1}^{X\prime}\circ\pi_{i'_2}^{X\prime}=\pi_{i'_1}^{X\prime}\quad\text{on}\ |T_{i'_1}^{X\prime}|\cap|T_{i'_2}^{X\prime}|,
$$
$$
\pi_{i'_3}^{X\prime}\circ\pi_{i_4,j_4}^X=\pi_{i'_3}^{X\prime}\quad\text{on}\ |T_{i'_3}^{X\prime}|\cap|T_{i_4,j_4}^X|,
$$
if $i_3<i_4$ moreover, then
$$
\rho_{i'_3}^{X\prime}\circ\pi_{i_4,j_4}^X=\rho_{i'_3}^{X\prime}\quad\text{on}\ |T_{i'_3}^{X\prime}|\cap|T_{i_4,j_4}^X|.
$$
(iv) For $i,\ i'$ and $j$ with $i<i_0,\ i'\in I_i$ and $\dim X'_{i'}=i$,
$$
T_{i'}^{X\prime}=T_{i,j}^X|_{|T_{i'}^{X\prime}|}.
$$\par
  Then we need to define $\{T_{i'}^{X\prime}:i'\in I_{i_0}\}$ so that the induction process works.
Before that we note a fact. \par\noindent
(v) Given $i_k,\,i'_k,\,j'_k,\ k=1,2$, with $i_k<i_0,\ i'_k\in I_{i_k},\ k=1,2,\ X'_{i'_1}\cap(\overline{X'_{i'_2}}-X'_{i'_2})\not=\emptyset$, $Y'_{j'_1}\subset\overline{Y'_{j'_2}}-Y'_{j'_2}$ and $f(X'_{i'_k})=Y'_{j'_k},\ k=1,2$, then the restriction of the map $(\pi_{i'_1}^{X\prime},f)$ to $X'_{i'_2}\cap|T_{i'_1}^{X\prime}|$ is a $C^1$ submersion into the fiber product $X'_{i'_1}\times_{(f,\pi_{j'_1}^{Y\prime})}(Y'_{j'_2}\cap|T_{j'_1}^{Y\prime}|)$. \par
The reason is the following. \par
  Case where $X'_{i'_k}\subset X_{i_k,j_k},\ k=1,2$, for some $j_1\not=j_2$.
The condition (4) in section 2 is shown to be equivalent to $(4)'$.
Now also similar equivalence holds.
Hence it suffices to see for each $x\in X'_{i'_2}\cap|T_{i'_1}^{X\prime}|$, the germ of $\pi_{i'_1}^{X\prime}|_{X'_{i'_2}\cap f^{-1}(f(x))}$ at $x$ is a $C^1$ submersion onto the germ of $X'_{i'_1}\cap f^{-1}(\pi_{j'_1}^{Y\prime}\circ f(x))$ at $\pi_{i'_1}^{X\prime}(x)$.
We have four properties.
$$
X'_{i'_2}\cap f^{-1}(f(x))=X_{i_2,j_2}\cap f^{-1}(f(x))\quad\text{by definition of }\{X'_{i'}\};
$$
$$
X'_{i'_1}\cap f^{-1}(\pi_{j'_1}^{Y\prime}\circ f(x))=X'_{i'_1}\cap f^{-1}(f\circ\pi_{i'_1}^{X\prime}(x))\quad\text{by (i)}
$$
$$
=X_{i_1,j_1}\cap f^{-1}(f\circ\pi_{i'_1}^{X\prime}(x))\quad\text{by definition of }\{X'_{i'}\};
$$
by $(4)'$ the germ of $\pi_{i_1,j_1}^X|_{X_{i_2,j_2}\cap f^{-1}(f(x))}$ at $x$ is a $C^1$ submersion onto the germ of $X_{i_1,j_1}\cap f^{-1}(f\circ\pi_{i_1,j_1}^X(x))$ at $\pi_{i_1,j_1}^X(x)$; by (iii)
$$
\pi_{i'_1}^{X\prime}\circ\pi_{i_1,j_1}^X=\pi_{i'_1}^{X\prime}\quad\text{on}\ |T_{i'_1}^{X\prime}|\cap|T_{i_1,j_1}^X|.
$$
Hence we only need to see the germ of $\pi_{i'_1}^{X\prime}|_{X_{i_1,j_1}\cap f^{-1}(f\circ\pi_{i_1,j_1}^X(x))}$ at $\pi_{i_1,j_1}^X(x)$ is a $C^1$ submersion onto the germ of $X'_{i'_1}\cap f^{-1}(f\circ\pi_{i'_1}^{X\prime}(x))$ at $\pi_{i'_1}^{X\prime}(x)$.
That is clear by (i) because $f|_{X_{i_1,j_1}}:X_{i_1,j_1}\to Y_{j_1}$ is a $C^1$ submersion onto a union of some connected components of $Y_{j_1}$ and $f\circ\pi_{i_1,j_1}^X(x)$ and $f\circ\pi_{i'_1}^{X\prime}(x)$ are contained in the same connected component. \par
  Note we use the hypothesis $X'_{i'_k}\subset X_{i_k,j_k},\ k=1,2$, $j_1\not=j_2$ in the above arguments for only the property that the germ of $\pi_{i_1,j_1}^X|_{X_{i_2,j_2}\cap f^{-1}(f(x))}$ is a $C^1$ submersion into $X_{i_1,j_1}\cap f^{-1}(f\circ\pi_{i_1,j_1}^X(x))$. \par
  Case where $i_1\not=i_2$ and $X'_{i'_k}\subset X_{i_k,j_k},\ k=1,2$, for some $j_1$.
In this case also the above property holds because $f\circ\pi_{i_1,j_1}^X=f$ on $X_{i_2,j_1}\cap|T_{i_1,j_1}^X|$ and $\pi_{i_1,j_1}^X|_{X_{i_2,j_1}\cap|T_{i_1,j_1}^X|}$ is a $C^1$ submersion into $X_{i_1,j_1}$. \par
  Case where $i_1=i_2$ and hence $X'_{i'_k}\subset X_{i_1,j_1},\ k=1,2$, for some $j_1$.
In this case the reason is simply $\pi_{i_1.j_1}^X|_{X_{i_1,j_1}}=\id$. \par
  Thus (v) is proved.
Now we define $\{T_{i'}^{X\prime}:i'\in I_{i_0}\}$.
For that it suffices to consider separately $\{X'_{i'}:X'_{i'}\subset X_{i_0,j}\}$ for each $j$.
Hence we assume all $X'_{i'}$ with $i'\in I_{i_0}$ are included in one $X_{i_0.j_0}$ for some $j_0$ and, moreover, $f(X_{i_0,j_0})=Y_{j_0}$ for simplicity of notation.
Then as shown below we have a semialgebraic $C^1$ tube system $\{T_{i'}^{X\prime}=(|T_{i'}^{X\prime}|,\pi_{i'}^{X\prime},\rho_{i'}^{X\prime}):i'\in I_0\}$ for $\{X'_{i'}:i'\in I_0\}$ such that\par\noindent
(vi) for $i'$ and $j'$ with $i'\in I_{i_0}$ and $f(X'_{i'})=Y'_{j'}$,
$$
f\circ\pi_{i'}^{X\prime}=\pi_{j'}^{Y\prime}\circ p\quad\text{on}\ |T_{i'}^{X\prime}|\cap p^{-1}(|T_{j'}^{Y\prime}|);
$$
(vii) for $j'\in J_{j_0},$ $\{T_{i'}^{X\prime}:f(X'_{i'})=Y'_{j'},\,i'\in I_{i_1},\,i_1\le i_0\}$ is a controlled semialgebraic $C^1$ tube system for $\{X'_{i'}:f(X'_{i'})=Y'_{j'},\,i'\in I_{i_1},\,i_1\le i_0\}$;\par\noindent
(viii) for $i_1,\,i'_k,\,k=1,2,3,\,i_4$ and $j_4$ with $i_1\le i_0,\,i'_1\in I_{i_1},\,i'_2,i'_3\in I_{i_0},\ X'_{i'_1}\cap(\overline{X'_{i'_2}}-X'_{i_2})\not=\emptyset$ and $X'_{i'_3}\subset\overline{X_{i_4,j_4}}$,
$$
\pi_{i'_1}^{X\prime}\circ\pi_{i'_2}^{X\prime}=\pi_{i'_1}^{X\prime}\quad\text{on}\ |T_{i'_1}^{X\prime}|\cap|T_{i'_2}^{X\prime}|,
$$
$$
\pi_{i'_3}^{X\prime}\circ\pi_{i_4,j_4}^X=\pi_{i'_3}^{X\prime}\quad\text{on}\ |T_{i'_3}^{X\prime}|\cap|T_{i_4,j_4}^X|,
$$
if $i_0<i_4$ then
$$
\rho_{i'_3}^{X\prime}\circ\pi_{i_4,j_4}^X=\rho_{i'_3}^{X\prime}\quad\text{on}\ |T_{i'_3}^{X\prime}|\cap|T_{i_4,j_4}^X|;
$$
(ix) for $i'\in I_{i_0}$ with $\dim X'_{i'}=i_0$,
$$
T_{i'}^{X\prime}=T_{i_0,j_0}^X|_{|T_{i'}^{X\prime}|}.
$$\par
  We construct $\{T_{i'}^{X\prime}:i'\in I_0\}$ as follows.
First we define $T_{i'}^{X\prime}$ on $|T_{i'}^{X\prime}|\cap X_{i_0,j_0}$, $i'\in I_{i_0}$, so that (vi), (vii) and the first equality in (viii) are satisfied by the usual arguments of lift of a tube system (see [1], Lemma II.6.1, [4] and its proof).
Secondly, extend $\pi_{i'}^{X\prime}$ to $|T_{i'}^{X\prime}|$ using $\pi_{i_0,j_0}^X$ as in the above construction of $\pi_{j'}^{Y\prime}$.
Then $\pi_{i'}^{X\prime}$ are of class $C^1$; (vi) holds because for $i'$ and $j'$ with $i'\in I_{i_0}$ and $f(X'_{i'})=Y'_{j'}$,
$$
f\circ\pi_{i'}^{X\prime}\overset{\text{definition of }\pi_{i'}^{X\prime}}=f\circ\pi_{i'}^{X\prime}\circ\pi_{i_0,j_0}^X\overset{\text{(vi) on }|T_{i'}^{X\prime}|\cap X_{i_0,j_0}}=\pi_{j'}^{Y\prime}\circ f\circ\pi_{i_0,j_0}^X
$$
$$
\overset{\text{(1) in section 2}}=\pi_{j'}^{Y\prime}\circ\pi_{j_0}^Y\circ p\overset{(**)_Y}=\pi_{j'}^{Y\prime}\circ p\quad\text{on}\ |T_{i'}^{X\prime}|\cap p^{-1}(|T_{j'}^{Y\prime}|);
$$
the first equality in (viii) for $i_1=i_0$ follows from definition of the extension; that for $i_1<i_0$ does from the second equality in (iii); the second in (viii) does from definition of the extension and the equality $\pi_{i_0,j_0}^X\circ\pi_{i_4,j_4}^X=\pi_{i_0,j_0}^X$; trivially $\pi_{i'}^{X\prime}=\pi_{i_0,j_0}^X$ for $i'\in I_{i_0}$ with $\dim X'_{i'}=i_0$.
Thirdly, extend $\rho_{i'}^{X\prime}$ to $|T_{i'}^{X\prime}|$ in the same way as $\rho_{j'}^{Y\prime}$.
Then $\{T_{i'}^{X\prime}:i'\in I_{i_0}\}$ is a semialgebraic $C^1$ tube system for $\{X'_{i'}:i'\in I_{i_0}\}$; (vii) holds because for $i'_0$ and $i'_1\in I_{i_1}$ with $i'_0\in I_{i_0},\ i_1<i_0$ and $f(X'_{i'_0})=f(X'_{i'_1})$,
$$
\rho_{i'_1}^{X\prime}\circ\pi_{i'_0}^{X\prime}=\rho_{i'_1}^{X\prime}\circ\pi_{i'_0}^{X\prime}\circ\pi_{i_0,j_0}^X\quad\text{by definition of }\pi_{i'_0}^{X\prime}
$$
$$
=\rho_{i'_1}^{X\prime}\circ\pi_{i_0,j_0}^X\quad\text{by (vii) on }X_{i_0,j_0}
$$
$$
=\rho_{i'_1}^{X\prime}\quad\text{by the third equality in (iii)};
$$
the extensions are chosen so that the third equality in (viii) and (ix) are satisfied, which completes construction of a semialgebraic $C^1$ tube system $\{T_{i'}^{X\prime}:i'\in I_{i_0}\}$ and hence by induction that of $\{T_{i'}^{X\prime}:X'_{i'}\subset X\}$ with (i), (ii), the first equality in (iii) and (v) for any $i_0$, i.e., controlled over $\{T_{j'}^{Y\prime}\}$. \par
  It remains only to consider $X'_{i'}$ in $Z$, i.e., the case where $X'_{i'}$ is of the form $\{0\}\times Y'_{j'}$ for some $j'$.
Set $\partial I=\{i':X'_{i'}\subset Z\}$.
Obviously, we set
$$
\pi_{i'}^{X\prime}(x)=(0,\pi_{j'}^{Y\prime}\circ p(x))\quad\text{for}\ x\in|T_{i'}^{X\prime}|,\ i'\in\partial I\ \text{and}\ j'\ \text{with}\ X'_{i'}=\{0\}\times Y'_{j'},
$$
where $|T_{i'}^{X\prime}|$ is a small semialgebraic neighborhood of $X'_{i'}$ in $\R^m\times\R^n$.
Then (i) for $i'\in\partial I$ is clear; the first equality in (iii) for $i'_1\in\partial I$ holds because
$$
\pi_{i'_1}^{X\prime}\circ\pi_{i'_2}^{X\prime}(x)\overset{\text{definition of }\pi_{i'_1}^{X\prime}}=(0,\pi_{j'_1}^{Y\prime}\circ p\circ\pi_{i'_2}^{X\prime}(x))\overset{\text{(i)}}=(0,\pi_{j'_1}^{Y\prime}\circ\pi_{j'_2}^{Y\prime}\circ p(x))
$$
$$
\overset{\text{controlledness of }\{T_{j'}^{Y\prime}\}}=(0,\pi_{j'_1}^{Y\prime}\circ p(x))=\pi_{i'_1}^{X\prime}(x)\quad\text{for}\ x\in|T_{i'_1}^{X\prime}|\cap|T_{i'_2}^{X\prime}|,
$$
where $j'_1$ and $j'_2$ are such that $f(X'_{i'_k})=Y'_{j'_k},\ k=1,2$; (v) for $i'_1\in\partial I$ is clear, to be precise, for $i'_1\in\partial I,\ i'_2,\ j'_1$ and $j'_2$ with $X'_{i'_1}\cap(\overline{X'_{i_2}}-X'_{i'_2})\not=\emptyset$, $Y'_{j'_1}\subset\overline{Y'_{j'_2}}-Y'_{j'_2}$ and $p(X'_{i'_k})=Y'_{j'_k},\ k=1,2$, the restriction of the map $(\pi_{i'_1}^{X\prime},p)$ to $X'_{i'_2}\cap|T_{i'_1}^{X\prime}|$ is a $C^1$ submersion into $X'_{i'_1}\times_{(p,\pi_{j'_1}^{Y\prime})}(Y'_{j'_2}\cap|T_{j'_1}^{Y\prime}|)$ because $p|_{X'_{i'_1}}:X'_{i'_1}\to Y'_{j'_1}$ is a $C^1$ diffeomorphism and $p|_{X'_{i'_2}}:X'_{i'_2}\to Y'_{j'_2}$ is a $C^1$ submersion. \par
  We want to define $\{\rho_{i'}^{X\prime}:i'\in\partial I\}$ so that $\{T_{i'}^{X\prime}=(|T_{i'}^{X\prime}|,\pi_{i'}^{X\prime},\rho_{i'}^{X\prime}):i'\in\partial I\}$ is a semialgebraic $C^1$ weak tube system and for each $j'$, $\{T_{i'}^{X\prime}:f(X'_{i'})=Y'_{j'}\}$ is controlled.
We proceed by double induction.
Let $d\ge 0\in\Z$, and assume $\rho_{i'}^{X\prime}$ are already defined if $\dim X'_{i'}>d$.
We need to construct $\rho_{i'}^{X\prime}$ for $i'\in\partial I$ with $\dim X'_{i'}=d$.
As the problem is local at such $X'_{i'}$, assume there exists only one $i'_0\in\partial I$ with $\dim X'_{i'_0}=d$.
Set $I'=\{i':X'_{i'_0}\subset\overline{X'_{i'}}-X'_{i'}\}$ and $Y'_{j'_0}=p(X'_{i'_0})$. \par
  For the moment we construct a non-negative semialgebraic $C^0$ function $\rho_{i'_0,d}^{X\prime}$ on $|T_{i'_0}^{X\prime}|$ with zero set $X'_{i'_0}$ which is of class $C^1$ on $|T_{i'_0}^{X\prime}|-X'_{i'_0}$ and such that $\{T_{i'_0,d}^{X\prime},T_{i'}^{X\prime}:i'\in I',\,p(X'_{i'})=Y'_{j'_0}\}$ is controlled, i.e.,
$$
\rho_{i'_0,d}^{X\prime}\circ\pi_{i'}^{X\prime}=\rho_{i'_0,d}^{X\prime}\quad\text{on}\ |T_{i'_0}^{X\prime}|\cap|T_{i'}^{X\prime}|\ \text{for}\ i'\in I'\ \text{with}\ p(X'_{i'})=Y'_{j'_0},
$$
where $d=1+\#I'$ and $T_{i'_0,d}^{X\prime}=(|T_{i'_0}^{X\prime}|,\pi_{i'_0}^{X\prime},\rho_{i'_0,d}^{X\prime})$.
(Namely we forget the condition that $\rho_{i'_0,d}^{X\prime}|_{X'_{i'}\cap\pi_{i'_0}^{X\prime-1}(x)-X'_{i'_0}}$ is $C^1$ regular for each $x$ and any $i'\in I'$.)
Order elements of $I'$ as $\{i'_1,...,i'_{d-1}\}$ so that $\dim X'_{i'_1}\le\cdots\le\dim X'_{i'_{d-1}}$. \par
  Let $k\in\Z$ with $0\le k<d-1$.
As the second induction, assume we have a non-negative semialgebraic $C^0$ function $\rho_{i'_0,k}^{X\prime}$ defined on $|T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_k}^{X\prime}|)$ such that $\rho_{i'_0,k}^{X\prime-1}(0)=X'_{i'_0},$ $\rho_{i'_0,k}^{X\prime}$ is of class $C^1$ outside of $X'_{i'_0}$ and $\{T_{i'_0,k}^{X\prime},T_{i'}^{X\prime}:i'\in I',\,p(X'_{i'})=Y'_{j'_0}\}$ is controlled, i.e.,
$$
\rho_{i'_0,k}^{X\prime}\circ\pi_{i'}^{X\prime}=\rho_{i'_0,k}^{X\prime}\quad\text{on}\ |T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_k}^{X\prime}|)\cap|T_{i'}^{X\prime}|\ \text{for}\ i'\in I'\ \text{with}\ p(X'_{i'})=Y'_{j'_0},
$$
where $T_{i'_0,k}^{X\prime}=(|T_{i'_0}^{X\prime}|,\pi_{i'_0}^{X\prime},\rho_{i'_0,k}^{X\prime})$.
Then we need to define $\rho_{i'_0,k+1}^{X\prime}$.
Let $\tilde\rho_{i'_0,k}^{X\prime}$ be any non-negative semialgebraic $C^0$ extension of $\rho_{i'_0,k}^{X\prime}|_{|T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_k}^{X\prime}|)\cap X'_{i'_{k+1}}}$ to $|T_{i'_0}^{X\prime}|\cap X'_{i'_{k+1}}$ with zero set $X'_{i'_0}$, let $V$ be an open semialgebraic neighborhood of $X'_{i'_1}\cup\cdots\cup X'_{i'_k}$ in $X'_{i'_1}\cup\cdots\cup X'_{i'_{k+1}}$ whose closure is included in $|T_{i'_1}^{X\prime}|\cup\cdots\cup |T_{i'_k}^{X\prime}|$, approximate $\tilde\rho_{i'_0,k}^{X\prime}|_{|T_{i'_0}^{X\prime}|\cap X'_{i'_{k+1}}-V}$ by a non-negative semialgebraic $C^0$ function $\Tilde{\Tilde\rho}_{i'_0,k}^{X\prime}$ in the uniform $C^0$ topology so that $\Tilde{\Tilde\rho}_{i'_0,k}^{X\prime-1}(0)=X'_{i'_0}$, and $\Tilde{\Tilde\rho}_{i'_0,k}^{X\prime}$ is of class $C^1$ outside of $X'_{i'_0}$ (Theorem II.4.1, [3]), let $\xi$ be a semialgebraic $C^1$ function on $|T_{i'_0}^{X\prime}|\cap X'_{i'_{k+1}}$ such that $0\le\xi\le 1$, $\xi=0$ on $|T_{i'_0}^{X\prime}|\cap X'_{i'_{k+1}}\cap V$ and $\xi=1$ on $|T_{i'_0}^{X\prime}|\cap X'_{i'_{k+1}}-|T_{i'_1}^{X\prime}|-\cdots|T_{i'_k}^{X\prime}|$, and set
$$
\hat\rho_{i'_0,k}^{X\prime}(x)=\xi(x)\Tilde{\Tilde\rho}_{i'_0,k}^{X\prime}(x)+(1-\xi(x))\rho_{i'_0,k}^{X\prime}(x)\quad\text{for }x\in|T_{i'_0}^{X\prime}|\cap X'_{i'_{k+1}}.
$$
Then $\hat\rho_{i'_0,k}^{X\prime}$ is a non-negative semialgebraic $C^0$ extension of $\rho_{i'_0,k}^{X\prime}|_{|T_{i'_0}^{X\prime}|\cap V\cap X'_{i'_{k+1}}}$ to $|T_{i'_0}^{X\prime}|\cap X'_{i'_{k+1}}$ with zero set $X'_{i'_0}$ and of class $C^1$ outside of $X'_{i'_0}$.
If $p(X'_{i'_{k+1}})\not=Y'_{j'_0}$, we continue to extend $\hat\rho_{i'_0,k}^{X\prime}$ to the required $\hat\rho_{i'_0,k+1}^{X\prime}:|T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_{k+1}}^{X\prime}|)\to\R$ shrinking $|T_{i'_1}^{X\prime}|,...,|T_{i'_k}^{X\prime}|$ and using a partition of unity in the same way so that $\rho_{i'_0,k+1}^{X\prime}=\rho_{i'_0,k}^{X\prime}$ on $|T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_k}^{X\prime}|)$.
Otherwise, set
$$
\rho_{i'_0,k+1}^{X\prime}=\left\{
\begin{array}{ll}
\rho_{i'_0,k}^{X\prime}\quad&\text{on}\ |T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_k}^{X\prime}|)\\
\hat\rho_{i'_0,k}^{X\prime}\circ\pi_{i'_0,k+1}^{X\prime}\quad&\text{on}\ |T_{i'_0}^{X\prime}|\cap|T_{i'_{k+1}}^{X\prime}|, \\
\end{array}
\right.
$$
which is well-defined because
$$
\hat\rho_{i'_0,k}^{X\prime}\circ\pi_{i'_0,k+1}^{X\prime}=\rho_{i'_0,k}^{X\prime}\circ\pi_{i'_0,k+1}^{X\prime}\quad\text{by definition of }\hat\rho_{i'_0,k}^{X\prime}\qquad\qquad\qquad\quad
$$
$$
=\rho_{i'_0,k}^{X\prime}\quad\text{by controlledness of }\{T_{i'_0,k}^{X\prime},T_{i'}^{X\prime}:i'\in I',\ p(X'_{i'})=Y'_{j'_0}\}\qquad
$$
$$
\qquad\qquad\text{on}\ |T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_k}^{X\prime}|)\cap|T_{i'_{k+1}}^{X\prime}|\text{ for shrunk }|T_{i'_1}^{X\prime}|,...,|T_{i'_k}^{X\prime}|.
$$
Then clearly $\rho_{i'_0,k+1}^{X\prime-1}(0)=X'_{i'_0},\ \rho_{i'_0,k+1}^{X\prime}$ is of class $C^1$ outside of $X'_{i'_0}$ and
$$
\rho_{i'_0,k+1}^{X\prime}\circ\pi_{i'}^{X\prime}=\rho_{i'_0,k+1}^{X\prime}\ \text{on}\ |T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i'_{k+1}}^{X\prime}|)\cap|T_{i'}^{X\prime}|\ \text{for}\ i'\in I'\ \text{with}\ p(X'_{i'})=Y'_{j'_0}
$$
as follows. It suffices to consider only the case where $\overline {X'_{i'}}-X'_{i'}\supset X'_{i'_{k+1}}$ and $p(X'_{i'})=p(X'_{i'_{k+1}})=Y'_{j'_0}$ and the equation on $|T_{i'_0}^{X\prime}|\cap|T_{i'_{k+1}}^{X\prime}|\cap|T_{i'}^{X\prime}|$.
We have
$$
\rho_{i'_0,k+1}^{X\prime}\circ\pi_{i'}^{X\prime}=\hat\rho_{i'_0,k}^{X\prime}\circ\pi_{i'_{k+1}}^{X\prime}\circ\pi_{i'}^{X\prime}\quad\text{by definition of }\rho_{i'_0,k+1}^{X\prime}\qquad\qquad
$$
$$
=\hat\rho_{i'_0,k}^{X\prime}\circ\pi_{i'_{k+1}}^{X\prime}\quad\text{by the first equation in (iii)}
$$
$$
\qquad\qquad=\rho_{i'_0,k+1}^{X\prime}\quad\text{by definition of }\rho_{i'_0,k+1}^{X\prime}\quad\text{on}\ |T_{i'_0}^{X\prime}|\cap|T_{i'_{k+1}}^{X\prime}|\cap|T_{i'}^{X\prime}|.
$$
Thus by the second induction we obtain $\rho_{i'_0,d-1}^{X\prime}:|T_{i'_0}^{X\prime}|\cap(|T_{i'_1}^{X\prime}|\cup\cdots\cup|T_{i',d-1}^{X\prime}|)\to\R$. \par
  It remains only to extend $\rho_{i'_0,d-1}^{X\prime}$ to a non-negative semialgebraic $C^0$ function $\rho_{i'_0,d}^{X\prime}$ on $|T_{i'_0}^{X\prime}|$ with zero set $X'_{i'_0}$ and of class $C^1$ outside of $X'_{i'_0}$.
However we have already carried out such a sort of extension by using a partition of unity $\xi$. \par
  We need to solve the problem of $C^1$ regularity of $\rho_{i'_0,d}^{X\prime}|_{X'_{i'}\cap\pi_{i'_0}^{X\prime-1}(x)-X'_{i'_0}}$.
For each $x\in X'_{i'_0}$, the restriction of $\rho_{i'_0,d}^{X\prime}$ to $X'_{i'}\cap\pi_{i'_0}^{X\prime-1}(x)\cap\rho_{i'_0,d}^{X\prime-1}((0,\,\delta_x))$ is $C^1$ regular for some $\delta_x>0\in\R$ and any $i'\in I'$.
Here we can choose $\delta_x$ so that the function $X'_{i'_0}\ni x\to\delta_x\in\R$ is semialgebraic (but not necessarily continuous).
Then there exists a semialgebraic closed subset $X''_{i'_0}$ of $X'_{i'_0}$ of smaller dimension such that each point $x$ in $X'_{i'_0}-X''_{i'_0}$ has a neighborhood in $X'_{i'_0}$ where $\delta_x$ is larger than a positive number.
Hence if we replace $X'_{i'_0}$ with $X'_{i'_0}-X''_{i'_0}$, i.e., $Y'_{j'_0}$ with $Y'_{j'_0}-p(X''_{i'_0})$ and shrink $|T_{i'_0}^{X\prime}|$ then the $C^1$ regularity holds.
Thus we obtain the required $\rho_{i'_0}^{X\prime}$ though $X'_{i'_0}$ is shrunk to $X'_{i'_0}-X''_{i'_0}$. \par
  The shrinking is admissible as follows.
Substratify $\{Y'_{j'}\cap p(\overline{X''_{i'_0}}),\,Y'_{j'}-p(\overline{X''_{i'_0}})\}$ to a Whitney semialgebraic $C^1$ stratification $\{Y''_{j''}\}$ such that $\{Y'_{j'}-p(\overline{X''_{i'_0}})\}=\{Y''_{j''}-p(\overline{X''_{i'_0}})\}$, set $\{X''_{i''}\}=\{X_{i,j}\cap p^{-1}(Y''_{j''}),\,Z\cap\{0\}\times Y''_{j''}\}$, which implies $\{X'_{i'}-p^{-1}(p(\overline{X''_{i'_0}}))\}=\{X''_{i''}-p^{-1}(p(\overline{X''_{i'_0}}))\}$, and repeat all the above arguments to $\overline f:\{X''_{i''}\}\to\{Y''_{j''}\}$.
Then we obtain a semialgebraic $C^1$ tube system $\{T_{j''}^{Y\prime\prime}\}$ for $\{Y''_{j''}\}$ and a semialgebraic $C^1$ tube system $\{T_{i''}^{X\prime\prime}:X''_{i''}\subset X\}$ for $\{X''_{i''}\subset X\}$ controlled over $\{T_{j''}^{Y\prime\prime}\}$ such that $\{T_{j''}^{Y\prime\prime}:Y''_{j''}\cap p(\overline{X''_{i'_0}})=\emptyset\}$ and $\{T_{i''}^{X\prime\prime}:X''_{i''}\subset X,\ X''_{i''}\cap p^{-1}(p(\overline{X''_{i'_0}}))=\emptyset\}$ are equal to $\{T_{j'}^{Y\prime}|_{|T_{j'}^{Y\prime}|-\pi_{j'}^{Y\prime-1}(p(\overline{X''_{i'_0}}))}\}$ and $\{T_{i'}^{X\prime}|_{|T_{i'}^{X\prime}|-\pi_{i'}^{X\prime-1}(p^{-1}(p(\overline{X''_{i'_0}})))}\}$, respectively, by (iv) and (ix), where the domains of the latter two tube systems are shrunk.
Moreover we continue construction of $\rho_{i''}^{X\prime\prime}$ for $X''\subset Z$.
Since $\{X''_{i''}\subset Z:\dim X''_{i''}>d\}=\{X'_{i'}\subset Z:\dim X'_{i'}>d\}$ and $\{X''_{i''}\subset Z:\dim X''_{i''}=d\}=\{X'_{i'_0}-X''_{i'_0}\}$ we choose $\rho_{i'}^{X\prime}$ as $\rho_{i''}^{X\prime\prime}$ for $X''_{i''}\subset Z$ with $\dim X''_{i''}>d$ and $\rho_{i'_0}^{X\prime}|_{|T_{i''}^{X\prime\prime}|}$ as $\rho_{i''}^{X\prime\prime}$ for $X''_{i''}\subset Z$ with $\dim X''_{i''}=d$.
Hence we can assume $X''_{i'_0}=\emptyset$ from the beginning, which completes the construction of $\rho_{i'_0}^{X\prime}$ and hence of the required $\{\rho_{i'}^{X\prime}:i'\in\partial I\}$ by induction.\par
  Thus $\overline f:\{X'_{i'}\}\to\{Y'_{j'}\},\ \{T_{i'}^{X\prime}\}$ and $\{T_{j'}^{Y\prime}\}$ satisfy the conditions in theorem 2.2.
Hence theorem 1.2 follows. \qed


TITLE: Birthday problem without electronic aids in a nuclear winter
QUESTION [8 upvotes]: The Birthday Problem is well known, with many related questions and answers on this site.
Most solutions somewhere make use of a statement equivalent to:
$\frac{365!}{342!365^{23}} < \frac 1 2$. The correctness of this statement is usually demonstrated by asserting (by use of a calculator, other electronic means, or log tables) that the left hand side is approximately 0.492703.
My question asks: "What would be the most efficient way of demonstrating the truth of the above statement using only pen and paper?"  Assume that all computers and tables of logarithms have been destroyed in a nuclear holocaust.
Clearly it would be possible (but painful) to do this following long-division in long-hand:
$$\frac{365\cdot 364 \cdot 363 \cdot \dots \cdot 343 } {365\cdot 365 \cdot 365 \cdot \dots \cdot 365}$$ but there must be better ways.
My first thought was to prove something simpler from which the result still follows.  For example, one can show easily with pen and paper that
$$\frac{365!}{342!365^{23}} = \prod_{k=0}^{22}\left(1-\frac k {365}\right)<\prod_{k=0}^{22}  e^{-\frac k {365}}= \exp\left({-\frac {253}{365}}\right).$$  It would therefore be sufficient to demonstrate that $\exp\left({-\frac {253}{365}}\right) < \frac 1 2$ (which is a true statement since $\exp\left({-\frac {253}{365}}\right) \approx 0.4999982478$). Equivalently it would be sufficient to show that $\frac{253}{365}>\ln 2$.  But these may not be the best ways of proceeding, and I have not managed to bring them to a satisfactory pen-and-paper conclusion.

REPLY [1 votes]: I think I have a much better/simpler/more-direct approach to answering this question.  It's nothing to do with my previous $\ln 2$ related answer (see elsewhere in this thread) so I'm posting it separately.
Here I try to show directly $$\frac{365!}{342!365^{23}} <\frac 1 2$$ using only a `difference of two squares' inequality: $a^2\ge a^2-b^2 = (a+b)(a-b)$.
Here goes:
$$\begin{align}
\frac{365!}{342!365^{23}} &= \frac{365\cdot 364 \cdot 363 \cdot \dots \cdot 343 } {365^{23}}
\\
&=
\frac{(354+11)\cdot (354+10) \cdot  \dots \cdot (354-10)\cdot(354-11) } {365^{23}}
\\
&=
\frac{\left[(354^2-11^2)\cdot (354^2-10^2) \cdot  \dots \cdot (354^2-1^2)\right]\cdot(354-0) } {365^{23}}
\\
&<
\frac{\left[(354^2-0^2)\cdot (354^2-0^2) \cdot  \dots \cdot (354^2-0^2)\right]\cdot(354-0) } {365^{23}}
\\
&=
\left(\frac{354}{365}\right)^{23}.
\end{align}
$$
From here it is relatively easy to show (with only pen and paper) that $\left(\frac{354}{365}\right)^{23}\approx0.495<\frac 1 2$.  For example, abbreviating the value of $\frac{354}{365}$ by the symbol $\rho$, we could repeatedly square $\rho$ no more than four times, and then evaluate $\rho^{23}$ from the product $\rho^{1+2+4+16}=\rho^1 \rho^2 (\rho^2)^2 (((\rho^2)^2)^2)^2$.  This requires a total of seven multiplications (four taken while repeatedly squaring $\rho$, and then a further three multiplications to combine those results into the final answer).


text:
(*  Author:  Gertrud Bauer, Tobias Nipkow  *)

section "Further Plane Graph Properties"

theory PlaneProps
imports Invariants
begin

subsection \<open>@{const final}\<close>

lemma plane_final_facesAt:
assumes "inv g" "final g" "v : \<V> g" "f \<in> set (facesAt g v)" shows "final f"
proof -
  from assms(1,3,4) have "f \<in> \<F> g" by(blast intro: minGraphProps inv_mgp)
  with assms(2) show ?thesis by (rule finalGraph_face)
qed

lemma finalVertexI:
  "\<lbrakk> inv g;  final g;  v \<in> \<V> g \<rbrakk> \<Longrightarrow> finalVertex g v"
by (auto simp add: finalVertex_def nonFinals_def filter_empty_conv plane_final_facesAt)

lemma setFinal_notin_finals:
 "\<lbrakk> f \<in> \<F> g; \<not> final f; minGraphProps g \<rbrakk> \<Longrightarrow> setFinal f \<notin> set (finals g)"
apply(drule minGraphProps11)
apply(cases f)
apply(fastforce simp:finals_def setFinal_def normFaces_def normFace_def
                    verticesFrom_def minVertex_def inj_on_def distinct_map
           split:facetype.splits)
done

subsection \<open>@{const degree}\<close>

lemma planeN4: "inv g \<Longrightarrow> f \<in> \<F> g \<Longrightarrow> 3 \<le> |vertices f|"
apply(subgoal_tac "2 < | vertices f |")
 apply arith
apply(drule inv_mgp)
apply (erule (1) minGraphProps2)
done

lemma degree_eq:
assumes pl: "inv g" and fin: "final g" and v: "v : \<V> g"
shows "degree g v = tri g v + quad g v + except g v"
proof -
  have dist: "distinct(facesAt g v)" using pl v by simp
  have 3: "\<forall>f \<in> set(facesAt g v). |vertices f| = 3 \<or> |vertices f| = 4 \<or>
                                  |vertices f| \<ge> 5"
  proof
    fix f assume f: "f \<in> set (facesAt g v)"
    hence "|vertices f| \<ge> 3"
      using minGraphProps5[OF inv_mgp[OF pl] v f] planeN4[OF pl] by blast
    thus "|vertices f| = 3 \<or> |vertices f| = 4 \<or> |vertices f| \<ge> 5" by arith
  qed
  have "degree g v = |facesAt g v|" by(simp add:degree_def)
  also have "\<dots> = card(set(facesAt g v))" by (simp add:distinct_card[OF dist])
  also have "set(facesAt g v) = {f \<in> set(facesAt g v). |vertices f| = 3} \<union>
                                {f \<in> set(facesAt g v). |vertices f| = 4} \<union>
                                {f \<in> set(facesAt g v). |vertices f| \<ge> 5}"
    (is "_ = ?T \<union> ?Q \<union> ?E")
    using 3 by blast
  also have "card(?T \<union> ?Q \<union> ?E) = card ?T + card ?Q + card ?E"
    apply (subst card_Un_disjoint)
    apply simp
    apply simp
    apply fastforce
    apply (subst card_Un_disjoint)
    apply simp
    apply simp
    apply fastforce
    apply simp
    done
  also have "\<dots> = tri g v + quad g v + except g v" using fin
    by(simp add:tri_def quad_def except_def
                distinct_card[symmetric] distinct_filter[OF dist]
                plane_final_facesAt[OF pl fin v] cong:conj_cong)
  finally show ?thesis .
qed

lemma plane_fin_exceptionalVertex_def:
assumes pl: "inv g" and fin: "final g" and v: "v : \<V> g"
shows "exceptionalVertex g v =
 ( | [f \<leftarrow> facesAt g v . 5 \<le> |vertices f| ] | \<noteq> 0)"
proof -
  have "\<And>f. f \<in> set (facesAt g v) \<Longrightarrow> final f"
    by(rule plane_final_facesAt[OF pl fin v])
  then show ?thesis by (simp add: filter_simp exceptionalVertex_def except_def)
qed

lemma not_exceptional:
  "inv g \<Longrightarrow> final g \<Longrightarrow> v : \<V> g \<Longrightarrow> f \<in> set (facesAt g v) \<Longrightarrow>
  \<not> exceptionalVertex g v \<Longrightarrow> |vertices f| \<le> 4"
by (auto simp add: plane_fin_exceptionalVertex_def except_def filter_empty_conv)

subsection \<open>Misc\<close>

lemma in_next_plane0I:
assumes "g' \<in> set (generatePolygon n v f g)" "f \<in> set (nonFinals g)"
        "v \<in> \<V> f" "3 \<le> n" "n < 4+p"
shows "g' \<in> set (next_plane0\<^bsub>p\<^esub> g)"
proof -
  from assms have
    "\<exists>n\<in>{3..<4 + p}. g' \<in> set (generatePolygon n v f g)"
    by auto
  with assms have
    "\<exists>v\<in>\<V> f. \<exists>n\<in>{3..<4 + p}. g' \<in> set (generatePolygon n v f g)"
    by auto
  with assms have
    "\<exists>f\<in>set (nonFinals g). \<exists>v\<in>\<V> f. \<exists>n\<in>{3..<4 + p}. g' \<in> set (generatePolygon n v f g)"
    by auto
  moreover have "\<not> final g" using assms(2)
    by (auto simp: nonFinals_def finalGraph_def filter_empty_conv)
  ultimately show ?thesis
    by (simp add: next_plane0_def)
qed

lemma next_plane0_nonfinals: "g [next_plane0\<^bsub>p\<^esub>]\<rightarrow> g' \<Longrightarrow> nonFinals g \<noteq> []"
by(auto simp:next_plane0_def finalGraph_def)

lemma next_plane0_ex:
assumes a: "g [next_plane0\<^bsub>p\<^esub>]\<rightarrow> g'"
shows "\<exists>f\<in> set(nonFinals g). \<exists>v \<in> \<V> f. \<exists>i \<in> set([3..<Suc(maxGon p)]).
       g' \<in> set (generatePolygon i v f g)"
proof -
  from a have "\<not> final g" by (auto simp add: next_plane0_def)
  with a show ?thesis
   by (auto simp add: next_plane0_def nonFinals_def)
qed

lemma step_outside2:
 "inv g \<Longrightarrow> g [next_plane0\<^bsub>p\<^esub>]\<rightarrow> g' \<Longrightarrow> \<not> final g' \<Longrightarrow> |faces g'| \<noteq> 2"
apply(frule inv_two_faces)
apply(frule inv_finals_nonempty)
apply(drule inv_mgp)
apply(insert len_faces_sum[of g] len_faces_sum[of g'])
apply(subgoal_tac "|nonFinals g| \<noteq> 0")
 prefer 2 apply(drule next_plane0_nonfinals) apply simp
apply(subgoal_tac "|nonFinals g'| \<noteq> 0")
 prefer 2 apply(simp add:finalGraph_def)
apply(drule (1) next_plane0_incr_faces)
apply(case_tac "|faces g| = 2")
 prefer 2 apply arith
apply(subgoal_tac "|finals g| \<noteq> 0")
 apply arith
apply simp
done

subsection\<open>Increasing final faces\<close>

lemma set_finals_splitFace[simp]:
 "\<lbrakk> f \<in> \<F> g; \<not> final f \<rbrakk> \<Longrightarrow>
  set(finals(snd(snd(splitFace g u v f vs)))) = set(finals g)"
apply(auto simp add:splitFace_def split_def finals_def
                split_face_def)
 apply(drule replace5)
 apply(clarsimp)
apply(erule replace4)
apply clarsimp
done

lemma next_plane0_finals_incr:
 "g [next_plane0\<^bsub>p\<^esub>]\<rightarrow> g' \<Longrightarrow> f \<in> set(finals g) \<Longrightarrow> f \<in> set(finals g')"
apply(auto simp:next_plane0_def generatePolygon_def split:if_split_asm)
apply(erule subdivFace_pres_finals)
apply (simp add:nonFinals_def)
done

lemma next_plane0_finals_subset:
  "g' \<in> set (next_plane0\<^bsub>p\<^esub> g) \<Longrightarrow>
  set (finals g) \<subseteq> set (finals g')"
  by (auto simp add: next_plane0_finals_incr)

lemma next_plane0_final_mono:
  "\<lbrakk> g' \<in> set (next_plane0\<^bsub>p\<^esub> g); f \<in> \<F> g; final f \<rbrakk> \<Longrightarrow> f \<in> \<F> g'"
apply(drule next_plane0_finals_subset)
apply(simp add:finals_def)
apply blast
done

subsection\<open>Increasing vertices\<close>

lemma next_plane0_vertices_subset:
 "\<lbrakk> g' \<in> set (next_plane0\<^bsub>p\<^esub> g); minGraphProps g \<rbrakk> \<Longrightarrow> \<V> g \<subseteq> \<V> g'"
apply(rule next_plane0_incr)
    apply(erule (1) subset_trans)
   apply(simp add: vertices_makeFaceFinal)
  defer apply assumption+
apply (auto simp: splitFace_def split_def vertices_graph)
done

subsection\<open>Increasing vertex degrees\<close>

lemma next_plane0_incr_faceListAt:
 "\<lbrakk> g' \<in> set (next_plane0\<^bsub>p\<^esub> g); minGraphProps g \<rbrakk>
  \<Longrightarrow> |faceListAt g| \<le> |faceListAt g'| \<and>
      (\<forall>v < |faceListAt g|. |faceListAt g ! v| \<le> |faceListAt g' ! v| )"
 (is "_ \<Longrightarrow> _ \<Longrightarrow> ?Q g g'")
apply(rule next_plane0_incr[where Q = ?Q])
prefer 4 apply assumption
prefer 4 apply assumption
  apply(rule conjI) apply fastforce
  apply(clarsimp)
  apply(erule allE, erule impE, assumption)
  apply(erule_tac x = v in allE, erule impE) apply force
  apply force
 apply(simp add: makeFaceFinal_def makeFaceFinalFaceList_def)
apply (simp add: splitFace_def split_def nth_append nth_list_update)
done

lemma next_plane0_incr_degree:
 "\<lbrakk> g' \<in> set (next_plane0\<^bsub>p\<^esub> g); minGraphProps g; v \<in> \<V> g \<rbrakk>
  \<Longrightarrow> degree g v \<le> degree g' v"
apply(frule (1) next_plane0_incr_faceListAt)
apply(frule (1) next_plane0_vertices_subset)
apply(simp add:degree_def facesAt_def)
apply(frule minGraphProps4)
apply(simp add:vertices_graph)
done

subsection\<open>Increasing @{const except}\<close>

lemma next_plane0_incr_except:
assumes "g' \<in> set (next_plane0\<^bsub>p\<^esub> g)" "inv g" "v \<in> \<V> g"
shows "except g v \<le> except g' v"
proof (unfold except_def)
  note inv' = invariantE[OF inv_inv_next_plane0, OF assms(1,2)]
  note mgp = inv_mgp[OF assms(2)] and mgp' = inv_mgp[OF inv']
  note dist = distinct_filter[OF mgp_dist_facesAt[OF mgp \<open>v : \<V> g\<close>]]
  have "v \<in> \<V> g'"
    using assms(3) next_plane0_vertices_subset[OF assms(1) mgp] by blast
  note dist' = distinct_filter[OF mgp_dist_facesAt[OF mgp' \<open>v : \<V> g'\<close>]]
  have "|[f\<leftarrow>facesAt g v . final f \<and> 5 \<le> |vertices f| ]| =
        card{f\<in> set(facesAt g v) . final f \<and> 5 \<le> |vertices f|}"
    (is "?L = card ?M") using distinct_card[OF dist] by simp
  also have "?M = {f\<in> \<F> g. v \<in> \<V> f \<and> final f \<and> 5 \<le> |vertices f|}"
    by(simp add: minGraphProps_facesAt_eq[OF mgp assms(3)])
  also have "\<dots> = {f \<in> set(finals g) . v \<in> \<V> f \<and> 5 \<le> |vertices f|}"
    by(auto simp:finals_def)
  also have "card \<dots> \<le> card{f \<in> set(finals g'). v \<in> \<V> f \<and> 5 \<le> |vertices f|}"
    (is "_ \<le> card ?M")
    apply(rule card_mono)
    apply simp
    using next_plane0_finals_subset[OF assms(1)] by blast
  also have "?M = {f\<in> \<F> g' . v \<in> \<V> f \<and> final f \<and> 5 \<le> |vertices f|}"
    by(auto simp:finals_def)
  also have "\<dots> = {f \<in> set(facesAt g' v) . final f \<and> 5 \<le> |vertices f|}"
    by(simp add: minGraphProps_facesAt_eq[OF mgp' \<open>v \<in> \<V> g'\<close>])
  also have "card \<dots> =
    |[f \<leftarrow> facesAt g' v . final f \<and> 5 \<le> |vertices f| ]|" (is "_ = ?R")
    using distinct_card[OF dist'] by simp
  finally show "?L \<le> ?R" .
qed

subsection\<open>Increasing edges\<close>

lemma next_plane0_set_edges_subset:
  "\<lbrakk> minGraphProps g;  g [next_plane0\<^bsub>p\<^esub>]\<rightarrow> g' \<rbrakk> \<Longrightarrow> edges g \<subseteq> edges g'"
apply(rule next_plane0_incr)
    apply(erule (1) subset_trans)
   apply(simp add: edges_makeFaceFinal)
  apply(erule snd_snd_splitFace_edges_incr)
 apply assumption+
done

subsection\<open>Increasing final vertices\<close>

(*
This should really be proved via the (unproven) invariant
v : f \<Longrightarrow> ((g,v).f).(f.v) = v
*)

declare  atLeastLessThan_iff[iff]

lemma next_plane0_incr_finV:
 "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); minGraphProps g \<rbrakk>
  \<Longrightarrow> \<forall>v \<in> \<V> g. v \<in> \<V> g' \<and>
        ((\<forall>f\<in>\<F> g. v \<in> \<V> f \<longrightarrow> final f) \<longrightarrow>
         (\<forall>f\<in>\<F> g'. v \<in> \<V> f \<longrightarrow> f \<in> \<F> g))" (is "_ \<Longrightarrow> _ \<Longrightarrow> ?Q g g'")
apply(rule next_plane0_incr[where Q = ?Q and g=g and g'=g'])
prefer 4 apply assumption
prefer 4 apply assumption
  apply fast
 apply(clarsimp simp:makeFaceFinal_def vertices_graph makeFaceFinalFaceList_def)
 apply(drule replace5)
 apply(erule disjE)apply blast
 apply(simp add:setFinal_def)
apply(unfold pre_splitFace_def)
apply(clarsimp simp:splitFace_def split_def vertices_graph)
apply(rule conjI)
 apply(clarsimp simp:split_face_def vertices_graph atLeastLessThan_def)
 apply(blast dest:inbetween_inset)
apply(clarsimp)
apply(erule disjE[OF replace5]) apply blast
apply(clarsimp simp:split_face_def vertices_graph)
apply(blast dest:inbetween_inset)
done

lemma next_plane0_finalVertex_mono:
 "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); inv g; u \<in> \<V> g; finalVertex g u \<rbrakk>
  \<Longrightarrow> finalVertex g' u"
apply(frule (1) invariantE[OF inv_inv_next_plane0])
apply(subgoal_tac "u \<in> \<V> g'")
 prefer 2 apply(blast dest:next_plane0_vertices_subset inv_mgp)
apply(clarsimp simp:finalVertex_def minGraphProps_facesAt_eq[OF inv_mgp])
apply(blast dest:next_plane0_incr_finV inv_mgp)
done

subsection\<open>Preservation of @{const facesAt} at final vertices\<close>

lemma next_plane0_finalVertex_facesAt_eq:
 "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); inv g; v \<in> \<V> g; finalVertex g v \<rbrakk>
  \<Longrightarrow> set(facesAt g' v) = set(facesAt g v)"
apply(frule (1) invariantE[OF inv_inv_next_plane0])
apply(subgoal_tac "v \<in> \<V> g'")
 prefer 2 apply(blast dest:next_plane0_vertices_subset inv_mgp)
apply(clarsimp simp:finalVertex_def minGraphProps_facesAt_eq[OF inv_mgp])
by(blast dest:next_plane0_incr_finV next_plane0_final_mono inv_mgp)

lemma next_plane0_len_filter_eq:
assumes "g' \<in> set (next_plane0\<^bsub>p\<^esub> g)" "inv g" "v \<in> \<V> g" "finalVertex g v"
shows "|filter P (facesAt g' v)| = |filter P (facesAt g v)|"
proof -
  note inv' = invariantE[OF inv_inv_next_plane0, OF assms(1,2)]
  note mgp = inv_mgp[OF assms(2)] and mgp' = inv_mgp[OF inv']
  note dist = distinct_filter[OF mgp_dist_facesAt[OF mgp \<open>v : \<V> g\<close>]]
  have "v \<in> \<V> g'"
    using assms(3) next_plane0_vertices_subset[OF assms(1) mgp] by blast
  note dist' = distinct_filter[OF mgp_dist_facesAt[OF mgp' \<open>v : \<V> g'\<close>]]
  have "|filter P (facesAt g' v)| = card{f \<in> set(facesAt g' v) . P f}"
    using distinct_card[OF dist'] by simp
  also have "\<dots> = card{f \<in> set(facesAt g v) . P f}"
    by(simp add: next_plane0_finalVertex_facesAt_eq[OF assms])
  also have "\<dots> = |filter P (facesAt g v)|"
    using distinct_card[OF dist] by simp
  finally show ?thesis .
qed

subsection\<open>Properties of @{const subdivFace'}\<close>

lemma new_edge_subdivFace':
  "\<And>f v n g.
  pre_subdivFace' g f u v n ovs \<Longrightarrow> minGraphProps g \<Longrightarrow> f \<in> \<F> g \<Longrightarrow>
  subdivFace' g f v n ovs = makeFaceFinal f g \<or>
  (\<forall>f' \<in> \<F> (subdivFace' g f v n ovs) - (\<F> g - {f}).
   \<exists>e \<in> \<E> f'. e \<notin> \<E> g)"
proof (induct ovs)
  case Nil thus ?case by simp
next
  case (Cons ov ovs)
  note IH = Cons(1) and pre = Cons(2) and mgp = Cons(3) and fg = Cons(4)
  have uf: "u \<in> \<V> f" and vf: "v \<in> \<V> f" and distf: "distinct (vertices f)"
    using pre by(simp add:pre_subdivFace'_def)+
  note distFg = minGraphProps11'[OF mgp]
  show ?case
  proof (cases ov)
    case None
    have pre': "pre_subdivFace' g f u v (Suc n) ovs"
      using None pre by (simp add: pre_subdivFace'_None)
    show ?thesis using None
      by (simp add: IH[OF pre' mgp fg])
  next
    case (Some w)
    note pre = pre[simplified Some]
    have uvw: "before (verticesFrom f u) v w"
      using pre by(simp add:pre_subdivFace'_def)
    have uw: "u \<noteq> w" using pre by(clarsimp simp: pre_subdivFace'_def)
    { assume w: "f \<bullet> v = w" and n: "n = 0"
      have pre': "pre_subdivFace' g f u w 0 ovs"
        using pre Some n using [[simp_depth_limit = 5]] by (simp add: pre_subdivFace'_Some2)
      note IH[OF pre' mgp fg]
    } moreover
    { let ?vs = "[countVertices g..<countVertices g + n]"
      let ?fdg = "splitFace g v w f ?vs"
      let  ?f\<^sub>1 = "fst ?fdg" and ?f\<^sub>2 = "fst(snd ?fdg)" and ?g' = "snd(snd ?fdg)"
      let ?g'' = "subdivFace' ?g' ?f\<^sub>2 w 0 ovs"
      let ?fvw = "between(vertices f) v w" and ?fwv = "between(vertices f) w v"
      assume a: "f \<bullet> v = w \<longrightarrow> 0 < n"
      have fsubg: "\<V> f \<subseteq> \<V> g"
        using mgp fg by(simp add: minGraphProps_def faces_subset_def)
      have pre_fdg: "pre_splitFace g v w f ?vs"
           apply (rule pre_subdivFace'_preFaceDiv[OF pre fg _ fsubg])
           using a by (simp)
      hence "v \<noteq> w" and "w \<in> \<V> f" by(unfold pre_splitFace_def)simp+
      have f\<^sub>1: "?f\<^sub>1= fst(split_face f v w ?vs)"
        and f\<^sub>2: "?f\<^sub>2 = snd(split_face f v w ?vs)"
        by(auto simp add:splitFace_def split_def)
      note pre_split = pre_splitFace_pre_split_face[OF pre_fdg]
      have E\<^sub>1: "\<E> ?f\<^sub>1 = Edges (w # rev ?vs @ [v]) \<union> Edges (v # ?fvw @ [w])"
        using f\<^sub>1 by(simp add:edges_split_face1[OF pre_split])
      have E\<^sub>2: "\<E> ?f\<^sub>2 = Edges (v # ?vs @ [w]) \<union> Edges (w # ?fwv @ [v])"
        by(simp add:splitFace_def split_def
            edges_split_face2[OF pre_split])
      note mgp' = splitFace_holds_minGraphProps[OF pre_fdg mgp]
      note distFg' = minGraphProps11'[OF mgp']
      have pre': "pre_subdivFace' ?g' ?f\<^sub>2 u w 0 ovs"
        by (rule pre_subdivFace'_Some1[OF pre fg _ fsubg HOL.refl HOL.refl])
           (simp add:a)
      note f2inF = splitFace_add_f21'[OF fg]
      have 1: "\<exists>e \<in> \<E> ?f\<^sub>1. e \<notin> \<E> g"
      proof cases
        assume "rev ?vs = []"
        hence "(w,v) \<in> \<E> ?f\<^sub>1 \<and> (w,v) \<notin> \<E> g" using pre_fdg E\<^sub>1
          by(unfold pre_splitFace_def) (auto simp:Edges_Cons)
        thus ?thesis by blast
      next
        assume "rev ?vs \<noteq> []"
        then obtain x xs where rvs: "rev ?vs = x#xs"
          by(auto simp only:neq_Nil_conv)
        hence "(w,x) \<in> \<E> ?f\<^sub>1" using E\<^sub>1 by (auto simp:Edges_Cons)
        moreover have "(w,x) \<notin> \<E> g"
        proof -
          have "x \<in> set(rev ?vs)" using rvs by simp
          hence "x \<ge> countVertices g" by simp
          hence "x \<notin> \<V> g" by(induct g) (simp add:vertices_graph_def)
          thus ?thesis
            by (auto simp:edges_graph_def)
               (blast dest: in_edges_in_vertices minGraphProps9[OF mgp])
        qed
        ultimately show ?thesis by blast
      qed
      have 2: "\<exists>e \<in> \<E> ?f\<^sub>2. e \<notin> \<E> g"
      proof cases
        assume "?vs = []"
        hence "(v,w) \<in> \<E> ?f\<^sub>2 \<and> (v,w) \<notin> \<E> g" using pre_fdg E\<^sub>2
          by(unfold pre_splitFace_def) (auto simp:Edges_Cons)
        thus ?thesis by blast
      next
        assume "?vs \<noteq> []"
        then obtain x xs where vs: "?vs = x#xs"
          by(auto simp only:neq_Nil_conv)
        hence "(v,x) \<in> \<E> ?f\<^sub>2" using E\<^sub>2 by (auto simp:Edges_Cons)
        moreover have "(v,x) \<notin> \<E> g"
        proof -
          have "x \<in> set ?vs" using vs by simp
          hence "x \<ge> countVertices g" by simp
          hence "x \<notin> \<V> g" by(induct g) (simp add:vertices_graph_def)
          thus ?thesis
            by (auto simp:edges_graph_def)
               (blast dest: in_edges_in_vertices minGraphProps9[OF mgp])
        qed
        ultimately show ?thesis by blast
      qed
      have fdg: "(?f\<^sub>1,?f\<^sub>2,?g') = splitFace g v w f ?vs" by auto
      hence Fg': "\<F> ?g' = {?f\<^sub>1,?f\<^sub>2} \<union> (\<F> g - {f})"
        using set_faces_splitFace[OF mgp fg pre_fdg] by blast
      have "\<forall>f' \<in> \<F> ?g'' - (\<F> g - {f}). \<exists>e \<in> \<E> f'. e \<notin> \<E> g"
      proof (clarify)
        fix f' assume f'g'': "f' \<in> \<F> ?g''" and f'ng: "f' \<notin> \<F> g - {f}"
        from IH[OF pre' mgp' f2inF]
        show "\<exists>e \<in> \<E> f'. e \<notin> \<E> g"
        proof
          assume "?g'' = makeFaceFinal ?f\<^sub>2 ?g'"
          hence "f' = setFinal ?f\<^sub>2 \<or> f' = ?f\<^sub>1" (is "?A \<or> ?B")
            using f'g'' Fg' f'ng
            by(auto simp:makeFaceFinal_def makeFaceFinalFaceList_def
              distinct_set_replace[OF distFg'])
          thus ?thesis
          proof
            assume ?A thus ?thesis using 2 by(simp)
          next
            assume ?B thus ?thesis using 1 by blast
          qed
        next
          assume A: "\<forall>f' \<in> \<F> ?g'' - (\<F> ?g' - {?f\<^sub>2}).
                     \<exists>e \<in> \<E> f'. e \<notin> \<E> ?g'"
          show ?thesis
          proof cases
            assume "f' \<in> {?f\<^sub>1,?f\<^sub>2}"
            thus ?thesis using 1 2 by blast
          next
            assume "f' \<notin> {?f\<^sub>1,?f\<^sub>2}"
            hence "\<exists>e\<in>\<E> f'. e \<notin> \<E> ?g'"
              using A f'g'' f'ng Fg' by simp
            with splitFace_edges_incr[OF pre_fdg fdg]
            show ?thesis by blast
          qed
        qed
      qed
    }
    ultimately show ?thesis using Some by(auto simp: split_def)
  qed
qed

lemma dist_edges_subdivFace':
  "pre_subdivFace' g f u v n ovs \<Longrightarrow> minGraphProps g \<Longrightarrow> f \<in> \<F> g \<Longrightarrow>
  subdivFace' g f v n ovs = makeFaceFinal f g \<or>
  (\<forall>f' \<in> \<F> (subdivFace' g f v n ovs) - (\<F> g - {f}). \<E> f' \<noteq> \<E> f)"
apply(drule (2) new_edge_subdivFace')
apply(erule disjE)
 apply blast
apply(rule disjI2)
apply(clarify)
apply(drule bspec)
 apply fast
apply(simp add:edges_graph_def)
by(blast)

lemma between_last: "\<lbrakk> distinct(vertices f); u \<in> \<V> f \<rbrakk> \<Longrightarrow>
   between (vertices f) u (last (verticesFrom f u)) =
   butlast(tl(verticesFrom f u))"
apply(drule split_list)
apply (fastforce dest: last_in_set
  simp: between_def verticesFrom_Def split_def
       last_append butlast_append fst_splitAt_last)
done

(* FIXME move condition to pre_addfacesnd? *)
lemma final_subdivFace': "\<And>f u n g. minGraphProps g \<Longrightarrow>
  pre_subdivFace' g f r u n ovs \<Longrightarrow> f \<in> \<F> g \<Longrightarrow>
  (ovs = [] \<longrightarrow> n=0 \<and> u = last(verticesFrom f r)) \<Longrightarrow>
  \<exists>f' \<in> set(finals(subdivFace' g f u n ovs)) - set(finals g).
   (f\<^bsup>-1\<^esup> \<bullet> r,r) \<in> \<E> f' \<and>  |vertices f'| =
      n + |ovs| + (if r=u then 1 else |between (vertices f) r u| + 2)"
proof (induct ovs)
  case Nil show ?case (is "\<exists>f' \<in> ?F. ?P f'")
  proof
    show "?P (setFinal f)" (is "?A \<and> ?B")
    proof
      show "?A" using Nil
        by(simp add:pre_subdivFace'_def prevVertex_in_edges
          del:is_nextElem_edges_eq)
      show  "?B"
        using Nil mgp_vertices3[OF Nil(1,3)]
        by(simp add:  setFinal_def between_last pre_subdivFace'_def)
    qed
  next
    show "setFinal f \<in> ?F" using Nil
      by(simp add:pre_subdivFace'_def setFinal_notin_finals minGraphProps11')
  qed
next
  case (Cons ov ovs)
  note IH = Cons(1) and mgp = Cons(2) and pre = Cons(3) and fg = Cons(4)
    and mt = Cons(5)
  have "r \<in> \<V> f" and "u \<in> \<V> f" and distf: "distinct (vertices f)"
    using pre by(simp add:pre_subdivFace'_def)+
  show ?case
  proof (cases ov)
    case None
    have pre': "pre_subdivFace' g f r u (Suc n) ovs"
      using None pre by (simp add: pre_subdivFace'_None)
    have "ovs \<noteq> []" using pre None by (auto simp: pre_subdivFace'_def)
    thus ?thesis using None IH[OF mgp pre' fg] by simp
  next
    case (Some v)
    note pre = pre[simplified Some]
      have ruv: "before (verticesFrom f r) u v" and "r \<noteq> v"
        using pre by(simp add:pre_subdivFace'_def)+
    show ?thesis
    proof (cases "f \<bullet> u = v \<and> n = 0")
      case True
      have pre': "pre_subdivFace' g f r v 0 ovs"
        using pre True using [[simp_depth_limit = 5]] by (simp add: pre_subdivFace'_Some2)
      have mt: "ovs = [] \<longrightarrow> 0 = 0 \<and> v = last (verticesFrom f r)"
        using pre by(clarsimp simp:pre_subdivFace'_def)
      show ?thesis using Some True IH[OF mgp pre' fg mt] \<open>r \<noteq> v\<close>
        by(auto simp: between_next_empty[OF distf]
          unroll_between_next2[OF distf \<open>r \<in> \<V> f\<close> \<open>u \<in> \<V> f\<close>])
    next
      case False
      let ?vs = "[countVertices g..<countVertices g + n]"
      let ?fdg = "splitFace g u v f ?vs"
      let ?g' = "snd(snd ?fdg)" and ?f\<^sub>2 = "fst(snd ?fdg)"
      let ?fvu = "between (vertices f) v u"
      have False': "f \<bullet> u = v \<longrightarrow> n \<noteq> 0" using False by auto
      have VfVg: "\<V> f \<subseteq> \<V> g" using mgp fg
          by (simp add: minGraphProps_def faces_subset_def)
      note pre_fdg = pre_subdivFace'_preFaceDiv[OF pre fg False' VfVg]
      hence "u \<noteq> v" and "v \<in> \<V> f" and disj: "\<V> f \<inter> set ?vs = {}"
        by(unfold pre_splitFace_def)simp+
      hence vvs: "v \<notin> set ?vs" by auto
      have vf\<^sub>2: "vertices ?f\<^sub>2 = [v] @ ?fvu @ u # ?vs"
        by(simp add:split_face_def splitFace_def split_def)
      hence betuvf\<^sub>2: "between (vertices ?f\<^sub>2) u v = ?vs"
        using splitFace_distinct1[OF pre_fdg]
        by(simp add: between_back)
      have betrvf\<^sub>2: "r \<noteq> u \<Longrightarrow> between (vertices ?f\<^sub>2) r v =
        between (vertices f) r u @ [u] @ ?vs"
      proof -
        assume "r\<noteq>u"
        have r: "r \<in> set (between (vertices f) v u)"
          using \<open>r\<noteq>u\<close> \<open>r\<noteq>v\<close> \<open>u\<noteq>v\<close> \<open>v \<in> \<V> f\<close> \<open>r \<in> \<V> f\<close> distf ruv
          by(blast intro:rotate_before_vFrom before_between)
        have "between (vertices f) v u =
          between (vertices f) v r @ [r] @ between (vertices f) r u"
          using split_between[OF distf \<open>v \<in> \<V> f\<close> \<open>u \<in> \<V> f\<close> r] \<open>r\<noteq>v\<close>
          by simp
        moreover hence "v \<notin> set (between (vertices f) r u)"
          using between_not_r1[OF distf, of v u] by simp
        ultimately show ?thesis using vf\<^sub>2 \<open>r\<noteq>v\<close> \<open>u\<noteq>v\<close> vvs
          by (simp add: between_back between_not_r2[OF distf])
      qed
      note mgp' = splitFace_holds_minGraphProps[OF pre_fdg mgp]
      note f2g = splitFace_add_f21'[OF fg]
      note pre' = pre_subdivFace'_Some1[OF pre fg False' VfVg HOL.refl HOL.refl]
      from pre_fdg have "v \<in> \<V> f" and disj: "\<V> f \<inter> set ?vs = {}"
        by(unfold pre_splitFace_def, simp)+
      have fr: "?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r = f\<^bsup>-1\<^esup> \<bullet> r"
      proof -
        note pre_split = pre_splitFace_pre_split_face[OF pre_fdg]
        have rinf\<^sub>2: "r \<in> \<V> ?f\<^sub>2"
        proof cases
          assume "r = u" thus ?thesis by(simp add:vf\<^sub>2)
        next
          assume "r \<noteq> u"
          hence "r \<in> set ?fvu" using distf \<open>v : \<V> f\<close> \<open>r\<noteq>v\<close> \<open>r : \<V> f\<close> ruv
            by(blast intro: before_between rotate_before_vFrom)
          thus ?thesis by(simp add:vf\<^sub>2)
        qed
        have E\<^sub>2: "\<E> ?f\<^sub>2 = Edges (u # ?vs @ [v]) \<union>
                             Edges (v # ?fvu @ [u])"
          by(simp add:splitFace_def split_def
            edges_split_face2[OF pre_split])
        moreover have "(?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r, r) \<in> \<E> ?f\<^sub>2"
          by(blast intro: prevVertex_in_edges rinf\<^sub>2
            splitFace_distinct1[OF pre_fdg])
        moreover have "(?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r, r) \<notin> Edges (u # ?vs @ [v])"
        proof -
          have "r \<notin> set ?vs" using \<open>r : \<V> f\<close> disj by blast
          thus ?thesis using \<open>r \<noteq> v\<close>
            by(simp add:Edges_Cons Edges_append notinset_notinEdge2) arith
        qed
        ultimately have "(?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r, r) \<in> Edges (v # ?fvu @ [u])" by blast
        hence "(?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r, r) \<in> \<E> f" using pre_split_face_symI[OF pre_split]
          by(blast intro: Edges_between_edges)
        hence eq: "f \<bullet> (?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r) = r" and inf: "?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r \<in> \<V> f"
          by(simp add:edges_face_eq)+
        have "?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r = f\<^bsup>-1\<^esup> \<bullet> (f \<bullet> (?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r))"
          using prevVertex_nextVertex[OF distf inf] by simp
        also have "\<dots> = f\<^bsup>-1\<^esup> \<bullet> r" using eq by simp
        finally show ?thesis .
      qed
      hence mt: "ovs = [] \<longrightarrow> 0 = 0 \<and> v = last (verticesFrom ?f\<^sub>2 r)"
        using pre' pre by(auto simp:pre_subdivFace'_def splitFace_def
          split_def last_vFrom)
      from IH[OF mgp' pre' f2g mt] \<open>r \<noteq> v\<close> obtain f' :: face where
        f: "f' \<in> set(finals(subdivFace' ?g' ?f\<^sub>2 v 0 ovs)) - set(finals ?g')"
        and ff: "(?f\<^sub>2\<^bsup>-1\<^esup> \<bullet> r, r) \<in> \<E> f'"
        "|vertices f'| = |ovs| + |between (vertices ?f\<^sub>2) r v| + 2"
        by simp blast
      show ?thesis (is "\<exists>f' \<in> ?F. ?P f'")
      proof
        show "f' \<in> ?F" using f pre Some fg
          by(simp add:False split_def pre_subdivFace'_def)
        show "?P f'" using ff fr by(clarsimp simp:betuvf\<^sub>2 betrvf\<^sub>2)
      qed
    qed
  qed
qed

lemma Seed_max_final_ex:
 "\<exists>f\<in>set (finals (Seed p)). |vertices f| = maxGon p"
  by (simp add: Seed_def graph_max_final_ex)

lemma max_face_ex: assumes a: "Seed\<^bsub>p\<^esub> [next_plane0\<^bsub>p\<^esub>]\<rightarrow>* g"
shows "\<exists>f \<in> set (finals g). |vertices f| = maxGon p"
using a
proof (induct rule: RTranCl_induct)
  case refl then show ?case using Seed_max_final_ex by simp
next
  case (succs g g')
  then obtain f where f: "f\<in>set (finals g)" and "|vertices f| = maxGon p"
    by auto
  moreover from succs(1) f have "f\<in>set (finals g')" by (rule next_plane0_finals_incr)
  ultimately show ?case by auto
qed

end

subset_name: curated


TITLE: A closed set in $\mathbb A^2_k\times\mathbb P^1_k$
QUESTION [1 upvotes]: Let $k$ be an algebraically closed field and consider the Zariski topology on $\mathbb A^2_k$ and on $\mathbb P^1_k$.
If
$$X:=\left\{((x_0,x_1),(y_0:y_1))\in\mathbb A^2_k\times \mathbb P^1_k\,\bigg| x_0y_1=x_1y_0\,\right\}\subseteq \mathbb A^2_k\times \mathbb P^1_k$$
I don't understand why $X$ is closed in $\mathbb A^2_k\times \mathbb P^1_k$.
The structure of variety on $\mathbb A^2_k\times \mathbb P^1_k$ is obtained by patching of the affine varieties $\{\mathbb A^2\times U_i\}_{i=0,1}$ where $U_1=\{(x_0:1)\,:x_0\in k\}$ and $U_0=\{(1:x_1)\,:x_1\in k\}$. Now is there some kind of "characterization" for closed sets of $\mathbb A^2_k\times \mathbb P^1_k$?

REPLY [3 votes]: Yes, there is a characterization of closed subsets of $\mathbb A^2_k\times \mathbb P^1_k$.
Namely, they are the common zeros of a family $(f_i(x_0,x_1;y_o,y_1))_{i\in I}$ of polynomials $f_i(x_0,x_1;y_o,y_1)$, required to be homogeneous in the variables $y_0,y_1$ associated to $\mathbb P^1_k$.
The degree of homogeneity of these polynomials may vary with $i\in I$.
Your example is a little confusing (by no fault of yours!) because the polynomial $x_0y_1-x_1y_0$ happens to be homogeneous (of degree $1$) also in the variables $x_0,x_1$ of $\mathbb A^2_k$, which is absolutely not required in general.
This means that your subvariety $X\subset \mathbb A^2_k\times \mathbb P^1_k$ descends to a subvariety $\mathbb P(X)\subset \mathbb P^1_k \times \mathbb P^1_k$.
A geometric interpretation
You have the Plücker embedding $$p:\mathbb P^1_k \times \mathbb P^1_k\hookrightarrow \mathbb P^3_k: ((x_0:x_1),(y_0:y_1))\mapsto (z_0:z_1:z_2:z_3)=(x_0y_0:x_0y_1:x_1y_0:x_1y_1)$$The image $p(\mathbb P(X))\subset \mathbb P^3_k$ of $\mathbb P(X)$ under that embedding is then the intersection of the quadric $z_0z_3-z_1z_2=0$ with the plane $z_1-z_2=0$.
 In other words, a good old projective conic!


TITLE: How to prove that any genus 2 curve is hyperelliptic?
QUESTION [0 upvotes]: How can one prove that any genus $2$ smooth curve is hyperelliptic? Remember that a smooth curve $C$ is called hyperelliptic if there exists a morphism $\phi:C \rightarrow \mathbb{P}^1$ of degree $2$.

REPLY [1 votes]: The hint given by Matt is true. But there are many nontrivial steps to prove your statement. Here is one proof:
Let $K_C$ be a canonical divisor of $C$. Thus, we have that $\mathcal{L}(K_C)\simeq\omega_C$. We know that the canonical sheaf $\omega_{C'}$ on a curve $C'$ of genus $g_{C'}\geq 2$ is generated by global sections. (Still, this is not trivial. The key points for this fact will be at the end of the proof.)
By Lemma II.7.8 of Hartshorne:=[H], we therefore get that $|K_C|$ is base point free since $g_C=2$. Also, $\dim|K_C|=g_C-1=1.$ Hence we have a morphism $\phi: C\rightarrow \mathbb{P}^1$ such that $\mathcal{L}(K_C)\simeq \phi^*(\mathcal{O}(1))$; cf. Remark II.7.8.1 of [H].
Lastly, we have to prove that $\deg(\phi)=2$. By Proposition II.6.9 of [H], we have that $$\deg(\phi)=\deg(\phi)\deg(P)=\deg(\phi^*(P))=\deg(K_C)=2g_C-2=2,$$ where $P\in\mathbb{P^1}.$ Here, $\deg(K_C)$ follows from the Riemann-Roch Theorem. We also used that $\mathcal{O}(1)\simeq\mathcal{L}(P).$ As a conclusion, we have proved that $deg(\phi)=2.$
Addendum for the nontrivial fact:
To prove that $|D|$ is base point free for a divisor $D$ on a curve $C$, it is enough to show that $\ell(D-P)<\ell(D),$ for all closed points $P\in C.$ Hence, our fact can be done by applying Riemann-Roch Theorem to $K_C-P,$ for all closed points $P.$