---

Step * 2 1 1 2 1 1 1 of Lemma maxsegsum_singleton


1. x : @i
2. r : 1@i
3. r = 0
 x  initseg_sum(0;[x]) 
BY
{ (InstLemma `initseg_sum0` [x;[]] THENA Auto) }

1
1. x : @i
2. r : 1@i
3. r = 0
4. initseg_sum(0;[x]) = x
 x  initseg_sum(0;[x]) 

---

Latex:



1.  x  :  \mBbbZ{}@i
2.  r  :  \mBbbN{}1@i
3.  r  =  0
\mvdash{}  x  \mgeq{}  initseg\_sum(0;[x]) 


By

(InstLemma  `initseg\_sum0`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index