---

Step * 2 1 of Lemma update-tuple_wf


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 
BY
{ ((Subst ⌜((||v|| + 1) + 1) - 1 ~ ||v|| + 1⌝ 0⋅ THENA Auto) THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  Type
2.  u1  :  Type
3.  v  :  Type  List
4.  \mforall{}[n:\mBbbN{}].  \mforall{}[x:if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi  ].
          \mforall{}[y:[u1  /  v][n]]
              (update-tuple(||v||  +  1;x;n;y)  \mmember{}  if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi  ) 
          supposing  n  <  ||v||  +  1
5.  n  :  \{1...\}
6.  x  :  u  \mtimes{}  if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi 
7.  n  <  (||v||  +  1)  +  1
8.  y  :  [u;  [u1  /  v]][n]
9.  ff  \mmember{}  \mBbbB{}
\mvdash{}  update-tuple(((||v||  +  1)  +  1)  -  1;snd(x);n  -  1;y)  \mmember{}  if  null(v)
    then  u1
    else  u1  \mtimes{}  tuple-type(v)
    fi 


By

---

Latex:
((Subst  \mkleeneopen{}((||v||  +  1)  +  1)  -  1  \msim{}  ||v||  +  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index