Nuprl - Proof: partial sort exists 2 1 1 1

(8steps 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: partial sort exists 2 1 1 1

1. T : Type
2. T List
3. P : T

T

4.

x,y:T. P(x,y)

P(y,x)
5. L1 : T List
6. i :

(||L1||-1)
7. P(L1[i],L1[(i+1)])
8. i = i
9.

i+1 = i
10. i+1 = i+1

P(L1[(i+1)],L1[i])

By:

EasyHyp

Generated subgoals:

None

About:

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

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