---

Step * 1 1 2 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) ∈ ℤ)
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
BY
{ ((Assert Σ{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}
          = Σ{v (j - 1) | i + 1≤j≤n + 1} BY
          ((BLemma `rsum_functionality` THENA Auto) THEN D 0 THEN Reduce 0 THEN 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}))
10. Σ{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} = Σ{v (j - 1) | i + 1≤j≤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} + Σ{v (j - 1) | i + 1≤j≤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))
9.  \mforall{}[x:\mBbbN{}(n  +  1)  +  1  {}\mrightarrow{}  \mBbbR{}].  (\mSigma{}\{x[i]  |  0\mleq{}i\mleq{}n  +  1\}  =  (\mSigma{}\{x[i]  |  0\mleq{}i\mleq{}i\}  +  \mSigma{}\{x[i]  |  i  +  1\mleq{}i\mleq{}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{}i\}
+  \mSigma{}\{if  i@0  <z  i  then  v  i@0
    if  i  <z  i@0  then  v  (i@0  -  1)
    else  r0
    fi    |  i  +  1\mleq{}i@0\mleq{}n  +  1\})
=  r1


By

---

Latex:
((Assert  \mSigma{}\{if  i@0  <z  i  then  v  i@0
                if  i  <z  i@0  then  v  (i@0  -  1)
                else  r0
                fi    |  i  +  1\mleq{}i@0\mleq{}n  +  1\}
                =  \mSigma{}\{v  (j  -  1)  |  i  +  1\mleq{}j\mleq{}n  +  1\}  BY
                ((BLemma  `rsum\_functionality`  THENA  Auto)  THEN  D  0  THEN  Reduce  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  )

---

Home Index