---

Step * 2 1 1 of Lemma append-tuple-zero


1. u : Type
2. v : Type List
3. ∀[x:tuple-type(v)]. ∀[y:Top].  (append-tuple(||v||;0;x;y) ~ if (||v|| =z 0) then y else x fi )
4. null(v) = ff
5. 0 < ||v|| + 1
6. ¬((||v|| + 1) = 1 ∈ ℤ)
7. ¬((||v|| + 1) = 0 ∈ ℤ)
8. x1 : u
9. x2 : tuple-type(v)
10. y@0 : Top
⊢ append-tuple(||v||;0;x2;y@0) ~ x2
BY
{ ((RWO "3" 0 THEN Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mforall{}[x:tuple-type(v)].  \mforall{}[y:Top].    (append-tuple(||v||;0;x;y)  \msim{}  if  (||v||  =\msubz{}  0)  then  y  else  x  fi  )
4.  null(v)  =  ff
5.  0  <  ||v||  +  1
6.  \mneg{}((||v||  +  1)  =  1)
7.  \mneg{}((||v||  +  1)  =  0)
8.  x1  :  u
9.  x2  :  tuple-type(v)
10.  y@0  :  Top
\mvdash{}  append-tuple(||v||;0;x2;y@0)  \msim{}  x2


By

---

Latex:
((RWO  "3"  0  THEN  Auto)  THEN  AutoSplit)

---

Home Index