---

Step * 1 1 of Lemma max_initseg_sum_wf


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))))  
BY
{ Auto }

---

Latex:



1.  [i]  :  \mBbbZ{}
2.  [L]  :  \mBbbZ{}  List
\mvdash{}  ((L  =  [])  \mwedge{}  (i  =  0))
    \mvee{}  ((\mexists{}h:\mBbbZ{}.  \mexists{}t:\mBbbZ{}  List.  (L  =  [h  /  t]))
        \mwedge{}  (\mforall{}r:\mBbbN{}||L||.  (i  \mgeq{}  initseg\_sum(r;L)  ))
        \mwedge{}  (\mexists{}c:\mBbbN{}||L||.  (i  =  initseg\_sum(c;L))))  \mmember{}  \mBbbP{}


By

Auto

---

Home Index