---

Step * 1 1 2 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
{ ((InstLemma `rsum-split2` [⌜0⌝;⌜n + 1⌝;⌜i⌝]⋅ THENA Auto) THEN (RWO "-1" 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) ∈ ℤ)
9. ∀[x:ℕ(n + 1) + 1 ⟶ ℝ]. (Σ{x[i] | 0≤i≤n + 1} = (Σ{x[i] | 0≤i≤i} + Σ{x[i] | i + 1≤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≤i}
+ Σ{if i@0 <z i then v i@0
  if i <z i@0 then v (i@0 - 1)
  else r0
  fi  | i + 1≤i@0≤n + 1})
= 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.  \mneg{}(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:
((InstLemma  `rsum-split2`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index