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