---

Step * 1 of Lemma append-tuple_wf


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
BY
{ ((DVar `L2' THEN DVar `v') THEN (All Reduce THEN Try ((ImpossibleEq Auto (-1) THEN Auto)))⋅) }

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mforall{}[L2:Type  List].  \mforall{}[x:tuple-type(v)].  \mforall{}[y:tuple-type(L2)].
          (append-tuple(||v||;||L2||;x;y)  \mmember{}  tuple-type(v  @  L2))
4.  L2  :  Type  List
5.  x  :  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi 
6.  y  :  tuple-type(L2)
7.  (v  @  L2)  =  []
\mvdash{}  if  ||v||  +  1  \mleq{}z  0  then  y
    if  (||v||  +  1  =\msubz{}  1)  then  if  ||L2||  \mleq{}z  0  then  x  else  <x,  y>  fi 
    else  let  a,b  =  x 
              in  <a,  append-tuple((||v||  +  1)  -  1;||L2||;b;y)>
    fi    \mmember{}  u


By

---

Latex:
((DVar  `L2'  THEN  DVar  `v')  THEN  (All  Reduce  THEN  Try  ((ImpossibleEq  Auto  (-1)  THEN  Auto)))\mcdot{})

---

Home Index