Nuprl - Proof: least wf 1

(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

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

1. k :

2. p : {p:(

k

)|

i:

k. p(i) }
3. (least i:

. p(i))

{i:

k| p(i) & (

j:

i.

p(j)) }

(least i:

. p(i))

k

By:	BackThru: {i:k\| p(i) & (j:i. p(j)) } k

Generated subgoals:

None

About:

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

(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc