---

Step * of Lemma append-tuple_wf

∀[L1,L2:Type List]. ∀[x:tuple-type(L1)]. ∀[y:tuple-type(L2)].  (append-tuple(||L1||;||L2||;x;y) ∈ tuple-type(L1 @ L2))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN RecUnfold `append-tuple` 0
   THEN Reduce 0
   THEN Try (Trivial)
   THEN OldAutoSplit)⋅ }

1
1. u : Type
2. v : Type List
3. ∀[L2:Type List]. ∀[x:tuple-type(v)]. ∀[y:tuple-type(L2)].  (append-tuple(||v||;||L2||;x;y) ∈ tuple-type(v @ L2))
4. L2 : Type List
5. x : if null(v) then u else u × tuple-type(v) fi 
6. y : tuple-type(L2)
7. (v @ L2) = [] ∈ (Type List)
⊢ if ||v|| + 1 ≤z 0 then y
  if (||v|| + 1 =z 1) then if ||L2|| ≤z 0 then x else <x, y> fi 
  else let a,b = x 
       in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
  fi  ∈ u

2
1. u : Type
2. v : Type List
3. ∀[L2:Type List]. ∀[x:tuple-type(v)]. ∀[y:tuple-type(L2)].  (append-tuple(||v||;||L2||;x;y) ∈ tuple-type(v @ L2))
4. L2 : Type List
5. x : if null(v) then u else u × tuple-type(v) fi 
6. y : tuple-type(L2)
7. null(v @ L2) = ff
⊢ if ||v|| + 1 ≤z 0 then y
  if (||v|| + 1 =z 1) then if ||L2|| ≤z 0 then x else <x, y> fi 
  else let a,b = x 
       in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
  fi  ∈ u × tuple-type(v @ L2)

---

Latex:

---

Latex:
\mforall{}[L1,L2:Type  List].  \mforall{}[x:tuple-type(L1)].  \mforall{}[y:tuple-type(L2)].
    (append-tuple(||L1||;||L2||;x;y)  \mmember{}  tuple-type(L1  @  L2))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  RecUnfold  `append-tuple`  0
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  OldAutoSplit)\mcdot{}

---

Home Index