---

Step * of Lemma initseg_sum0

h:. t: List.  (initseg_sum(0;[h / t]) = h)
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. h : @i
2. t :  List@i
 initseg_sum(0;[h / t]) = h

---

Latex:


\mforall{}h:\mBbbZ{}.  \mforall{}t:\mBbbZ{}  List.    (initseg\_sum(0;[h  /  t])  =  h)


By

RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index