---

Step * 1 of Lemma length-zip


1. u : Top
2. v : Top List
3. ∀[bs:Top List]. ||zip(v;bs)|| ~ ||v|| supposing ||v|| = ||bs|| ∈ ℤ
4. u1 : Top
5. v1 : Top List
6. ||zip([u / v];v1)|| ~ ||[u / v]|| supposing ||[u / v]|| = ||v1|| ∈ ℤ
7. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
⊢ (||zip(v;v1)|| + 1) = (||v|| + 1) ∈ ℤ
BY
{ (RWO "3" 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[bs:Top  List].  ||zip(v;bs)||  \msim{}  ||v||  supposing  ||v||  =  ||bs||
4.  u1  :  Top
5.  v1  :  Top  List
6.  ||zip([u  /  v];v1)||  \msim{}  ||[u  /  v]||  supposing  ||[u  /  v]||  =  ||v1||
7.  (||v||  +  1)  =  (||v1||  +  1)
\mvdash{}  (||zip(v;v1)||  +  1)  =  (||v||  +  1)


By

---

Latex:
(RWO  "3"  0\mcdot{}  THEN  Auto)

---

Home Index