root / CSL16 / draft / bc-convergence.tex @ 238
Historique | Voir | Annoter | Télécharger (14,24 ko)
| 1 |
|
|---|---|
| 2 |
\section{Convergence of Bellantoni-Cook programs in $\arith$}
|
| 3 |
\label{sect:bc-convergence}
|
| 4 |
%\anupam{In this section, use whatever form of the deduction theorem is necessary and reverse engineer precise statement later.}
|
| 5 |
|
| 6 |
In this section we show that $I\sigzer$, and so also $\arith$, proves the convergence of any equational specification induced by a BC program. Since BC programs can compute any polynomial-time function, we obtain a completeness result. In the next section we will show the converse, that any provably convergent function of $\arith$ is polynomial-time computable. |
| 7 |
|
| 8 |
The underlying construction of the proof here is similar in spirit to those occurring in \cite{Cantini02} and \cite{Leivant94:found-delin-ptime}. In fact, like in those works, only quantifier-free positive induction is required, but here we moreover must take care to respect additive and multiplicative behaviour of linear connectives, thereby achieving a somewhat stronger result.
|
| 9 |
|
| 10 |
We will assume the formulation of BC programs with regular PRN, not simultaneous PRN. |
| 11 |
|
| 12 |
|
| 13 |
%\subsection{Convergence in arithmetic}
|
| 14 |
|
| 15 |
%\begin{theorem}
|
| 16 |
% [Convergence] |
| 17 |
% If $\Phi(f)$ is an equational specification corresponding to a BC-program defining $f$, then $\cax{\Sigma^N_1}{\pind} \proves \ !\Phi(f) \limp \forall \vec{x}^{!N} . N(f(\vec x))$.
|
| 18 |
%\end{theorem}
|
| 19 |
|
| 20 |
%We first want to show that the system ${\Sigma^{\word}_1}-{\pind}$ is expressive enough, that is to say that all polynomial-time functions can be represented by some equational specifications that are provably total. To do so we consider equational specifications of BC-programs.
|
| 21 |
\begin{theorem}
|
| 22 |
% [Convergence] |
| 23 |
\label{thm:arith-proves-bc-conv}
|
| 24 |
If $\eqspec$ is a BC program defining a function $f$, then $I\sigzer$ proves $\conv(f, \eqspec)$. |
| 25 |
\end{theorem}
|
| 26 |
|
| 27 |
\anupam{Consider informalising some of these arguments under (some version of) the deduction theorem. Formal stuff can be put in an appendix. Maybe add a remark somewhere about arguing informally under deduction, taking care for non-modalised formulae.}
|
| 28 |
|
| 29 |
\begin{proof}
|
| 30 |
% We write function symbols in $\arith$ with arguments delimited by $;$, as for BC-programs. |
| 31 |
We appeal to Lemma~\ref{lemma:spec-norm-form} and show that $\closure{\eqspec} \cup I\sigzer$ proves,
|
| 32 |
\begin{equation}
|
| 33 |
\label{eqn:prv-cvg-ih}
|
| 34 |
\forall \vec{u}^{!\word} . \forall \vec{x}^\word . \word(f(\vec u ; \vec x))
|
| 35 |
\end{equation}
|
| 36 |
We proceed by induction on the structure of a BC program for $f$. |
| 37 |
% We give some key cases in what follows. |
| 38 |
|
| 39 |
Suppose $f$ is defined by PRN as: |
| 40 |
\[ |
| 41 |
\begin{array}{rcl}
|
| 42 |
f(0,\vec v ; \vec x) & = & g(\vec v ; \vec x) \\ |
| 43 |
f(\succ_i u , \vec v; \vec x) & = & h_i (u, \vec v ; \vec x , f(u , \vec v ; \vec x)) |
| 44 |
\end{array}
|
| 45 |
\] |
| 46 |
By the inductive hypothesis we already have \eqref{eqn:prv-cvg-ih} for $g,h_0,h_1$ in place of $f$. We construct the following proof:
|
| 47 |
\begin{equation}
|
| 48 |
\label{eqn:prn-cvg-base}
|
| 49 |
\vlderivation{
|
| 50 |
\vliq{\beta}{}{!\word(\vec v) , \word (\vec x) \seqar \word(f (\epsilon , \vec v ; \vec x)) }{
|
| 51 |
\vliq{\alpha}{}{!\word (\vec v) , \word (\vec x) \seqar \word (g (\vec v ; \vec x) ) }{
|
| 52 |
\vltr{\IH}{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x)) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 53 |
} |
| 54 |
} |
| 55 |
} |
| 56 |
\end{equation}
|
| 57 |
where $\alpha$ is, |
| 58 |
\[ |
| 59 |
\vlderivation{
|
| 60 |
% \vliin{\cut}{}{ \word (\vec x) \seqar \word ( g (\vec v ; \vec x)) }{
|
| 61 |
% \vlin{\rigrul{!}}{}{\seqar !\word (v)}{
|
| 62 |
% \vlin{assump}{}{\seqar \word (\vec v)}{\vlhy{}}
|
| 63 |
% } |
| 64 |
% }{
|
| 65 |
\vliin{\cut}{}{ !\word (\vec v ) , \word (\vec x) \seqar \word (g (\vec v ; \vec x )) }{
|
| 66 |
\vlhy{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x)) }
|
| 67 |
}{
|
| 68 |
\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 )) }{
|
| 69 |
\vlin{\id}{}{\word (g(\vec v ; \vec x )) \seqar \word (g(\vec v ; \vec x ))}{\vlhy{}}
|
| 70 |
} |
| 71 |
} |
| 72 |
% } |
| 73 |
} |
| 74 |
\] |
| 75 |
and $\beta$ is: |
| 76 |
\[ |
| 77 |
\vlderivation{
|
| 78 |
\vliin{\cut}{}{!\word (\vec v) , \word (\vec x) \seqar \word ( f ( \epsilon , \vec v ; \vec x ) ) }{
|
| 79 |
\vlhy{!\word (\vec v) , \word (\vec x) \seqar \word (g (\vec v ; \vec x) ) }
|
| 80 |
}{
|
| 81 |
\vliin{\cut}{}{ \word (g (\vec v ; \vec x) ) \seqar \word (f (\epsilon, \vec v ; \vec x) ) }{
|
| 82 |
\vlin{\closure{\eqspec}}{}{ \seqar f(\epsilon , \vec v ; \vec x) = g(\vec v ; \vec x) }{\vlhy{}}
|
| 83 |
}{
|
| 84 |
\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{}}
|
| 85 |
} |
| 86 |
} |
| 87 |
} |
| 88 |
\] |
| 89 |
|
| 90 |
% We first prove, |
| 91 |
% \begin{equation}
|
| 92 |
% !\word (a) , !\word (\vec v) , \word (\vec x) \land \word (f( a , \vec v ; \vec x ) ) |
| 93 |
% \seqar |
| 94 |
% \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) ) |
| 95 |
% \end{equation}
|
| 96 |
% for $i=0,1$, whence we will apply $\ind$. We construct the following proofs: |
| 97 |
|
| 98 |
We also construct, for $i=0,1$, the proofs, |
| 99 |
\begin{equation}
|
| 100 |
\label{eqn:prn-cvg-ind}
|
| 101 |
%\vlderivation{
|
| 102 |
% \vlin{\rigrul{\limp}}{}{ \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) ) \seqar \word (\vec x) \limp \word( f(\succ_i u , \vec v ; \vec x) ) }{
|
| 103 |
% \vliq{\gamma}{}{\word(\vec x), \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) ) \seqar \word( f(\succ_i u , \vec v ; \vec x) ) }{
|
| 104 |
% \vliin{\lefrul{\limp}}{}{\word(\vec x), \word(\vec x), \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) ) \seqar \word( f(\succ_i u , \vec v ; \vec x) ) }{
|
| 105 |
% \vlin{\id}{}{\word(\vec x) \seqar \word (\vec x) }{\vlhy{}}
|
| 106 |
% }{
|
| 107 |
% \vliq{\beta}{}{ \word (\vec x) , \word (f(u , \vec v ; \vec x) ) \seqar \word ( f(\succ_i u , \vec v ; \vec x) ) }{
|
| 108 |
% \vliq{\alpha}{}{ \word (\vec x) , \word (f(u , \vec v ; \vec x) ) \seqar \word ( h_i( u , \vec v ; \vec x , f( u, \vec v ; \vec x )) ) }{
|
| 109 |
% \vltr{IH}{ \seqar \forall u^{!\word}, \vec v^{!\word} . \forall \vec x^\word , y^\word . \word( h_i (u, \vec v ; \vec x, y) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 110 |
% } |
| 111 |
% } |
| 112 |
% } |
| 113 |
% } |
| 114 |
% } |
| 115 |
% } |
| 116 |
\vlderivation{
|
| 117 |
\vlin{\lefrul{\land}}{}{ !\word (a) , !\word (\vec v) , \word (\vec x) \land \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) ) }{
|
| 118 |
\vlin{\lefrul{\cntr}}{}{ !\word (a) , !\word (\vec v) , \word (\vec x) , \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )}{
|
| 119 |
\vliin{\rigrul{\land}}{}{ !\word (a) , !\word (\vec v) , \word(\vec x), \word (\vec x) , \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )}{
|
| 120 |
\vlin{\id}{}{\word (\vec x) \seqar \word (\vec x)}{\vlhy{}}
|
| 121 |
}{
|
| 122 |
\vliq{\beta}{}{ !\word (u) , !\word(\vec v) , \word (\vec x) , \word (f ( u , \vec v ; \vec x ) ) \seqar \word (f (\succ_i u , \vec{v} ; \vec x ) ) }{
|
| 123 |
\vliq{\alpha}{}{ !\word (u) , !\word (\vec v) , \word (\vec x) , \word (f ( u , \vec v ; \vec x ) ) \seqar \word ( h_i ( u , \vec v ; \vec x , f( u , \vec v ; \vec x ) ) ) }{
|
| 124 |
\vltr{\IH}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word , y^\word . \word ( h_i ( u, \vec v ; \vec x, y ) ) }{ \vlhy{\quad} }{\vlhy{}}{\vlhy{\quad}}
|
| 125 |
} |
| 126 |
} |
| 127 |
} |
| 128 |
} |
| 129 |
} |
| 130 |
} |
| 131 |
\end{equation}
|
| 132 |
where $\alpha$ and $\beta$ are constructed similarly to before. |
| 133 |
|
| 134 |
%% so let us suppose that $\word(\vec v)$ and prove, |
| 135 |
% \begin{equation}
|
| 136 |
%% \forall u^{!\word} . (\word(\vec x) \limp \word(f(u , \vec v ; \vec x) )
|
| 137 |
%!\word (u) , !\word (\vec v) , \word (\vec x) \seqar \word ( f(u, \vec v ; \vec x) ) |
| 138 |
% \end{equation}
|
| 139 |
% by $\cax{\Sigma^N_1}{\pind}$ on $u$. After this the result will follow by $\forall$-introduction for $u, \vec v , \vec x$.
|
| 140 |
|
| 141 |
% In the base case we have the following proof, |
| 142 |
% \[ |
| 143 |
% \vlderivation{
|
| 144 |
% \vlin{\rigrul{\limp}}{}{ \seqar \word (\vec x) \limp \word (f(\epsilon , \vec v ; \vec x )) }{
|
| 145 |
% \vliq{\beta}{}{ \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x) ) }{
|
| 146 |
% \vliq{\alpha}{}{ \word (\vec x) \seqar \word ( g (\vec v ; \vec x) ) }{
|
| 147 |
% \vltr{IH}{\seqar \forall v^{!\word} . \forall x^\word . \word( g(\vec v ; \vec x) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 148 |
% } |
| 149 |
% } |
| 150 |
% } |
| 151 |
% } |
| 152 |
|
| 153 |
|
| 154 |
Finally we compose these proofs as follows: |
| 155 |
|
| 156 |
\[ |
| 157 |
\vlderivation{
|
| 158 |
\vliq{\rigrul{\forall}}{}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word . \word ( f(u , \vec v ;\vec x) ) }{
|
| 159 |
\vliq{\lefrul{\cntr}}{}{ !\word (u), !\word (\vec v) , \word (\vec x) \seqar \word ( f(u , \vec v ;\vec x) ) }
|
| 160 |
{
|
| 161 |
\vliin{\cut}{}{ !\word (u), !\word(\vec v), !\word (\vec v) , \word (\vec x) , \word (\vec x) \seqar \word ( f(u , \vec v ;\vec x) ) }{
|
| 162 |
\vltr{}{ !\word (\vec v) , \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 163 |
} |
| 164 |
{
|
| 165 |
\vliq{\wk}{}{ !\word (u), !\word (\vec v) , \word (\vec x), \word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word ( f( u , \vec v ; \vec x ) ) }{
|
| 166 |
\vliq{\land\text{-}\mathit{inv}}{}{ !\word (u), !\word (\vec v) , \word (\vec x) ,\word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( u , \vec v ; \vec x ) ) }{
|
| 167 |
\vlin{\ind}{}{ !\word (u), !\word (\vec v) , \word (\vec x) \land \word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( u , \vec v ; \vec x ) ) }
|
| 168 |
{
|
| 169 |
\vlhy{
|
| 170 |
\left\{
|
| 171 |
\vltreeder{}{ !\word (a), !\word (\vec v) , \word (\vec x) \word ( f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( \succ_i u , \vec v ; \vec x ) ) }{\quad}{}{}
|
| 172 |
\right\}_{i=0,1}
|
| 173 |
} |
| 174 |
} |
| 175 |
} |
| 176 |
} |
| 177 |
} |
| 178 |
} |
| 179 |
} |
| 180 |
} |
| 181 |
\] |
| 182 |
where the steps \todo{minor steps}
|
| 183 |
|
| 184 |
%For the inductive step, we suppose that $\word (u)$ and the proof is as follows, |
| 185 |
% |
| 186 |
%where the steps indicated $\alpha$ and $\beta$ are analogous to those for the base case. |
| 187 |
%%, and $\gamma$ is an instance of the general scheme: |
| 188 |
%%\begin{equation}
|
| 189 |
%%\label{eqn:nat-cntr-left-derivation}
|
| 190 |
%%\vlderivation{
|
| 191 |
%% \vliin{\cut}{}{ \word (t) , \Gamma \seqar \Delta }{
|
| 192 |
%% \vlin{\wordcntr}{}{ \word (t) \seqar \word (t) \land \word (t) }{\vlhy{}}
|
| 193 |
%% }{
|
| 194 |
%% \vlin{\lefrul{\land}}{}{\word (t) \land \word (t) , \Gamma \seqar \Delta}{ \vlhy{\word (t) ,\word (t) , \Gamma \seqar \Delta} }
|
| 195 |
%% } |
| 196 |
%% } |
| 197 |
%%\end{equation}
|
| 198 |
% |
| 199 |
%% |
| 200 |
%%For the inductive step, we need to show that, |
| 201 |
%%\[ |
| 202 |
%%\forall x^{!N} . (( N(\vec y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N(\vec y) \limp N(f(\succ_i x , \vec x ; \vec y) ) )
|
| 203 |
%%\] |
| 204 |
%%so let us suppose that $N(x)$ and we give the following proof: |
| 205 |
%%\[ |
| 206 |
%%\vlderivation{
|
| 207 |
%% \vlin{N\cntr}{}{N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y) ) }{
|
| 208 |
%% \vliin{}{}{N(y) \limp N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y) ) }{
|
| 209 |
%% \vliin{}{}{ N(y) \limp N(y) \limp ( N(y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N( h_i (x , \vec x ; \vec y , f(x , \vec x ; \vec y) ) ) }{
|
| 210 |
%% \vltr{MLL}{( N(\vec y) \limp (N (\vec y) \limp N(f(x, \vec x ; \vec y) )) \limp N(f(x, \vec x ; \vec y)) }{\vlhy{\quad }}{\vlhy{\ }}{\vlhy{\quad }}
|
| 211 |
%% }{
|
| 212 |
%% \vlhy{2}
|
| 213 |
%% } |
| 214 |
%% }{
|
| 215 |
%% \vlhy{3}
|
| 216 |
%%} |
| 217 |
%%} |
| 218 |
%%} |
| 219 |
%%\] |
| 220 |
%%TOFINISH |
| 221 |
|
| 222 |
Suppose $f$ is defined by safe composition as follows: |
| 223 |
\[ |
| 224 |
f( \vec u ; \vec x ) |
| 225 |
\quad = \quad |
| 226 |
h( \vec g (\vec u ; ) ; \vec g' ( \vec u ; \vec x ) ) |
| 227 |
\] |
| 228 |
|
| 229 |
By the inductive hypothesis we already have \eqref{eqn:prv-cvg-ih} for $h$ and each $g_i$ and $g_j'$ in place of $f$. We construct the required proof as follows:
|
| 230 |
\[ |
| 231 |
\vlderivation{
|
| 232 |
\vliq{\rigrul{\forall}}{}{ \seqar \forall\vec u^{!\word} . \forall \vec x^\word . \word( f(\vec u ; \vec x ) ) }{
|
| 233 |
\vliq{\beta}{}{ !\word (\vec u) , \word (\vec x) \seqar \word ( f( \vec u ; \vec x ) ) }{
|
| 234 |
\vliq{\cntr}{}{ !\word (\vec u) , \word (\vec x) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x ) ) ) }{
|
| 235 |
\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 ) ) ) }{
|
| 236 |
\vlhy{
|
| 237 |
\left\{
|
| 238 |
\vlderivation{
|
| 239 |
\vlin{\rigrul{!}}{}{ !\word (\vec u) \seqar !\word ( g_i (\vec u ;) ) }{
|
| 240 |
\vliq{\alpha}{}{ !\word (\vec u) \seqar \word ( g_i (\vec u ;) }{
|
| 241 |
\vltr{\IH}{ \forall \vec u^{!\word} . \word (g_i (\vec u ;) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 242 |
} |
| 243 |
} |
| 244 |
} |
| 245 |
\right\}_{i \leq |\vec g| }
|
| 246 |
} |
| 247 |
}{
|
| 248 |
\vlhy{
|
| 249 |
\left\{
|
| 250 |
\vlderivation{
|
| 251 |
\vliq{\alpha}{}{ !\word ( \vec u ) , \word (\vec x) \seqar \word ( g_j' ( \vec u ; \vec x ) ) }{
|
| 252 |
\vltr{\IH}{ \seqar \forall \vec u^{!\word}. \forall \vec x^\word . \word ( g_j' (\vec u ; \vec x) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 253 |
} |
| 254 |
} |
| 255 |
\right\}_{j \leq |\vec g'|}
|
| 256 |
} |
| 257 |
}{
|
| 258 |
\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 ) ) ) ) }{
|
| 259 |
\vltr{\IH}{ \seqar \forall \vec v^{!\word} . \forall \vec y^\word . \word ( h( \vec v ; \vec y ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 260 |
} |
| 261 |
} |
| 262 |
} |
| 263 |
} |
| 264 |
} |
| 265 |
} |
| 266 |
\] |
| 267 |
where $\alpha$ and $\beta$ are similar to before. |
| 268 |
|
| 269 |
\todo{reformat a bit}
|
| 270 |
|
| 271 |
It remains to check the initial functions. |
| 272 |
|
| 273 |
Consider the conditional function, defined equationally as: |
| 274 |
\[ |
| 275 |
\begin{array}{rcl}
|
| 276 |
C (; \epsilon, y_\epsilon , y_0, y_1 ) & = & y_\epsilon \\ |
| 277 |
C(; \succ_0 x , y_\epsilon , y_0, y_1) & = & y_0 \\ |
| 278 |
C(; \succ_1 x , y_\epsilon , y_0, y_1) & = & y_1 |
| 279 |
\end{array}
|
| 280 |
\] |
| 281 |
Let $\vec y = ( y_\epsilon , y_0, y_1 )$ and construct the required proof as follows: |
| 282 |
\[ |
| 283 |
\vlderivation{
|
| 284 |
\vliq{}{}{ \word (x) , \word (\vec y) \seqar \word ( C(; x ,\vec y) )}{
|
| 285 |
\vliin{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) ) }{
|
| 286 |
\vliq{}{}{ x = \epsilon , \word (\vec y) \seqar \word ( C(; x , \vec y) ) }{
|
| 287 |
\vliq{}{}{ \word (\vec y) \seqar \word ( C( ; \epsilon , \vec y ) ) }{
|
| 288 |
\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_\epsilon) }{
|
| 289 |
\vlin{\id}{}{\word (y_\epsilon) \seqar \word ( y_\epsilon )}{\vlhy{}}
|
| 290 |
} |
| 291 |
} |
| 292 |
} |
| 293 |
}{
|
| 294 |
\vlhy{
|
| 295 |
\left\{
|
| 296 |
\vlderivation{
|
| 297 |
\vlin{\lefrul{\exists}}{}{ \exists z^\word . x = \succ_i z , \word (\vec y) \seqar \word ( C(;x , \vec y) ) }{
|
| 298 |
\vliq{}{}{ x = \succ_i a , \word (\vec y ) \seqar \word (C(; x ,\vec y)) }{
|
| 299 |
\vliq{}{}{ \word (\vec y) \seqar \word ( C(; \succ_i a , \vec y ) ) }{
|
| 300 |
\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_i) }{
|
| 301 |
\vlin{\id}{}{\word (y_i) \seqar \word (y_i)}{\vlhy{}}
|
| 302 |
} |
| 303 |
} |
| 304 |
} |
| 305 |
} |
| 306 |
} |
| 307 |
\right\}_{i = 0,1}
|
| 308 |
} |
| 309 |
} |
| 310 |
} |
| 311 |
} |
| 312 |
\] |
| 313 |
whence the result follows by $\forall$-introduction. |
| 314 |
\todo{reformat a bit}
|
| 315 |
|
| 316 |
Other initial functions are far simpler. |
| 317 |
|
| 318 |
\end{proof}
|
| 319 |
|
| 320 |
|
| 321 |
|
| 322 |
|
| 323 |
|
| 324 |
|
| 325 |
|
| 326 |
|
| 327 |
|
| 328 |
|
| 329 |
|
| 330 |
|
| 331 |
|
| 332 |
|
| 333 |
|
| 334 |
|
| 335 |
|
| 336 |
|
| 337 |
|
| 338 |
|
| 339 |
|
| 340 |
|
| 341 |
|
| 342 |
|
| 343 |
|
| 344 |
|
| 345 |
|
| 346 |
|
| 347 |
|
| 348 |
|
| 349 |
|
| 350 |
|
| 351 |
|
| 352 |
|
| 353 |
|
| 354 |
|
| 355 |
|
| 356 |
|
| 357 |
|
| 358 |
|
| 359 |
|
| 360 |
|