Step
*
1
1
1
2
of Lemma
maxsegsum_sqexists
1. L :  List
 max_initseg_sum(0;[])
BY
{ (Unfold `max_initseg_sum` 0 THEN Auto) }
Latex:
1.  L  :  \mBbbZ{}  List
\mvdash{}  max\_initseg\_sum(0;[])
By
(Unfold  `max\_initseg\_sum`  0  THEN  Auto)
Home
Index