(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 2

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
9. a<b
  P(a,b)


By: BackThru: Hyp:3


Generated subgoals:

None

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