---

Step * 2 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|| + 1) - 1;0;x2;y@0) ~ x2
BY
{ (Subst ⌜(||v|| + 1) - 1 ~ ||v||⌝ 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||;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.  x1  :  u
9.  x2  :  tuple-type(v)
10.  y@0  :  Top
\mvdash{}  append-tuple((||v||  +  1)  -  1;0;x2;y@0)  \msim{}  x2


By

---

Latex:
(Subst  \mkleeneopen{}(||v||  +  1)  -  1  \msim{}  ||v||\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index