1: \begin{proof}[Verification of Numerical Checks A through E']

2: For these verifications, we must precisely locate the filled Julia set and some pieces of invariant manifolds. The set-oriented algorithms explained above will be extensively used for this.

3: 

4: The algorithm for computing the filled Julia set is already mentioned; now we explain how to use the graph $G$ defined above to construct an outer approximation of invariant manifolds. Recall that the pieces of invariant manifolds we want to control are defined by nested sequences of the iterations of boxes. For example, we consider 

5: %

6: \[\mathcal{V}^s_{\mathrm{loc}}(p_1)=\mathcal{B}^+_0\cap f^{-1}(\mathcal{B}^+_0\cap \cdots \cap f^{-1}(\mathcal{B}^+_0\cap f^{-1}(\mathcal{B}^+_0))\cdots).\]

7: % 

8: Let $R$ be a rectangle containing $\mathcal{B}^+_0$, and $R = \bigcup_{i \in I} R_i$ be its decomposition into smaller rectangles. Let $G$ be the graph associated to this decomposition and the map $f_{a, b}$. Now we compute $\mathrm{V}^{+\infty}(G)$, the set of vertices $v$ of $G$ such that there exists a one-sided path starting from $v$. Then, again the inclusion:

9: %

10: \[\mathcal{V}^s_{\mathrm{loc}}(p_1) \subset \bigcup_{i \in \mathrm{V}^{+\infty}(G)} R_i\]

11: %

12: rigorously holds. By taking the preimage of this rigorous covering of $\mathcal{V}^s_{\mathrm{loc}}(p_1)$, again using the set-oriented algorithm, we can also construct a rigorous covering of $\mathcal{V}_{31\overline{0}}^s(a, b)^+$. In the same way, a rigorous covering of $\mathcal{V}_{\overline{0}23}^u(a, b)^+$ can be obtained. Thus, by verifying $\frac{\partial}{\partial u}\left\{\pi_u \circ f^2(u, v_0)\right\}\ne 0$ using the interval arithmetic on the intersection of these coverings, we complete the proof of Numerical Check E.

13: 

14: The strategies for the remaining Numerical Checks are similar. 

15: \end{proof}

16: