---

Step * 1 of Lemma max_initseg_sum_wf


1. [i] : 
2. [L] :  List
 max_initseg_sum(i;L)  
BY
{ Unfold `max_initseg_sum` 0 }

1
1. [i] : 
2. [L] :  List
 ((L = [])  (i = 0))
   ((h:. t: List. (L = [h / t]))  (r:||L||. (i  initseg_sum(r;L) ))  (c:||L||. (i = initseg_sum(c;L))))  

---

Latex:



1.  [i]  :  \mBbbZ{}
2.  [L]  :  \mBbbZ{}  List
\mvdash{}  max\_initseg\_sum(i;L)  \mmember{}  \mBbbP{}


By

Unfold  `max\_initseg\_sum`  0

---

Home Index