---

Step * 1 1 of Lemma sum-map-append1

.....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)))
BY
{ xxx(InductionOnNat
      THEN (UnivCD THENA Auto)
      THEN Reduce 0
      THEN Try (Trivial)
      THEN (RWO "sum-unroll" 0 THENA Auto)
      THEN AutoSplit
      THEN EqCD
      THEN Try ((BackThruSomeHyp THEN Auto)))xxx }

1
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]]

---

Latex:

---

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


By

---

Latex:
xxx(InductionOnNat
        THEN  (UnivCD  THENA  Auto)
        THEN  Reduce  0
        THEN  Try  (Trivial)
        THEN  (RWO  "sum-unroll"  0  THENA  Auto)
        THEN  AutoSplit
        THEN  EqCD
        THEN  Try  ((BackThruSomeHyp  THEN  Auto)))xxx

---

Home Index