---

Step * 1 of Lemma select-update-tuple

.....wf..... 
1. m : ℤ
2. 0 < m
3. ∀[n:ℕ]. ∀[L:Type List].
     (∀[x:tuple-type(L)]. ∀[y:Top].
        (update-tuple(||L||;x;n;y).m - 1 ~ if (n =z m - 1) then y else x.m - 1 fi )) supposing 
        (m - 1 < ||L|| and 
        n < ||L||)
4. n : ℕ
5. u : Type
6. v : Type List
7. n < ||v|| + 1
8. m < ||v|| + 1
9. x : if null(v) then u else u × tuple-type(v) fi 
10. y : Top
11. ¬(m = 0 ∈ ℤ)
12. ¬(n = 0 ∈ ℤ)
⊢ snd(x) ∈ tuple-type(v)
BY
{ (At ⌜𝕌'⌝ (SplitOnHypITE -4 )⋅ THEN Auto) }

1
.....truecase..... 
1. m : ℤ
2. 0 < m
3. ∀[n:ℕ]. ∀[L:Type List].
     (∀[x:tuple-type(L)]. ∀[y:Top].
        (update-tuple(||L||;x;n;y).m - 1 ~ if (n =z m - 1) then y else x.m - 1 fi )) supposing 
        (m - 1 < ||L|| and 
        n < ||L||)
4. n : ℕ
5. u : Type
6. v : Type List
7. n < ||v|| + 1
8. m < ||v|| + 1
9. x : u
10. y : Top
11. ¬(m = 0 ∈ ℤ)
12. ¬(n = 0 ∈ ℤ)
13. v = [] ∈ (Type List)
⊢ snd(x) ∈ tuple-type(v)

---

Latex:

---

Latex:
.....wf..... 
1.  m  :  \mBbbZ{}
2.  0  <  m
3.  \mforall{}[n:\mBbbN{}].  \mforall{}[L:Type  List].
          (\mforall{}[x:tuple-type(L)].  \mforall{}[y:Top].
                (update-tuple(||L||;x;n;y).m  -  1  \msim{}  if  (n  =\msubz{}  m  -  1)  then  y  else  x.m  -  1  fi  ))  supposing 
                (m  -  1  <  ||L||  and 
                n  <  ||L||)
4.  n  :  \mBbbN{}
5.  u  :  Type
6.  v  :  Type  List
7.  n  <  ||v||  +  1
8.  m  <  ||v||  +  1
9.  x  :  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi 
10.  y  :  Top
11.  \mneg{}(m  =  0)
12.  \mneg{}(n  =  0)
\mvdash{}  snd(x)  \mmember{}  tuple-type(v)


By

---

Latex:
(At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (SplitOnHypITE  -4  )\mcdot{}  THEN  Auto)

---

Home Index