---

Step * 1 1 1 2 1 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
6. seg_sum(0;0;[x]) = initseg_sum(0;[x])
 x  initseg_sum(0;[x]) 
BY
{ ((InstLemma `initseg_sum0` [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])
7. initseg_sum(0;[x]) = x
 x  x 

---

Latex:



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


By

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

---

Home Index