---

Step * of Lemma append-tuple-zero

∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[y:Top].  (append-tuple(||L||;0;x;y) ~ if (||L|| =z 0) then y else x fi )
BY
{ (InductionOnList
   THEN RecUnfold `append-tuple` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN Repeat (OldAutoSplit)
   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. 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

2
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

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[x:tuple-type(L)].  \mforall{}[y:Top].
    (append-tuple(||L||;0;x;y)  \msim{}  if  (||L||  =\msubz{}  0)  then  y  else  x  fi  )


By

---

Latex:
(InductionOnList
  THEN  RecUnfold  `append-tuple`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  (OldAutoSplit)
  THEN  Auto')

---

Home Index