Nuprl - Proof: all intseg vs iter and 1 2

(12steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all intseg vs iter and 1 2

1. a :

2.

b:

, P:({a..b

}

Prop). b

a

((

i:{a..b

}. P(i))

(And i:{a..b

}. P(i)))

k:

, b:

.

b-a = k

(

P:({a..b

}

Prop). (

i:{a..b

}. P(i))

(And i:{a..b

}. P(i)))

By:	NatInd Concl THEN UnivCD

Generated subgoals:

1 3. b :
4. b-a = 0
5. P : {a..b}Prop
  (i:{a..b}. P(i))  (And i:{a..b}. P(i))
1 step

2 3. k :
4. 0<k
5. b:.
5. b-a = k-1
5.
5. (P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i)))
6. b :
7. b-a = k
8. P : {a..b}Prop
  (i:{a..b}. P(i))  (And i:{a..b}. P(i))
2 steps

About:

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

(12steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc