root / CSL16 / appendix-bc-convergence.tex @ 249
Historique | Voir | Annoter | Télécharger (5,18 ko)
| 1 |
\section{Further proof details for Thm.~\ref{thm:arith-proves-bc-conv}, Sect.~\ref{sect:bc-convergence}}
|
|---|---|
| 2 |
\label{sect:app-bc-conv}
|
| 3 |
|
| 4 |
For derivation \eqref{eqn:prn-cvg-base} $\alpha$ is,
|
| 5 |
\[ |
| 6 |
\vlderivation{
|
| 7 |
% \vliin{\cut}{}{ \word (\vec x) \seqar \word ( g (\vec v ; \vec x)) }{
|
| 8 |
% \vlin{\rigrul{!}}{}{\seqar !\word (v)}{
|
| 9 |
% \vlin{assump}{}{\seqar \word (\vec v)}{\vlhy{}}
|
| 10 |
% } |
| 11 |
% }{
|
| 12 |
\vliin{\cut}{}{ !\word (\vec v ) , \word (\vec x) \seqar \word (g (\vec v ; \vec x )) }{
|
| 13 |
\vlhy{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x)) }
|
| 14 |
}{
|
| 15 |
\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 )) }{
|
| 16 |
\vlin{\id}{}{\word (g(\vec v ; \vec x )) \seqar \word (g(\vec v ; \vec x ))}{\vlhy{}}
|
| 17 |
} |
| 18 |
} |
| 19 |
% } |
| 20 |
} |
| 21 |
\] |
| 22 |
and $\beta$ is: |
| 23 |
\[ |
| 24 |
\hspace{-1em}
|
| 25 |
\small |
| 26 |
\vlderivation{
|
| 27 |
\vliin{\cut}{}{!\word (\vec v) , \word (\vec x) \seqar \word ( f ( \epsilon , \vec v ; \vec x ) ) }{
|
| 28 |
\vlhy{!\word (\vec v) , \word (\vec x) \seqar \word (g (\vec v ; \vec x) ) }
|
| 29 |
}{
|
| 30 |
\vliin{\cut}{}{ \word (g (\vec v ; \vec x) ) \seqar \word (f (\epsilon, \vec v ; \vec x) ) }{
|
| 31 |
\vlin{\closure{\eqspec}}{}{ \seqar f(\epsilon , \vec v ; \vec x) = g(\vec v ; \vec x) }{\vlhy{}}
|
| 32 |
}{
|
| 33 |
\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{}}
|
| 34 |
} |
| 35 |
} |
| 36 |
} |
| 37 |
\] |
| 38 |
|
| 39 |
Suppose $f$ is defined by safe composition as follows: |
| 40 |
\[ |
| 41 |
f( \vec u ; \vec x ) |
| 42 |
\quad = \quad |
| 43 |
h( \vec g (\vec u ; ) ; \vec g' ( \vec u ; \vec x ) ) |
| 44 |
\] |
| 45 |
|
| 46 |
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: |
| 47 |
\[ |
| 48 |
\hspace{-1em}
|
| 49 |
\tiny |
| 50 |
\vlderivation{
|
| 51 |
\vliq{\rigrul{\forall}}{}{ \seqar \forall\vec u^{!\word} . \forall \vec x^\word . \word( f(\vec u ; \vec x ) ) }{
|
| 52 |
\vliq{\beta}{}{ !\word (\vec u) , \word (\vec x) \seqar \word ( f( \vec u ; \vec x ) ) }{
|
| 53 |
\vliq{\cntr}{}{ !\word (\vec u) , \word (\vec x) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x ) ) ) }{
|
| 54 |
\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 ) ) ) }{
|
| 55 |
\vlhy{
|
| 56 |
\left\{
|
| 57 |
\vlderivation{
|
| 58 |
\vlin{\rigrul{!}}{}{ !\word (\vec u) \seqar !\word ( g_i (\vec u ;) ) }{
|
| 59 |
\vliq{\alpha}{}{ !\word (\vec u) \seqar \word ( g_i (\vec u ;) }{
|
| 60 |
\vltr{\IH}{ \forall \vec u^{!\word} . \word (g_i (\vec u ;) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 61 |
} |
| 62 |
} |
| 63 |
} |
| 64 |
\right\}_{i \leq |\vec g| }
|
| 65 |
} |
| 66 |
}{
|
| 67 |
\vlhy{
|
| 68 |
\left\{
|
| 69 |
\vlderivation{
|
| 70 |
\vliq{\alpha}{}{ !\word ( \vec u ) , \word (\vec x) \seqar \word ( g_j' ( \vec u ; \vec x ) ) }{
|
| 71 |
\vltr{\IH}{ \seqar \forall \vec u^{!\word}. \forall \vec x^\word . \word ( g_j' (\vec u ; \vec x) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 72 |
} |
| 73 |
} |
| 74 |
\right\}_{j \leq |\vec g'|}
|
| 75 |
} |
| 76 |
}{
|
| 77 |
\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 ) ) ) ) }{
|
| 78 |
\vltr{\IH}{ \seqar \forall \vec v^{!\word} . \forall \vec y^\word . \word ( h( \vec v ; \vec y ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 79 |
} |
| 80 |
} |
| 81 |
} |
| 82 |
} |
| 83 |
} |
| 84 |
} |
| 85 |
\] |
| 86 |
where $\alpha$ and $\beta$ are similar to before. |
| 87 |
|
| 88 |
|
| 89 |
We also give the case of the conditional initial function $C (; x, y_\epsilon , y_0, y_1)$, to exemplify the use of additives. |
| 90 |
%The conditional is defined equationally as: |
| 91 |
%\[ |
| 92 |
%\begin{array}{rcl}
|
| 93 |
%C (; \epsilon, y_\epsilon , y_0, y_1 ) & = & y_\epsilon \\ |
| 94 |
%C(; \succ_0 x , y_\epsilon , y_0, y_1) & = & y_0 \\ |
| 95 |
%C(; \succ_1 x , y_\epsilon , y_0, y_1) & = & y_1 |
| 96 |
%\end{array}
|
| 97 |
%\] |
| 98 |
Let $\vec y = ( y_\epsilon , y_0, y_1 )$ and construct the required proof as follows: |
| 99 |
\[ |
| 100 |
\small |
| 101 |
\vlderivation{
|
| 102 |
\vliq{}{}{ \word (x) , \word (\vec y) \seqar \word ( C(; x ,\vec y) )}{
|
| 103 |
\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{
|
| 104 |
\vlderivation{
|
| 105 |
\vliq{}{}{ x = \epsilon , \word (\vec y) \seqar \word ( C(; x , \vec y) ) }{
|
| 106 |
\vliq{}{}{ \word (\vec y) \seqar \word ( C( ; \epsilon , \vec y ) ) }{
|
| 107 |
\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_\epsilon) }{
|
| 108 |
\vlin{\id}{}{\word (y_\epsilon) \seqar \word ( y_\epsilon )}{\vlhy{}}
|
| 109 |
} |
| 110 |
} |
| 111 |
} |
| 112 |
} |
| 113 |
\qquad |
| 114 |
\left\{
|
| 115 |
\vlderivation{
|
| 116 |
\vlin{\lefrul{\exists}}{}{ \exists z^\word . x = \succ_i z , \word (\vec y) \seqar \word ( C(;x , \vec y) ) }{
|
| 117 |
\vliq{}{}{ x = \succ_i a , \word (\vec y ) \seqar \word (C(; x ,\vec y)) }{
|
| 118 |
\vliq{}{}{ \word (\vec y) \seqar \word ( C(; \succ_i a , \vec y ) ) }{
|
| 119 |
\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_i) }{
|
| 120 |
\vlin{\id}{}{\word (y_i) \seqar \word (y_i)}{\vlhy{}}
|
| 121 |
} |
| 122 |
} |
| 123 |
} |
| 124 |
} |
| 125 |
} |
| 126 |
\right\}_{i = 0,1}
|
| 127 |
} |
| 128 |
} |
| 129 |
} |
| 130 |
} |
| 131 |
\] |
| 132 |
whence the result follows by $\forall$-introduction. |
| 133 |
%The other initial functions are routine. |