Step
*
of Lemma
maxsegsum_singleton
x:. (max_seg_sum(x;[x])  max_initseg_sum(x;[x]))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }
1
1. x : @i
 max_seg_sum(x;[x])
2
1. x : @i
 max_initseg_sum(x;[x])
Latex:
\mforall{}x:\mBbbZ{}.  (max\_seg\_sum(x;[x])  \mwedge{}  max\_initseg\_sum(x;[x]))
By
RepeatFor  2  ((D  0  THENA  Auto))
Home
Index