---

Step * 2 2 of Lemma append-tuple_wf


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 
BY
{ ((Assert 0 ≤ ||v|| BY Auto) THEN (OReduce 0 THENA Auto)) }

1
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
10. 0 ≤ ||v||
⊢ let a,b = x 
  in <a, append-tuple(((||v|| + 1) + 1) - 1;||L2||;b;y)> ∈ u × if null(v @ L2) then u1 else u1 × tuple-type(v @ L2) fi 

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  0  \mleq{}  ||v||  BY  Auto)  THEN  (OReduce  0  THENA  Auto))

---

Home Index