---

Step * 1 1 1 2 2 1 of Lemma maxsegsum_singleton


1. x : @i
 x = seg_sum(0;0;[x])
BY
{ ((InstLemma `seg_sum0` [0;[x]] THENA Auto) THEN (InstLemma `initseg_sum0` [x;[]] THENA Auto)) }

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

---

Latex:



1.  x  :  \mBbbZ{}@i
\mvdash{}  x  =  seg\_sum(0;0;[x])


By

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

---

Home Index