Rank | Theorem | Name |
2 | Thm* f:(A A A), u:A, a,b: , e:({a..b } A), k: .
Thm* (Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) j:{a+k..b+k }. e(j-k)) | [iter_via_intseg_shift_rw] |
cites the following: |
1 | 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)) | [all_int_segs_by_upper_ind] |
0 | Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* b a  (Iter(f;u) i:{a..b }. e(i)) = u | [iter_via_intseg_null] |
1 | Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* a<b
Thm* 
Thm* (Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..b-1 }. e(i)),e(b-1)) | [iter_via_intseg_split_last] |