---

Step * 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. v = [] ∈ (Type List)
5. 0 < ||v|| + 1
6. ¬((||v|| + 1) = 1 ∈ ℤ)
7. ¬((||v|| + 1) = 0 ∈ ℤ)
8. x : u
9. y@0 : Top
⊢ let a,b = x 
  in <a, append-tuple((||v|| + 1) - 1;0;b;y@0)> ~ x
BY
{ (D (-4) THEN (RWO "4" 0 THEN Reduce 0) THEN Auto) }

---

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.  v  =  []
5.  0  <  ||v||  +  1
6.  \mneg{}((||v||  +  1)  =  1)
7.  \mneg{}((||v||  +  1)  =  0)
8.  x  :  u
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  (-4)  THEN  (RWO  "4"  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index