---

Step * 2 1 1 1 of Lemma maxsegsum_singleton


1. x : @i
 h:. t: List. ([x] = [h / t])
BY
{ (InstConcl [x;[]] THEN Auto) }

---

Latex:



1.  x  :  \mBbbZ{}@i
\mvdash{}  \mexists{}h:\mBbbZ{}.  \mexists{}t:\mBbbZ{}  List.  ([x]  =  [h  /  t])


By

(InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index