---

Step * 2 of Lemma sum-map-append1


1. f : Top
2. L : Top List
3. x : Top
4. 0 < ||L|| + ||[x]||
⊢ f[L @ [x][||L||]] ~ f[x]
BY
{ xxx(((RWO "select-append" 0 THENM AutoSplit) THENA Auto) THEN Subst' ||L|| - ||L|| ~ 0 0 THEN Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(((RWO  "select-append"  0  THENM  AutoSplit)  THENA  Auto)
        THEN  Subst'  ||L||  -  ||L||  \msim{}  0  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index