---

Step * of Lemma sum-map-append1

∀[f:Top]. ∀[L:Top List]. ∀[x:Top].  (Σf[x] for x ∈ L @ [x] ~ Σf[x] for x ∈ L + f[x])
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``sum-map`` 0
   THEN (RW (AddrC [1] (LemmaC `sum-unroll`)) 0 THENA Auto)
   THEN (Decide ⌜0 < ||L @ [x]||⌝⋅ THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN Try ((D -1 THEN Complete (Auto')))
   THEN (RWO "length-append" (-1) THENA Auto)
   THEN Subst' ||L @ [x]|| - 1 ~ ||L|| 0
   THEN Try ((RWO "length-append" 0 THEN Auto'))
   THEN EqCD) }

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

2
1. f : Top
2. L : Top List
3. x : Top
4. 0 < ||L|| + ||[x]||
⊢ f[L @ [x][||L||]] ~ f[x]

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[L:Top  List].  \mforall{}[x:Top].    (\mSigma{}f[x]  for  x  \mmember{}  L  @  [x]  \msim{}  \mSigma{}f[x]  for  x  \mmember{}  L  +  f[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``sum-map``  0
  THEN  (RW  (AddrC  [1]  (LemmaC  `sum-unroll`))  0  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}0  <  ||L  @  [x]||\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  Try  ((D  -1  THEN  Complete  (Auto')))
  THEN  (RWO  "length-append"  (-1)  THENA  Auto)
  THEN  Subst'  ||L  @  [x]||  -  1  \msim{}  ||L||  0
  THEN  Try  ((RWO  "length-append"  0  THEN  Auto'))
  THEN  EqCD)

---

Home Index