---

Step * 2 of Lemma tuple_wf


1. u : Type
2. v : Type List
3. (||v|| + 1) - 1 ≠ 0
4. ¬(v = [] ∈ (Type List))
5. ∀F:i:ℕ||v|| ⟶ v[i]
     (rec-case(map(λi.F[i];upto(||v||))) of
      [] => ⋅
      a::as =>
       r.if null(as) then a else <a, r> fi  ∈ tuple-type(v))
6. F : i:ℕ||v|| + 1 ⟶ [u / v][i]
7. ¬False
⊢ <F[0], rec-case(map(λx.F[x + 1];upto((||v|| + 1) - 1))) of [] => ⋅ | h::t => r.if null(t) then h else <h, r> fi > ∈ u
  × tuple-type(v)
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. u : Type
2. v : Type List
3. (||v|| + 1) - 1 ≠ 0
4. ¬(v = [] ∈ (Type List))
5. ∀F:i:ℕ||v|| ⟶ v[i]
     (rec-case(map(λi.F[i];upto(||v||))) of
      [] => ⋅
      a::as =>
       r.if null(as) then a else <a, r> fi  ∈ tuple-type(v))
6. F : i:ℕ||v|| + 1 ⟶ [u / v][i]
7. ¬False
⊢ F[0] ∈ u

2
.....subterm..... T:t
2:n
1. u : Type
2. v : Type List
3. (||v|| + 1) - 1 ≠ 0
4. ¬(v = [] ∈ (Type List))
5. ∀F:i:ℕ||v|| ⟶ v[i]
     (rec-case(map(λi.F[i];upto(||v||))) of
      [] => ⋅
      a::as =>
       r.if null(as) then a else <a, r> fi  ∈ tuple-type(v))
6. F : i:ℕ||v|| + 1 ⟶ [u / v][i]
7. ¬False
⊢ rec-case(map(λx.F[x + 1];upto((||v|| + 1) - 1))) of
  [] => ⋅
  h::t =>
   r.if null(t) then h else <h, r> fi  ∈ tuple-type(v)

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  (||v||  +  1)  -  1  \mneq{}  0
4.  \mneg{}(v  =  [])
5.  \mforall{}F:i:\mBbbN{}||v||  {}\mrightarrow{}  v[i]
          (rec-case(map(\mlambda{}i.F[i];upto(||v||)))  of
            []  =>  \mcdot{}
            a::as  =>
              r.if  null(as)  then  a  else  <a,  r>  fi    \mmember{}  tuple-type(v))
6.  F  :  i:\mBbbN{}||v||  +  1  {}\mrightarrow{}  [u  /  v][i]
7.  \mneg{}False
\mvdash{}  <F[0]
    ,  rec-case(map(\mlambda{}x.F[x  +  1];upto((||v||  +  1)  -  1)))  of
        []  =>  \mcdot{}
        h::t  =>
          r.if  null(t)  then  h  else  <h,  r>  fi 
    >  \mmember{}  u  \mtimes{}  tuple-type(v)


By

---

Latex:
MemCD

---

Home Index