---

Step * 1 1 1 of Lemma sum-map-append1


1. f : Top
2. L : Top List
3. x : Top
4. 0 < ||L|| + ||[x]||
5. n : ℤ
6. 0 < n
7. ((n - 1) ≤ ||L||) ⇒ (Σ(f[L @ [x][i]] | i < n - 1) ~ Σ(f[L[i]] | i < n - 1))
8. n ≤ ||L||
9. 0 < n
⊢ f[L @ [x][n - 1]] ~ f[L[n - 1]]
BY
{ xxx((RWO "select-append" 0 THENA Auto) THEN AutoSplit)xxx }

---

Latex:

---

Latex:

1.  f  :  Top
2.  L  :  Top  List
3.  x  :  Top
4.  0  <  ||L||  +  ||[x]||
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  ((n  -  1)  \mleq{}  ||L||)  {}\mRightarrow{}  (\mSigma{}(f[L  @  [x][i]]  |  i  <  n  -  1)  \msim{}  \mSigma{}(f[L[i]]  |  i  <  n  -  1))
8.  n  \mleq{}  ||L||
9.  0  <  n
\mvdash{}  f[L  @  [x][n  -  1]]  \msim{}  f[L[n  -  1]]


By

---

Latex:
xxx((RWO  "select-append"  0  THENA  Auto)  THEN  AutoSplit)xxx

---

Home Index