Révision 217 CSL17/completeness.tex

completeness.tex (revision 217)
76 76 
	}
77 77 
\patrick{I also assume access to the following predicates:
78 78 
\begin{itemize}
79 
   \item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)"
80 
   \item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$"
79 
%   \item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)"
80 
%   \item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$"
81 81 
   \item $\addtosequence(w,y,w')$. "$w'$ represents the sequence obtained by adding $y$ at the end of the sequence represented by $w$". Here we are referring to sequences which can be decoded with predicate $\beta$.
82 82 
\end{itemize}}
83 
Now suppose that $f$ is defined by PRN:
83 
In the following we will use the predicates $\zerobit (u,k)$, $\onebit(u,k)$, $\pref(k,x,y)$ which have been defined in Sect. \ref{sect:graphsbasicfunctions}.
84 

  		





  
  85
  
    
Suppose that $f$ is defined by predicative recursion on notation:


  		





  84
  86
  
    
\[


  		





  85
  87
  
    
\begin{array}{rcl}


  		





  86
  88
  
    
f(0 , \vec u ; \vec x) & \dfn & g(\vec u ; \vec x) \\


  		





  ......




  97
  99
  
    
\begin{array}{ll}


  		





  98
  100
  
    
& 


  		





  99
  101
  
    
%Seq(z) \cand 


  		





  100
  
  
    
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\


  		





  
  102
  
    
\exists^{\safe} y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\


  		





  101
  103
  
    
%\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )\\


  		





  102
  
  
    
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )


  		





  
  104
  
    
\cand & \forall^{\normal}  k < |u| . \exists^{\safe} y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )


  		





  103
  105
  
    
\end{array}


  		





  104
  106
  
    
\right)


  		





  105
  107
  
    
\]


  		












Formats disponibles :
  Unified diff