Nuprl - Proof: least is least2 1 1

(5steps 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 least2 1 1

1. p : {p:(

)|

i:

. p(i) }
2. (least i:

. p(i))

{i:

| p(i) & (

j:

. j<i

p(j)) }

j:

(least i:

. p(i)).

p(j)

By:

Analyze-1

Generated subgoal:

1 2. (least i:. p(i))
3. p(least i:. p(i)) & (j:. j<(least i:. p(i))  p(j))  [not for witness]
  j:(least i:. p(i)). p(j)
2 steps

About:

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

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