---

Step * 2 of Lemma update-tuple_wf


1. u : Type
2. v : Type List
3. ∀[n:ℕ]. ∀[x:tuple-type(v)].  ∀[y:v[n]]. (update-tuple(||v||;x;n;y) ∈ tuple-type(v)) supposing n < ||v||
⊢ ∀[n:ℕ]. ∀[x:if null(v) then u else u × tuple-type(v) fi ].
    ∀[y:[u / v][n]]
      (if (n =z 0)
       then if (||v|| + 1 =z 1) then y else <y, snd(x)> fi 
       else <fst(x), update-tuple((||v|| + 1) - 1;snd(x);n - 1;y)>
       fi  ∈ if null(v) then u else u × tuple-type(v) fi ) 
    supposing n < ||v|| + 1
BY
{ (Auto THEN DVar `v' THEN All Reduce THEN Auto') }

1
1. u : Type
2. u1 : Type
3. v : Type List
4. ∀[n:ℕ]. ∀[x:if null(v) then u1 else u1 × tuple-type(v) fi ].
     ∀[y:[u1 / v][n]]. (update-tuple(||v|| + 1;x;n;y) ∈ if null(v) then u1 else u1 × tuple-type(v) fi ) 
     supposing n < ||v|| + 1
5. n : {1...}
6. x : u × if null(v) then u1 else u1 × tuple-type(v) fi 
7. n < (||v|| + 1) + 1
8. y : [u; [u1 / v]][n]
9. ff ∈ 𝔹
⊢ update-tuple(((||v|| + 1) + 1) - 1;snd(x);n - 1;y) ∈ if null(v) then u1 else u1 × tuple-type(v) fi 

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mforall{}[n:\mBbbN{}].  \mforall{}[x:tuple-type(v)].
          \mforall{}[y:v[n]].  (update-tuple(||v||;x;n;y)  \mmember{}  tuple-type(v))  supposing  n  <  ||v||
\mvdash{}  \mforall{}[n:\mBbbN{}].  \mforall{}[x:if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi  ].
        \mforall{}[y:[u  /  v][n]]
            (if  (n  =\msubz{}  0)
              then  if  (||v||  +  1  =\msubz{}  1)  then  y  else  <y,  snd(x)>  fi 
              else  <fst(x),  update-tuple((||v||  +  1)  -  1;snd(x);n  -  1;y)>
              fi    \mmember{}  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi  ) 
        supposing  n  <  ||v||  +  1


By

---

Latex:
(Auto  THEN  DVar  `v'  THEN  All  Reduce  THEN  Auto')

---

Home Index