---

Step * 1 1 1 of Lemma simplex-face_wf


1. n : ℤ
2. 0 ≤ n
3. v : Δ(n)
4. i : ℕn + 2
5. ∀i:ℕn + 1. (r0 ≤ (v i))
6. Σ{v i | 0≤i≤n} = r1
7. ∀i@0:ℕ(n + 1) + 1. (r0 ≤ if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi )
8. i = (n + 1) ∈ ℤ
⊢ Σ{if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi  | 0≤i@0≤n + 1} = r1
BY
{ (RWO "rsum-split-last" 0 THENA Auto) }

1
1. n : ℤ
2. 0 ≤ n
3. v : Δ(n)
4. i : ℕn + 2
5. ∀i:ℕn + 1. (r0 ≤ (v i))
6. Σ{v i | 0≤i≤n} = r1
7. ∀i@0:ℕ(n + 1) + 1. (r0 ≤ if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi )
8. i = (n + 1) ∈ ℤ
⊢ (Σ{if i@0 <z i then v i@0
if i <z i@0 then v (i@0 - 1)
else r0
fi  | 0≤i@0≤(n + 1) - 1}
+ if n + 1 <z i then v (n + 1)
  if i <z n + 1 then v ((n + 1) - 1)
  else r0
  fi )
= r1

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  \mleq{}  n
3.  v  :  \mDelta{}(n)
4.  i  :  \mBbbN{}n  +  2
5.  \mforall{}i:\mBbbN{}n  +  1.  (r0  \mleq{}  (v  i))
6.  \mSigma{}\{v  i  |  0\mleq{}i\mleq{}n\}  =  r1
7.  \mforall{}i@0:\mBbbN{}(n  +  1)  +  1.  (r0  \mleq{}  if  i@0  <z  i  then  v  i@0  if  i  <z  i@0  then  v  (i@0  -  1)  else  r0  fi  )
8.  i  =  (n  +  1)
\mvdash{}  \mSigma{}\{if  i@0  <z  i  then  v  i@0  if  i  <z  i@0  then  v  (i@0  -  1)  else  r0  fi    |  0\mleq{}i@0\mleq{}n  +  1\}  =  r1


By

---

Latex:
(RWO  "rsum-split-last"  0  THENA  Auto)

---

Home Index