---

Step * 2 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. 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)
BY
{ ((Assert 0 < ||v|| + 1 BY Auto) THEN (OReduce 0 THENA Auto) THEN DVar `v' THEN All Reduce) }

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

2
1. u : Type
2. u1 : Type
3. v : Type List
4. ∀[L2:Type List]. ∀[x:if null(v) then u1 else u1 × tuple-type(v) fi ]. ∀[y:tuple-type(L2)].
     (append-tuple(||v|| + 1;||L2||;x;y) ∈ if null(v @ L2) then u1 else u1 × tuple-type(v @ L2) fi )
5. L2 : Type List
6. x : u × if null(v) then u1 else u1 × tuple-type(v) fi 
7. y : tuple-type(L2)
8. ff = ff
9. 0 < (||v|| + 1) + 1
⊢ if ((||v|| + 1) + 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) - 1;||L2||;b;y)>
  fi  ∈ u × if null(v @ L2) then u1 else u1 × tuple-type(v @ L2) fi 

---

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.  null(v  @  L2)  =  ff
\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  \mtimes{}  tuple-type(v  @  L2)


By

---

Latex:
((Assert  0  <  ||v||  +  1  BY  Auto)  THEN  (OReduce  0  THENA  Auto)  THEN  DVar  `v'  THEN  All  Reduce)

---

Home Index