2. k :
3. 0<k
4.
b:, e:({a..b
}
).
4. b-a = k-1
((
i:{a..b}. e(i)) = 0 
(Or i:{a..b}. e(i) = 0))
5. b :
6. e : {a..b
}
7. b-a = k
( i:{a..b}. e(i)) = 0 (Or i:{a..b}. e(i) = 0)
b:, e:({a..b}).
(( i:{a..b}. e(i)) = 0 (Or i:{a..b}. e(i) = 0))
}
( i:{a..b}. e(i)) = 0 (Or i:{a..b}. e(i) = 0)| By: |
Thm* f:(AAA), 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))
THEN Reduce Concl |
| 1 |
( i:{a..b-1}. e(i)) e(b-1) = 0 (Or i:{a..b-1}. e(i) = 0)  e(b-1) = 0 | 2 steps |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |
 |