Nuprl - Proof: rel star finite 1 1 1 2 1 2 1 1 1 1 2 1 1

(41steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star finite 1 1 1 2 1 2 1 1 1 1 2 1 1

1. n :

2. R :

n

n

Prop
3. x :

n
4. y :

n
5. n@0 :

6.

j:

. j<n@0

(x R^j y)

(

k:

(n+1). x R^k y)
7. L :

n List
8. ||L|| = n@0+1
9. L[0] = x
10. last(L) = y
11.

i:

n@0. L[i] R L[(i+1)]
12.

n@0

n
13. i :

(n@0+1)
14. j :

(n@0+1)
15. i<j
16. L[i] = L[j]
17. ||firstn(i+1;L) @ nth_tl(j+1;L)|| = n@0-(j-i)+1

(firstn(i+1;L) @ nth_tl(j+1;L))[0] = x

By:	RWO Thm* as,bs:T List, i:\|\|as\|\|. (as @ bs)[i] = as[i] 0 THEN RWO Thm* as:T List, n:{0...\|\|as\|\|}, i:n. firstn(n;as)[i] = as[i] 0

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(41steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc