CS486 Problem Set 11 DUE: 5/01/03

=

1.

We show that all functions that are representable in the theory $\mathcal{Q}$ are computable. Recall that an $n$-ary function $f: \mathbb{N}^n \to \mathbb{N}$ is representable in the theory $\mathcal{Q}$ if there is an $(n+1)$-ary predicate $R_f$, such that for all $x_1, \ldots, x_n \in \mathbb{N}$:

• $f(x_1,\ldots,x_n)=y$ implies $\models_{\mathcal{Q}}~ R_f\left(\underline{x_1}, \ldots,\underline{x_n}, \underline{y}\right)$.
• $f(x_1,\ldots,x_n)\neq y$ implies $\models_{\mathcal{Q}}~ \sim R_f\left(\underline{x_1}, \ldots,\underline{x_n}, \underline{y}\right)$.

Furthermore, recall that the theory $\mathcal{Q}$ is finitely axiomatizable; hence, it is possible (i.e., computable) to enumerate all of the derivations that follow from the axioms of $\mathcal{Q}$. Therefore, to calculate $f(x_1,\ldots,x_n)$, it suffices to search for a $y$ such that there exists a proof of $R_f(\underline{x_1}, \ldots,\underline{x_n},\underline{y})$.

2.

Let $B_1(x)$ and $B_2(x)$ be formulas in the language $\mathcal{Q}$ with $x$ as the sole free variable. We show how to construct formulas $G_1$ and $G_2$ such that

$$\models_{\mathcal{Q}} G_1 \Leftrightarrow B_1\left(\left\l... ...Leftrightarrow B_2\left(\left\lceil G_1 \right\rceil\right)$$

Recall that $\mathcal{Q}$ is a theory in which $diag$ is representable. Hence, by the Diagonal Lemma, for any formula $B(x)$ with $x$ as the sole free variable, there is a formula $G$ such that $\models_{\mathcal{Q}} G \Leftrightarrow B\left(\left\lceil G \right\rceil\right)$. Note that $B_1(\lceil B_2(x)\rceil)$ is a formula with $x$ as the sole free variable. Hence, there is a formula $G$ such that $\models_{\mathcal{Q}} G \Leftrightarrow B_1(\lceil B_2(\lceil G\rceil)\rceil)$. Define $G_1 = G$ and $G_2 = B_2(\lceil G\rceil)$. Then

$$\models_{\mathcal{Q}} G_1 \Leftrightarrow B_1\left(\left\l... ..._2\left(\left\lceil G\right\rceil\right) \right\rceil\right)$$

and

$$\models_{\mathcal{Q}} G_2 \Leftrightarrow B_2\left(\left\l... ...) \Leftrightarrow B_2\left(\left\lceil G \right\rceil\right)$$

3.

Let $Prov$ be a provability predicate for the theory $\mathcal{Q}$ and $X$ and $Y$ be formulas in the language of $\mathcal{Q}$. Assume $\models_{\mathcal{Q}} Prov\left(\left\lceil X \right\rceil\right) \supset Y$ and $\models_{\mathcal{Q}} Prov\left(\left\lceil Y \right\rceil\right) \supset X$. We show that both $X$ and $Y$ are theorems in $\mathcal{Q}$. Recall the properties of a provability predicate:

(P1) for all $X$, if $\models_{\mathcal{Q}} X$, then $\models_{\mathcal{Q}} Prov(\lceil X\rceil)$

(P2) for all $X$ and $Y$, $\models_{\mathcal{Q}} Prov(\lceil X \supset Y\rceil) \supset (Prov(\lceil X\rceil) \supset Prov(\lceil Y\rceil))$

(P3) for all $X$, $\models_{\mathcal{Q}} Prov(\lceil X\rceil) \supset Prov(\lceil Prov(\lceil X\rceil)\rceil)$

(NOTE: (P1) is not equivalent to ``for all $X$, $\models_{\mathcal{Q}} X \supset Prov(\lceil X\rceil)$''.) Recall that $\mathcal{Q}$ is a theory that can represent the computable functions. Hence, by Löb's Theorem, we have:

(L) for all $X$, if $\models_{\mathcal{Q}} Prov(\lceil X\rceil) \supset X$, then $\models_{\mathcal{Q}} X$

Finally, recall that $\mathcal{Q}$ is a consistent theory; hence, the following modus ponens style theorems are true:

(MP1) for all $X$ and $Y$, if $\models_{\mathcal{Q}} X \supset Y$ and $\models_{\mathcal{Q}} X$, then $\models_{\mathcal{Q}} Y$

(MP2) for all $X$ and $Y$ and $Z$, if $\models_{\mathcal{Q}} X \supset Y$ and $\models_{\mathcal{Q}} Y \supset Z$, then $\models_{\mathcal{Q}} X \supset Z$

We reason as follows:

(A1) $\models_{\mathcal{Q}} Prov(\lceil X\rceil) \supset Y$, by assumption.

(A2) $\models_{\mathcal{Q}} Prov(\lceil Y\rceil) \supset X$, by assumption.

(B1) $\models_{\mathcal{Q}} Prov(\lceil Prov(\lceil X\rceil) \supset Y\rceil)$, by (A1) and (P1).

(B2) $\models_{\mathcal{Q}} Prov(\lceil Prov(\lceil Y\rceil) \supset X\rceil)$, by (A2) and (P1).

(C1) $\models_{\mathcal{Q}} Prov(\lceil Prov(\lceil X\rceil)\rceil) \supset Prov(\lceil Y\rceil)$, by (P2), (B1), and (MP1).

(C2) $\models_{\mathcal{Q}} Prov(\lceil Prov(\lceil Y\rceil)\rceil) \supset Prov(\lceil X\rceil)$, by (P2), (B2), and (MP1).

(D1) $\models_{\mathcal{Q}} Prov(\lceil Prov(\lceil X\rceil)\rceil) \supset X$, by (C1), (A2), and (MP2).

(D2) $\models_{\mathcal{Q}} Prov(\lceil Prov(\lceil Y\rceil)\rceil) \supset Y$, by (C2), (A1), and (MP2).

(E1) $\models_{\mathcal{Q}} Prov(\lceil X\rceil) \supset X$, by (P3), (D1), and (MP2).

(E2) $\models_{\mathcal{Q}} Prov(\lceil Y\rceil) \supset Y$, by (P3), (D1), and (MP2).

(F1) $\models_{\mathcal{Q}} X$, by (E1) and (L).

(F2) $\models_{\mathcal{Q}} Y$, by (E2) and (L).

Thus, both $X$ and $Y$ are theorems in $\mathcal{Q}$.

4.

A pair of natural numbers $\langle a,b\rangle$ is called a stamps pair if for all $n \geq a + b$ there are natural numbers $i$ and $j$ such that $n = i * a + j * b$.

(a)

We prove in $\lambda$-PRL that $\langle3,5\rangle$ is a stamps pair.

__{{}}\

 
$\vdash$$\forall$n:int. 8 $\leq$n $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


| 		 by induction 1 8 10 3 


|


| 1. n:int 


| 2. n $<$8 


| 3. 8 $\leq$n+1 $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n+1 $=$i * 3 + j * 5) 


| $\vdash$8 $\leq$n $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


| | 		 by impR 


| $\ldots$


| 4. 8 $\leq$n 


| $\vdash$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


| 		 by arith $\surd$ 


|


| $\vdash$8 $\leq$8 $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(8 $=$i * 3 + j * 5) 


| | 		 by impR 


| 1. 8 $\leq$8 


| $\vdash$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(8 $=$i * 3 + j * 5) 


| | 		 by exR 1 1 


| $\ldots$


| $\vdash$(0 $\leq$1) $\land$(0 $\leq$1) $\land$(8 $=$1 * 3 + 1 * 5) 


| 		 by arith $\surd$ 


|


| $\vdash$8 $\leq$9 $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(9 $=$i * 3 + j * 5) 


| | 		 by impR 


| 1. 8 $\leq$9 


| $\vdash$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(9 $=$i * 3 + j * 5) 


| | 		 by exR 3 0 


| $\ldots$


| $\vdash$(0 $\leq$3) $\land$(0 $\leq$0) $\land$(9 $=$3 * 3 + 0 * 5) 


| 		 by arith $\surd$ 


|


| $\vdash$8 $\leq$10 $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(10 $=$i * 3 + j * 5) 


| | 		 by impR 


| 1. 8 $\leq$10 


| $\vdash$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(10 $=$i * 3 + j * 5) 


| | 		 by exR 0 2 


| $\ldots$


| $\vdash$(0 $\leq$0) $\land$(0 $\leq$2) $\land$(10 $=$0 * 3 + 2 * 5) 


| 		 by arith $\surd$ 


 


1. n:int 


2. 10 $<$n 


3. 8 $\leq$n-3 $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n-3 $=$i * 3 + j * 5) 


  $\vdash$8 $\leq$n $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


  | 		 by impL 3 


  |


  | $\ldots$


  | $\vdash$8 $\leq$n-3 


  | 		 by arith $\surd$ 


  | 


   


    $\ldots$


3. 8 $\leq$n-3 


4. $\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n-3 $=$i * 3 + j * 5) 


    $\vdash$8 $\leq$n $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


    | 		 by exR 4 





























































    | 


    $\ldots$


4. i:int 


5. j:int 


6. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n-3 $=$i * 3 + j * 5) 


    $\vdash$8 $\leq$n $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


    | 		 by andL 6 


    $\ldots$


6. 0 $\leq$i 


7. 0 $\leq$j 


8. n-3 $=$i * 3 + j * 5 


    $\vdash$8 $\leq$n $\Rightarrow$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


    | 		 by impR 


    $\ldots$


9. 8 $\leq$n 


    $\vdash$$\exists$i,j:int. (0 $\leq$i) $\land$(0 $\leq$j) $\land$(n $=$i * 3 + j * 5) 


    | 		 by exR i+1,j 


    $\ldots$


    $\vdash$(0 $\leq$i+1) $\land$(0 $\leq$j) $\land$(n $=$(i+1) * 3 + j * 5) 


by arith $\surd$

(b)

We describe the algorithm implicitly contained in the proof of $(a)$ in $\lambda$-PRL notation.

__{{}}\

stampsi(n:int):int $\equiv$n => 0 


8 => 1 


9 => 3 


10 => 0 


n => stampsi(n-3) + 1




stampsj(n:int):int $\equiv$n => 0 


8 => 1 


9 => 0 


10 => 2 


n => stampsj(n-3)
      

(c)

If $\langle a,b\rangle$ is a stamps pair (such that $a \leq b$), then

• $a=1$, or
• $a=2$ and $b = 1~\mathsf{mod}~2$, or
• $a=3$ and $b=4$, or
• $a=3$ and $b=5$

5.

We prove in $\lambda$-PRL that every non-empty list of integers has a maximal element.

__{{}}\

$\forall$l:list. ($\sim$(l=[]) $\Rightarrow$$\exists$i:int. (i$\in$l $\land$$\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i))) 
  

We give a $\lambda$-PRL definition of the predicate __{{}}\ i$\in$l:

__{{}}\

i$\in$l $\equiv$$\exists$k:int. (index(k,l)=i $\land$0$\leq$k $\land$k$<$length(l))
  

We prove the above statement $\lambda$-PRL's refinement logic:

__{{}}\

 
$\vdash$$\forall$l:list. ($\sim$(l=[]) $\Rightarrow$$\exists$i:int. (i$\in$l $\land$$\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i))) 


| 		 by induction x::l 


|


| $\vdash$$\sim$([]=[]) $\Rightarrow$$\exists$i:int. (i$\in$[] $\land$$\forall$j:int. (j$\in$[] $\Rightarrow$j$\leq$i)) 


| | 		 by impR 


| 1. $\sim$([]=[]) 


| $\vdash$$\exists$i:int. (i$\in$[] $\land$$\forall$j:int. (j$\in$[] $\Rightarrow$j$\leq$i)) 


| | 		 by notL 1 


| $\ldots$


| $\vdash$[]=[] 


| 		 by equality $\surd$ 


|


| 1. x:int 


| $\vdash$$\sim$([x]=[]) $\Rightarrow$$\exists$i:int. (i$\in$[x] $\land$$\forall$j:int. (j$\in$[x] $\Rightarrow$j$\leq$i)) 


| | 		 by impR 


| $\ldots$


| 2. $\sim$([x]=[]) 


| $\vdash$$\exists$i:int. (i$\in$[x] $\land$$\forall$j:int. (j$\in$[x] $\Rightarrow$j$\leq$i)) 


| | 		 by exR x 


| $\ldots$


| $\vdash$x$\in$[x] $\land$$\forall$j:int. (j$\in$[x] $\Rightarrow$j$\leq$x) 


| | 		 by andR 


| |


| | $\ldots$


| | $\vdash$x$\in$[x] 


| | | 		 by unfold $\in$ in 0 


| | $\ldots$


| | $\vdash$$\exists$k:int. (index(k,[x])=i $\land$0$\leq$k $\land$k$<$length([x])) 


| | | 		 by exR 0 


| | $\ldots$


| | $\vdash$index(0,[x])=x $\land$0$\leq$0 $\land$0$<$length([x]) 


| | | 		 by simplify in 0 


| | $\ldots$


| | $\vdash$x=x $\land$0$\leq$0 $\land$0$<$1
| | 		 by arith $\surd$ 


|  


|   $\ldots$


|   $\vdash$$\forall$j:int. (j$\in$[x] $\Rightarrow$j$\leq$x) 


|   | 		 by allR 


|   $\ldots$


|   3. j:int 


|   $\vdash$j$\in$[x] $\Rightarrow$j$\leq$x 


|   | 		 by impR 


|   | 


|   $\ldots$


|   4. j$\in$[x] 


|   $\vdash$j$\leq$x 


|   | 		 by unfold $\in$ in 4 


|   $\ldots$


|   4. $\exists$k:int. (index(k,[x])=j $\land$0$\leq$k $\land$k$<$length([x])) 


|   $\vdash$j$\leq$x 


|   | 		 by exL 4 





























































|   | 


|   $\ldots$


|   4. k:int 


|   5. index(k,[x])=j $\land$0$\leq$k $\land$k$<$length([x]) 


|   $\vdash$j$\leq$x 


|   | 		 by simplify in 5 


|   $\ldots$


|   5. index(k,[x])=j $\land$0$\leq$k $\land$k$<$1 


|   $\vdash$j$\leq$x 


|   | 		 by andL 5 


|   $\ldots$


|   5. index(k,[x])=j 


|   6. 0$\leq$k 


|   7. k$<$1 


|   $\vdash$j$\leq$x 


|   | 		 by cut k=0 


|   | 


|   | $\ldots$


|   | $\vdash$k=0 


|   | 		 by arith $\surd$ 


|     


|     $\ldots$


|     8. k=0 


|     $\vdash$j$\leq$x 


|     | 		 by cut index(k,[x])=j 


|     | 


|     | $\ldots$


|     | $\vdash$index(k,[x])=j 


|     | 		 by hyp 5 $\surd$ 


|       


|       $\ldots$


|       9. index(k,[x])=j 


|       $\vdash$j$\leq$x 


|       | 		 by subst 8 9 


|       $\ldots$


|       9. index(0,[x])=j 


|       $\vdash$j$\leq$x 


|       | 		 by simplify 9 


|       $\ldots$


|       9. x=j 


|       $\vdash$j$\leq$x 


| 		 by arith $\surd$ 


 


1. x:int 


2. l:list 


3. $\sim$(l=[]) $\Rightarrow$$\exists$i:int. (i$\in$l $\land$$\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i)) 


  $\vdash$$\sim$(x::l=[]) $\Rightarrow$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


  | 		 by cut (l=[]) $\lor$$\sim$(l=[]) 


  |


  | $\ldots$


  | $\vdash$(l=[]) $\lor$$\sim$(l=[]) 


  | 		 by equality $\surd$ 


   


    $\ldots$


4. (l=[]) $\lor$$\sim$(l=[]) 


    $\vdash$$\sim$(x::l=[]) $\Rightarrow$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


    | 		 by orL 4 


    |


    | $\ldots$


    | 4. l=[] 


    | $\vdash$$\sim$(x::l=[]) $\Rightarrow$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


    | | 		 by subst 4 0 


    | $\ldots$


    | $\vdash$$\exists$i:int. (i$\in$x::[] $\land$$\forall$j:int. (j$\in$x::[] $\Rightarrow$j$\leq$i)) 


    | | 		 by simplify 0 





























































    | | 


    | $\ldots$


    | $\vdash$$\exists$i:int. (i$\in$[x] $\land$$\forall$j:int. (j$\in$[x] $\Rightarrow$j$\leq$i)) 


    | 		 by proof of previous case $\surd$ 


    | 


     


      $\ldots$


4. $\sim$(l=[]) 


      $\vdash$$\sim$(x::l=[]) $\Rightarrow$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


      | 		 by impR 


      $\ldots$


5. $\sim$(x::l=[]) 


      $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


      | 		 by impL 3 


      |


      | $\ldots$


      | $\vdash$$\sim$(l=[]) 


      | 		 by hyp 4 $\surd$ 


       


        $\ldots$


3. $\sim$(l=[]) 


4. $\sim$(x::l=[]) 


5. $\sim$(l=[]) 


6. $\exists$i:int. (i$\in$l $\land$$\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i)) 


        $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


        | 		 by exL 6 


        $\ldots$


6. i:int 


7. i$\in$l $\land$$\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i) 


        $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


        | 		 by andL 7 


        $\ldots$


7. i$\in$l 


8. $\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i) 


        $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


        | 		 by unfold $\in$ 7 


        $\ldots$


7. $\exists$k:int. (index(k,l)=i $\land$0$\leq$k $\land$k$<$length(x::l)) 


8. $\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i) 


        $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


        | 		 by exL 7 


        $\ldots$


7. k:int 


8. index(k,l)=i $\land$0$\leq$k $\land$k$<$length(x::l) 


9. $\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i) 


        $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


        | 		 by andL 8 


        $\ldots$


8. index(k,l)=i 


9. 0$\leq$k 


10. k$<$length(x::l) 


11. $\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i) 


        $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


        | 		 by simplify 10 


        $\ldots$


8. index(k,l)=i 


9. 0$\leq$k 


10. k$<$length(l)+1 


11. $\forall$j:int. (j$\in$l $\Rightarrow$j$\leq$i) 


        $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


        | 		 by cut (x $\leq$i) $\lor$(x $>$i) 


        |


        | $\ldots$


        | $\vdash$(x $\leq$i) $\lor$(x $>$i) 


        | 		 by arith $\surd$ 





























































        | 


         


          $\ldots$


12. (x $\leq$i) $\lor$(x $>$i) 


          $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


          | 		 by orL 12 


          |


          | $\ldots$


          | 12. x $\leq$i 


          | $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


          | | 		 by exR i 


          | $\ldots$


          | $\vdash$i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i) 


          | | 		 by andR 


          | |


          | | $\ldots$


          | | $\vdash$i$\in$x::l 


          | | | 		 by unfold $\in$ in 0 


          | | $\ldots$


          | | $\vdash$$\exists$k:int. (index(k,x::l)=i $\land$0$\leq$k $\land$k$<$length(x::l)) 


          | | | 		 by exR k+1 


          | | $\ldots$


          | | $\vdash$index(k+1,x::l)=i $\land$0$\leq$k+1 $\land$k+1$<$length(x::l) 


          | | | 		 by def index(k+1,x::l) up 


          | | | 


          | | | $\ldots$


          | | | $\vdash$0 $<$k+1 


          | | | 		 by arith $\surd$ 


          | |   


          | |   $\ldots$


          | |   13. 0 $<$k+1 


          | |   14. index(k+1,x::l) = index(k+1-1,tl(x::l)) 


          | |   $\vdash$index(k+1,x::l)=i $\land$0$\leq$k+1 $\land$k+1$<$length(x::l) 


          | |   | 		 by subst 14 0 


          | |   $\ldots$


          | |   $\vdash$index(k+1-1,tl(x::l))=i $\land$0$\leq$k+1 $\land$k+1$<$length(x::l) 


          | |   | 		 by simplify 0 


          | |   $\ldots$


          | |   $\vdash$index(k,l)=i $\land$0$\leq$k+1 $\land$k+1$<$length(l)+1 


          | | 		 by arith $\surd$ 


          |  


          |   $\ldots$


          |   $\vdash$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i) 


          |   | 		 by allR 


          |   $\ldots$


          |   13. j: int 


          |   $\vdash$j$\in$x::l $\Rightarrow$j$\leq$i 


          |   | 		 by impR 


          |   $\ldots$


          |   14. j$\in$x::l 


          |   $\vdash$j$\leq$i 


          |   | 		 by unfold $\in$ in 14 


          |   $\ldots$


          |   14. $\exists$k:int. (index(k,x::l)=j $\land$0$\leq$k $\land$k$<$length(x::l)) 


          |   $\vdash$j$\leq$i 


          |   | 		 exL 14 


          |   $\ldots$


          |   14. k':int 


          |   15. index(k',x::l)=j $\land$0$\leq$k' $\land$k'$<$length(x::l)) 


          |   $\vdash$j$\leq$i 


          |   | 		 andL 15 





























































          |   | 


          |   $\ldots$


          |   15. index(k',x::l)=j 


          |   16. 0$\leq$k' 


          |   17. k'$<$length(x::l)) 


          |   $\vdash$j$\leq$i 


          |   | 		 by simplify 17 


          |   $\ldots$


          |   17. k'$<$length(l)+1 


          |   $\vdash$j$\leq$i 


          |   | 		 cut k'=0 $\lor$k'$>$0 


          |   | 


          |   | $\ldots$


          |   | $\vdash$k'=0 $\lor$k'$>$0 


          |   | 		 by arith $\surd$ 


          |     


          |     $\ldots$


          |     18. k'=0 $\lor$k'$>$0 


          |     $\vdash$j$\leq$i 


          |     | 		 by orL 18 


          |     | 


          |     | $\ldots$


          |     | 18. k'=0 


          |     | $\vdash$j$\leq$i 


          |     | | 		 by cut index(k',x::l)=j 


          |     | |  


          |     | | $\ldots$


          |     | | $\vdash$index(k',x::l)=j 


          |     | | 		 by hyp 15 


          |     |   


          |     |   $\ldots$


          |     |   19. index(k',x::l)=j 


          |     |   $\vdash$j$\leq$i 


          |     |   | 		 by subst 18 19 


          |     |   $\ldots$


          |     |   19. index(0,x::l)=j 


          |     |   $\vdash$j$\leq$i 


          |     |   | 		 by simplify 19 


          |     |   $\ldots$


          |     |   19. x=j 


          |     |   $\vdash$j$\leq$i 


          |     | 		 by arith $\surd$ 


          |       


          |       $\ldots$


          |       18. k'$>$0 


          |       $\vdash$j$\leq$i 


          |       | 		 by allL 11 j 


          |       $\ldots$


          |       19. j$\in$l $\Rightarrow$j$\leq$i 


          |       $\vdash$j$\leq$i 


          |       | 		 by impL 19 


          |       | 


          |       | $\ldots$


          |       | $\vdash$j$\in$l 


          |       | | 		 by unfold $\in$ in 0 


          |       | $\ldots$


          |       | $\vdash$$\exists$k:int. (index(k,l)=j $\land$0$\leq$k $\land$k$<$length(l)) 


          |       | | 		 by exR k'-1 


          |       | $\ldots$


          |       | $\vdash$index(k'-1,l)=j $\land$0$\leq$k'-1 $\land$k'-1$<$length(l) 


          |       | | 		 by def index(k',x::l) up 


          |       | | 


          |       | | $\ldots$


          |       | | $\vdash$0$\leq$k' 


          |       | | 		 by hyp 18 





























































          |       | | 


          |       |   


          |       |   $\ldots$


          |       |   20. 0$\leq$k' 


          |       |   21. index(k',x::l) = index(k'-1,tl(x::l)) 


          |       |   $\vdash$index(k'-1,l)=j $\land$0$\leq$k'-1 $\land$k'-1$<$length(l) 


          |       |   | 		 by simplify 21 


          |       |   $\ldots$


          |       |   21. index(k',x::l) = index(k'-1,l) 


          |       |   $\vdash$index(k'-1,l)=j $\land$0$\leq$k'-1 $\land$k'-1$<$length(l) 


          |       | 		 by arith $\surd$ 


          |         


          |         19. j$\in$l 


          |         20. j$\leq$i 


          |         $\vdash$j$\leq$i 


          | 		 by hyp 20 $\surd$ 


           


            $\ldots$


12. x$>$i 


            $\vdash$$\exists$i:int. (i$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$i)) 


            | 		 by exR x 


            $\ldots$


            $\vdash$x$\in$x::l $\land$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$x) 


            | 		 by andR 


            |


            | $\ldots$


            | $\vdash$x$\in$x::l 


            | | 		 by unfold $\in$ in 0 


            | $\ldots$


            | $\vdash$$\exists$k:int. (index(k,x::l)=x $\land$0$\leq$k $\land$k$<$length(x::l)) 


            | | 		 by exR 0 


            | $\ldots$


            | $\vdash$index(0,x::l)=x $\land$0$\leq$0 $\land$0$<$length(x::l) 


            | | 		 by simplify 0 


            | $\ldots$


            | $\vdash$x=x $\land$0$\leq$0 $\land$0$<$length(l)+1 


            | 		 by arith $\surd$ 


             


              $\ldots$


              $\vdash$$\forall$j:int. (j$\in$x::l $\Rightarrow$j$\leq$x) 


              | 		 by allR 


              $\ldots$


13. j:int 


              $\vdash$j$\in$x::l $\Rightarrow$j$\leq$x 


              | 		 by impR 


              $\ldots$


14. j$\in$x::l 


              $\vdash$j$\leq$x 


              | 		 by unfold $\in$ in 14 


              $\ldots$


14. $\exists$k:int. (index(k,x::l)=j $\land$0$\leq$k $\land$k$<$length(x::l)) 


              $\vdash$j$\leq$x 


              | 		 by exL 14 


              $\ldots$


14. k':int 


15. index(k',x::l)=j $\land$0$\leq$k' $\land$k'$<$length(x::l) 


              $\vdash$j$\leq$x 


              | 		 by andL 15 


              $\ldots$


15. index(k',x::l)=j 


16. 0$\leq$k' 


17. k'$<$length(x::l) 


              $\vdash$j$\leq$x 


              | 		 by simplify 17 





























































              | 


              $\ldots$


17. k'$<$length(l)+1 


              $\vdash$j$\leq$x 


              | 		 by cut k'=0 $\lor$k'$>$0 


              | 


              | $\ldots$


              | $\vdash$k'=0 $\lor$k'$>$0 


              | 		 by arith $\surd$ 


                


                $\ldots$


18. k'=0 $\lor$k'$>$0 


                $\vdash$j$\leq$x 


                | 		 by orL 18 


                | 


                | $\ldots$


                | 18. k'=0 


                | $\vdash$j$\leq$x 


                | | 		 by cut index(k',x::l)=j 


                | | 


                | | $\ldots$


                | | $\vdash$index(k',x::l)=j 


                | | 		 by hyp 15 


                |   


                |   $\ldots$


                |   19. index(k',x::l)=j 


                |   $\vdash$j$\leq$x 


                |   | 		 by subst 18 19 


                |   $\ldots$


                |   19. index(0,x::l)=j 


                |   $\vdash$j$\leq$x 


                |   | 		 by simplify 19 


                |   $\ldots$


                |   19. x=j 


                |   $\vdash$j$\leq$x 


                | 		 by arith $\surd$ 


                  


                  $\ldots$


18. k'$>$0 


                  $\vdash$j$\leq$x 


                  | 		 by allL 11 j 


                  $\ldots$


19. j$\in$l $\Rightarrow$j$\leq$i 


                  $\vdash$j$\leq$x 


                  | 		 by impL 19 


                  | 


                  | $\ldots$


                  | $\vdash$j$\in$l 


                  | | 		 by unfold $\in$ in 0 


                  | $\ldots$


                  | $\vdash$$\exists$k:int. (index(k,l)=j $\land$0$\leq$k $\land$k$<$length(l)) 


                  | | 		 exR k'-1 


                  | $\ldots$


                  | $\vdash$index(k'-1,l)=j $\land$0$\leq$k'-1 $\land$k'-1$<$length(l)) 


                  | | 		 by def index(k',x::l) up 


                  | | 


                  | | $\ldots$


                  | | $\vdash$0$\leq$k' 


                  | | 		 by hyp 18 


                  |   


                  |   $\ldots$


                  |   20. 0$\leq$k' 


                  |   21. index(k',x::l) = index(k'-1,tl(x::l)) 


                  |   $\vdash$index(k'-1,l)=j $\land$0$\leq$k'-1 $\land$k'-1$<$length(l)) 


                  |   | 		 by simplify 21 





























































                  |   | 


                  |   $\ldots$


                  |   20. 0$\leq$k' 


                  |   21. index(k',x::l) = index(k'-1,l) 


                  |   $\vdash$index(k'-1,l)=j $\land$0$\leq$k'-1 $\land$k'-1$<$length(l)) 


                  | 		 by arith $\surd$ 


                    


                    $\ldots$


19. j$\in$l 


20. j$\leq$i 


                    $\vdash$j$\leq$x 


by arith $\surd$

We describe the extracted algorithm in $\lambda$-PRL notation.

__{{}}\

listmax(l:list):int $\equiv$0 => 0 


1 => hd(l) 


l => if tl(l) $=$[] 


then hd(l) 


else if hd(l) $\leq$listmax(tl(l)) 


then listmax(tl(l)) 


else hd(l)