---

Step * 2 2 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. 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 
BY
{ ((D -5 THEN Reduce 0) THEN MemCD THEN Try (Trivial)) }

1
.....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 

---

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
10.  0  \mleq{}  ||v||
\mvdash{}  let  a,b  =  x 
    in  <a,  append-tuple(((||v||  +  1)  +  1)  -  1;||L2||;b;y)>  \mmember{}  u  \mtimes{}  if  null(v  @  L2)
                                                                                                                              then  u1
                                                                                                                              else  u1  \mtimes{}  tuple-type(v  @  L2)
                                                                                                                              fi 


By

---

Latex:
((D  -5  THEN  Reduce  0)  THEN  MemCD  THEN  Try  (Trivial))

---

Home Index