\section{Further proof details for Thm.~\ref{thm:arith-proves-bc-conv}, Sect.~\ref{sect:bc-convergence}}
\label{sect:app-bc-conv}

For derivation \eqref{eqn:prn-cvg-base} $\alpha$ is,
	\[
	\vlderivation{
	%	\vliin{\cut}{}{ \word (\vec x) \seqar \word ( g (\vec v ; \vec x)) }{
	%		\vlin{\rigrul{!}}{}{\seqar !\word (v)}{
	%			\vlin{assump}{}{\seqar \word (\vec v)}{\vlhy{}}
	%			}
	%		}{
			\vliin{\cut}{}{ !\word (\vec v ) , \word (\vec x) \seqar \word (g (\vec v ; \vec x )) }{
				\vlhy{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x)) }
				}{
				\vliq{\lefrul{\forall}}{  }{ !\word (\vec v) , \word (\vec x) , \forall \vec v^{!\word} . \forall \vec x^\word \word (g(\vec v ; \vec x )) \seqar \word (g(\vec v ; \vec x )) }{
					\vlin{\id}{}{\word (g(\vec v ; \vec x )) \seqar \word (g(\vec v ; \vec x ))}{\vlhy{}}
					}
				}
	%		}
		}
	\]
	and $\beta$ is:
	\[
	\hspace{-1em}
	\small
	\vlderivation{
		\vliin{\cut}{}{!\word (\vec v) , \word (\vec x) \seqar \word ( f ( \epsilon , \vec v ; \vec x ) ) }{
			\vlhy{!\word (\vec v) , \word (\vec x) \seqar \word (g (\vec v ; \vec x) ) }
			}{
			\vliin{\cut}{}{ \word (g (\vec v ; \vec x) ) \seqar \word (f (\epsilon, \vec v ; \vec x) ) }{
				\vlin{\closure{\eqspec}}{}{ \seqar f(\epsilon , \vec v ; \vec x) = g(\vec v ; \vec x) }{\vlhy{}}
				}{
				\vlin{=}{}{\word ( g(\vec v ; \vec x) ) , f(\epsilon , \vec v ; \vec x) = g(\vec v ; \vec x)  \seqar \word (f (\epsilon, \vec v ; \vec x) ) }{\vlhy{}}
				}
			}
		}
	\]
	
	Suppose $f$ is defined by safe composition as follows:
	\[
	f( \vec u ; \vec x )
	\quad = \quad
	h( \vec g (\vec u ; )  ; \vec g' ( \vec u ; \vec x ) )
	\]
	
	By the inductive hypothesis we already have proofs of the covergence of $h$ and each $g_i$ and $g_j'$. Thus we construct the required proof as follows:
	\[
	\hspace{-1em}
	\tiny
	\vlderivation{
		\vliq{\rigrul{\forall}}{}{ \seqar \forall\vec u^{!\word} . \forall \vec x^\word . \word( f(\vec u ; \vec x ) ) }{
			\vliq{\beta}{}{ !\word (\vec u) , \word (\vec x) \seqar \word ( f( \vec u ; \vec x ) ) }{
				\vliq{\cntr}{}{  !\word (\vec u) , \word (\vec x) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x )  ) )  }{
					\vliiiq{\cut}{}{!\word (\vec u) , \dots ,  !\word (\vec u) , \word (\vec x) , \dots , \word (\vec x) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x )  ) )   }{
						\vlhy{
							\left\{  
							\vlderivation{
								\vlin{\rigrul{!}}{}{ !\word (\vec u) \seqar !\word ( g_i (\vec u ;) ) }{
									\vliq{\alpha}{}{ !\word (\vec u) \seqar \word ( g_i (\vec u ;) }{
										\vltr{\IH}{ \forall \vec u^{!\word} . \word (g_i (\vec u ;) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
										}
									}
								}
							\right\}_{i \leq |\vec g| }
							}
						}{
						\vlhy{
							\left\{
							\vlderivation{
								\vliq{\alpha}{}{ !\word ( \vec u )  , \word (\vec x) \seqar \word  ( g_j' ( \vec u ; \vec x ) ) }{
									\vltr{\IH}{ \seqar \forall \vec u^{!\word}. \forall \vec x^\word . \word ( g_j' (\vec u ; \vec x) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
									}
								}
							\right\}_{j \leq |\vec g'|}
							}
						}{
						\vliq{\alpha}{}{ !\word ( \vec g (\vec u ;) ) , \word ( \vec g ' ( \vec u ; \vec x ) ) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x )  )  ) ) }{
							\vltr{\IH}{ \seqar \forall \vec v^{!\word} . \forall \vec y^\word . \word ( h( \vec v ; \vec y ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
							}
						}
					}
				}
			}
		}
	\]
	where $\alpha$ and $\beta$ are similar to before.
	
	
	We also give the case of the conditional initial function $C (; x, y_\epsilon , y_0, y_1)$, to exemplify the use of additives. 
	%The conditional is defined equationally as:
	%\[
	%\begin{array}{rcl}
	%C (; \epsilon, y_\epsilon , y_0, y_1  ) & = & y_\epsilon \\
	%C(; \succ_0 x , y_\epsilon , y_0, y_1) & = & y_0 \\
	%C(; \succ_1 x , y_\epsilon , y_0, y_1) & = & y_1 
	%\end{array}
	%\]
	Let $\vec y = ( y_\epsilon , y_0, y_1 )$ and construct the required proof as follows:
	\[
	\small
	\vlderivation{
		\vliq{}{}{ \word (x) , \word (\vec y) \seqar \word ( C(; x ,\vec y) )}{
			\vlin{2\cdot \laor}{}{ x = \epsilon \laor \exists z^\word . x = \succ_0 z \laor \exists z^\word x = \succ_1 z , \word (\vec y) \seqar \word ( C(;x \vec y) ) }{ \vlhy{
				\vlderivation{
				\vliq{}{}{ x = \epsilon , \word (\vec y) \seqar \word ( C(; x , \vec y) ) }{
									\vliq{}{}{ \word (\vec y) \seqar \word ( C( ; \epsilon , \vec y ) ) }{
										\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_\epsilon) }{ 
											\vlin{\id}{}{\word (y_\epsilon) \seqar \word ( y_\epsilon )}{\vlhy{}}
										}
									}
								}
				}
\qquad
				\left\{ 
				\vlderivation{
					\vlin{\lefrul{\exists}}{}{ \exists z^\word . x = \succ_i z , \word (\vec y) \seqar \word ( C(;x , \vec y) ) }{
						\vliq{}{}{ x = \succ_i a , \word (\vec y ) \seqar \word (C(; x ,\vec y)) }{
							\vliq{}{}{ \word (\vec y) \seqar \word ( C(; \succ_i a , \vec y ) ) }{
								\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_i) }{
									\vlin{\id}{}{\word (y_i) \seqar \word (y_i)}{\vlhy{}}
								}
							}
						}
					}
				}
				\right\}_{i = 0,1}
			}
		}
	}
}
\]
whence the result follows by $\forall$-introduction.
%The other initial functions are routine.