---

Step * 1 of Lemma sum-map-append1


1. f : Top
2. L : Top List
3. x : Top
4. 0 < ||L|| + ||[x]||
⊢ Σ(f[L @ [x][i]] | i < ||L||) ~ Σ(f[L[i]] | i < ||L||)
BY
{ xxxAssert ⌜∀n:ℕ. ((n ≤ ||L||) ⇒ (Σ(f[L @ [x][i]] | i < n) ~ Σ(f[L[i]] | i < n)))⌝⋅xxx }

1
.....assertion..... 
1. f : Top
2. L : Top List
3. x : Top
4. 0 < ||L|| + ||[x]||
⊢ ∀n:ℕ. ((n ≤ ||L||) ⇒ (Σ(f[L @ [x][i]] | i < n) ~ Σ(f[L[i]] | i < n)))

2
1. f : Top
2. L : Top List
3. x : Top
4. 0 < ||L|| + ||[x]||
5. ∀n:ℕ. ((n ≤ ||L||) ⇒ (Σ(f[L @ [x][i]] | i < n) ~ Σ(f[L[i]] | i < n)))
⊢ Σ(f[L @ [x][i]] | i < ||L||) ~ Σ(f[L[i]] | i < ||L||)

---

Latex:

---

Latex:

1.  f  :  Top
2.  L  :  Top  List
3.  x  :  Top
4.  0  <  ||L||  +  ||[x]||
\mvdash{}  \mSigma{}(f[L  @  [x][i]]  |  i  <  ||L||)  \msim{}  \mSigma{}(f[L[i]]  |  i  <  ||L||)


By

---

Latex:
xxxAssert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  ((n  \mleq{}  ||L||)  {}\mRightarrow{}  (\mSigma{}(f[L  @  [x][i]]  |  i  <  n)  \msim{}  \mSigma{}(f[L[i]]  |  i  <  n)))\mkleeneclose{}\mcdot{}xxx

---

Home Index