---

Step * 1 2 of Lemma sum-map-append1


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||)
BY
{ xxx(BHyp -1  THEN Auto)xxx }

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(BHyp  -1    THEN  Auto)xxx

---

Home Index