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