(12steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int segs from base by upper ind 1 1 1 1

1. P : Prop
2. a : 
3. b:{...a}. P(a,b)
4. b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b)
5. k : 
6. k1:k1<k  (b:{a...}. b-ak1  P(a,b))
7. b : {a...}
8. b-ak
  P(a,b)


By: Decide: a<b


Generated subgoals:

1 9. a<b
  P(a,b)

2 steps
2 9. a<b
  P(a,b)

1 step

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

(12steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc