---

Step * 2 2 1 1 of Lemma append-tuple_wf

.....subterm..... T:t
2:n
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) + 1) - 1;||L2||;x2;y) ∈ if null(v @ L2) then u1 else u1 × tuple-type(v @ L2) fi 
BY
{ (Subst' ((||v|| + 1) + 1) - 1 ~ ||v|| + 1 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. 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 

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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)  +  1)  -  1;||L2||;x2;y)  \mmember{}  if  null(v  @  L2)
    then  u1
    else  u1  \mtimes{}  tuple-type(v  @  L2)
    fi 


By

---

Latex:
(Subst'  ((||v||  +  1)  +  1)  -  1  \msim{}  ||v||  +  1  0  THENA  Auto)

---

Home Index