Nuprl - Proof: least characterized2 1 1 2 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. p :

2. i :

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

. p(i))

{i:

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

j:

i.

p(j)) }

{i:

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

j:

i.

p(j)) }

{i:

| p(i) & (

j:

. j<i

p(j)) }

By:

Analyze

Generated subgoal:

1 5. x : {i:(i+1)| p(i) & (j:i. p(j)) }
x {i:| p(i) & (j:. j<i p(j)) }
3 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