Step
*
1
of Lemma
maxsegsum_singleton
1.
x
:
@i
max_seg_sum(x;[x])
BY
{
Unfold
`max_seg_sum`
0
}
1
1.
x
:
@i
(([x]
=
[])
(x
=
0))
((
h:
.
t:
List.
([x]
=
[h
/
t]))
(
p:
||[x]||.
q:{p..||[x]||
}.
(x
seg_sum(p;q;[x])
))
(
a:
||[x]||.
b:{a..||[x]||
}.
(x
=
seg_sum(a;b;[x]))))
Latex:
1. x : \mBbbZ{}@i
\mvdash{} max\_seg\_sum(x;[x])
By
Unfold `max\_seg\_sum` 0
Home
Index
@i
max_seg_sum(x;[x])@i (([x] = []) 
(x = 0))
((
h:. t: List. ([x] = [h / t])) (
p:
||[x]||. q:{p..||[x]||
}. (x 
seg_sum(p;q;[x]) )) (a:||[x]||. b:{a..||[x]||}. (x = seg_sum(a;b;[x]))))