(7steps total) Remark PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iter via intseg shift rw 1
1. A : Type
2. f : AAA
3. u : A
  a,b:, e:({a..b}A), k:.
  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k))
By: BackThru: 
Thm*  P:(Prop). 
Thm*  (a:, b:{...a}. P(a,b))
Thm*  
Thm*  (a:, b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (a,b:. P(a,b))

Generated subgoals:

1 4. a : 
5. b : {...a}
6. e : {a..b}A
7. k : 
  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k))
1 step
2 4. a : 
5. b : {a+1...}
6. c:{a..b}, e:({a..c}A), k:.
6. (Iter(f;u) i:{a..c}. e(i)) = (Iter(f;u) j:{a+k..c+k}. e(j-k))
7. e : {a..b}A
8. k : 
  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k))
4 steps

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

(7steps total) Remark PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc