a,b:
, e:({a..b
}
).
a<b 
(c:. b = c+1 (
i:{a..b}. e(i)) = ( i:{a..c}. e(i))
e(c)) a,b:, e:({a..b}).
a<b (c:. b = c+1 ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c))| By: |
Thm* f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* a<b Thm*
Thm* ( c:.
Thm* (b = c+1 Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..c}. e(i)),e(c)))
Using:[A:= | f:=  x,y. xy | 1]
THEN Reduce Hyp:-1 |
None
About:
 |  |  |  |  |  |  |
 |  |  |  |  |