Nuprl - Proof: least characterized2 1 1 2 1 1

(10steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: least characterized2 1 1 2 1 1

1. p :

2. i :

3. p(i)
4. (least i:

. p(i))

{i:

(i+1)| p(i) & (

j:

i.

p(j)) }
5. x : {i:

(i+1)| p(i) & (

j:

i.

p(j)) }

x

{i:

| p(i) & (

j:

. j<i

p(j)) }

By:

Analyze5

Generated subgoal:

1 5. x : (i+1)
6. p(x) & (j:x. p(j))
x {i:| p(i) & (j:. j<i p(j)) }
2 steps

About:

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

(10steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc