Nuprl - Proof: partial sort exists 2 1 2 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 2 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. P(L1[i],L1[(i+1)])
9. P(L1[(i+1)],L1[i])

count(x < y in L1 | P(x,y))+-1+1<count(x < y in L1 | P(x,y))

By:	AllHyps (h.FwdThru h [-1] THEN Complete Auto)

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