---

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


1. x : @i
2. p : 1@i
3. q : {p..1}@i
4. p = 0
5. q = 0
 x  seg_sum(0;0;[x]) 
BY
{ ((InstLemma `seg_sum0` [0;[x]] THENA Auto) THEN (HypSubst (-1) 0 THENA Auto)) }

1
1. x : @i
2. p : 1@i
3. q : {p..1}@i
4. p = 0
5. q = 0
6. seg_sum(0;0;[x]) = initseg_sum(0;[x])
 x  initseg_sum(0;[x]) 

---

Latex:



1.  x  :  \mBbbZ{}@i
2.  p  :  \mBbbN{}1@i
3.  q  :  \{p..1\msupminus{}\}@i
4.  p  =  0
5.  q  =  0
\mvdash{}  x  \mgeq{}  seg\_sum(0;0;[x]) 


By

((InstLemma  `seg\_sum0`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (HypSubst  (-1)  0  THENA  Auto))

---

Home Index