---

Step * 1 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) - 1}
+ if n + 1 <z i then v (n + 1)
  if i <z n + 1 then v ((n + 1) - 1)
  else r0
  fi )
= 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  | 0≤i@0≤(n + 1) - 1} = Σ{v i | 0≤i≤n} BY
          ((Subst' (n + 1) - 1 ~ n 0 THENA Auto)
           THEN BLemma `rsum_functionality`
           THEN Auto
           THEN D 0
           THEN Reduce 0
           THEN Auto))
   THEN RWO "-1" 0
   THEN Auto) }

---

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)  -  1\}
+  if  n  +  1  <z  i  then  v  (n  +  1)
    if  i  <z  n  +  1  then  v  ((n  +  1)  -  1)
    else  r0
    fi  )
=  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    |  0\mleq{}i@0\mleq{}(n  +  1)  -  1\}
                =  \mSigma{}\{v  i  |  0\mleq{}i\mleq{}n\}  BY
                ((Subst'  (n  +  1)  -  1  \msim{}  n  0  THENA  Auto)
                  THEN  BLemma  `rsum\_functionality`
                  THEN  Auto
                  THEN  D  0
                  THEN  Reduce  0
                  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index