1. x:

2.y: [not for witness]

3.x+1<y

{z:|x<z&z<y}

The sequent above claims that there is some "witness" expression *not* containing *y*

1. x:

2.y:

3.x+1<y

??? {z:|x<z&z<y}

in which case the witness *y*-1 {*z*:| *x*<*z* & *z*<*y* }*x*+1"*y*

Now, why do we care about restricting the use of declared variables from witnesses?
*k**i*:| 0 *i* < *k* }*k*

Thm* k:x:(kList){y:(k+1)|ygreater-boundsx}Thm* k:.x:(kList){y:(k+1)|ygreater-boundsx}where

Def ,ygreater-boundsx==i:||x||.x[i]<y

and|| denotes the length of a list,x||

anddenotes the member at position x[i]of list i||x||, x

the head of a list being considered position0 .

The first is the type of functions which, applied to *k* *k**k**k*

The second, an *k* List)*k* *k*

The proofs given for the above two theorems begin similarly, producing the following subgoals respectively:

1. k:

2.x:kList

{y:(k+1)|ygreater-boundsx}

1. k: [not for witness]

2.x:kList

{y:(k+1)|ygreater-boundsx}

the difference being simply that the upper sequent can be satisfied by witness *k*"*k*"*x* : A List B(*x*)*u* : A 2. *v* : A List 3. B(*v*) B((*u*.*v*))

Case of x; nil p ;u.v, rec:rq(u;v;r)

from witnesses *u*; *v*; *r*)"

Representing

About: