---

Step * 2 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. x : u × tuple-type(v)
9. y@0 : Top
⊢ let a,b = x 
  in <a, append-tuple((||v|| + 1) - 1;0;b;y@0)> ~ x
BY
{ ((D (-2) THEN Reduce 0) THEN Auto) }

1
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|| + 1) - 1;0;x2;y@0) ~ x2

---

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.  x  :  u  \mtimes{}  tuple-type(v)
9.  y@0  :  Top
\mvdash{}  let  a,b  =  x 
    in  <a,  append-tuple((||v||  +  1)  -  1;0;b;y@0)>  \msim{}  x


By

---

Latex:
((D  (-2)  THEN  Reduce  0)  THEN  Auto)

---

Home Index