---

Step * 2 2 1 1 1 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. x1 : u
7. x2 : if null(v) then u1 else u1 × tuple-type(v) fi 
8. y : tuple-type(L2)
9. ff = ff
10. 0 < (||v|| + 1) + 1
11. 0 ≤ ||v||
⊢ append-tuple(||v|| + 1;||L2||;x2;y) ∈ if null(v @ L2) then u1 else u1 × tuple-type(v @ L2) fi 
BY
{ BackThruSomeHyp }

---

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.  x1  :  u
7.  x2  :  if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi 
8.  y  :  tuple-type(L2)
9.  ff  =  ff
10.  0  <  (||v||  +  1)  +  1
11.  0  \mleq{}  ||v||
\mvdash{}  append-tuple(||v||  +  1;||L2||;x2;y)  \mmember{}  if  null(v  @  L2)  then  u1  else  u1  \mtimes{}  tuple-type(v  @  L2)  fi 


By

---

Latex:
BackThruSomeHyp

---

Home Index