---

Step * 2 1 1 2 1 1 of Lemma maxsegsum_singleton


1. x : @i
2. r : ||[x]||@i
 x  initseg_sum(r;[x]) 
BY
{ ((Reduce 2 THEN Assert r = 0 THEN Auto) THEN (HypSubst (-1) 0 THENA Auto)) }

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

---

Latex:



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


By

((Reduce  2  THEN  Assert  \mkleeneopen{}r  =  0\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  (HypSubst  (-1)  0  THENA  Auto))

---

Home Index