Nuprl - Proof: least exists 1 1

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

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

1. k :

2. P :

k

Prop
3.

i:

k. P(i) [not for witness]
4. p :

k

5.

i:

k. p(i)

P(i)

{i:

k| P(i) & (

j:

i.

P(j)) }

By:	Inst: Thm* k:, p:{p:(k)\| i:k. p(i) }. Thm* (least i:. p(i)) {i:k\| p(i) & (j:i. p(j)) } Using:[k \| p]

Generated subgoals:

1 3. i:k. P(i)
4. p : k
5. i:k. p(i)  P(i)
  p  {p:(k)| i:k. p(i) }
2 steps

2 6. (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }
  {i:k| P(i) & (j:i. P(j)) }
4 steps

About:

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

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