Nuprl - Proof: least is least 1

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

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

1. k :

2. p : {p:(

k

)|

i:

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

. p(i))

{i:

k| p(i) & (

j:

i.

p(j)) }

j:

(least i:

. p(i)).

p(j)

By:	(least i:. p(i)) By BackThru: {i:k\| p(i) & (j:i. p(j)) } { for type checking } THEN Analyze3 THEN Unhide THEN Analyze-2

Generated subgoal:

1 3. (least i:. p(i))  k
4. p(least i:. p(i))
5. j:(least i:. p(i)). p(j)
6. (least i:. p(i))
  j:(least i:. p(i)). p(j)
Auto

About:

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

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